[Merged by Bors] - feat(CategoryTheory): Beck's comonadicity theorem by mckoen · Pull Request #14238 · leanprover-community/mathlib4

mckoen · 2024-06-28T20:25:29Z

Prove Beck's comonadicity theorem by dualizing everything in CategoryTheory.Monad.Monadicity.

This contribution was created as part of the AIM workshop "Formalizing Algebraic Geometry" in June 2024.

depends on: [Merged by Bors] - feat(CategoryTheory): Split equalizers #14170
depends on: [Merged by Bors] - feat(CategoryTheory): Special equalizers associated to a comonad #14171
depends on: [Merged by Bors] - feat(CategoryTheory): (co)limits in the category of coalgebras #14236

…unity/mathlib4 into mckoen/AIM_comonadicity3

github-actions · 2024-06-28T20:26:13Z

PR summary 37d2a649e9

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.CategoryTheory.Monad.Comonadicity`	555

Declarations diff

+ CreatesLimitOfIsCosplitPair
+ HasEqualizerOfIsCosplitPair
+ PreservesLimitOfIsCoreflexivePair
+ PreservesLimitOfIsCosplitPair
+ ReflectsLimitOfIsCosplitPair
+ comonadicOfCreatesFSplitEqualizers
+ comonadicOfHasPreservesCoreflexiveEqualizersOfReflectsIsomorphisms
+ comonadicOfHasPreservesFSplitEqualizersOfReflectsIsomorphisms
+ comonadicOfHasPreservesReflectsFSplitEqualizers
+ comparisonAdjunction
+ comparisonAdjunction_counit_f
+ comparisonAdjunction_counit_f_aux
+ comparisonAdjunction_unit_app
+ comparisonRightAdjointHomEquiv
+ comparisonRightAdjointObj
+ counitFork
+ counitLimitOfPreservesEqualizer
+ createsFSplitEqualizersOfComonadic
+ instance [CreatesLimitOfIsCosplitPair F] : ∀ (A : Coalgebra adj.toComonad),
+ instance [HasEqualizerOfIsCosplitPair F] : ∀ (A : Coalgebra adj.toComonad),
+ instance [PreservesLimitOfIsCoreflexivePair F] : ∀ X : Coalgebra adj.toComonad,
+ instance [PreservesLimitOfIsCosplitPair F] : ∀ (A : Coalgebra adj.toComonad),
+ instance [ReflectsLimitOfIsCosplitPair F] : ∀ (A : Coalgebra adj.toComonad),
+ instance {A B} (f g : A ⟶ B) [F.IsCosplitPair f g] [CreatesLimitOfIsCosplitPair F] :
+ instance {A B} (f g : A ⟶ B) [F.IsCosplitPair f g] [PreservesLimitOfIsCosplitPair F] :
+ instance {A B} (f g : A ⟶ B) [F.IsCosplitPair f g] [ReflectsLimitOfIsCosplitPair F] :
+ instance {A B} (f g : A ⟶ B) [IsCoreflexivePair f g] [PreservesLimitOfIsCoreflexivePair F] :
+ main_pair_F_cosplit
+ main_pair_coreflexive
+ rightAdjointComparison
+ unitEqualizerOfCoreflectsEqualizer
+ unitFork
+ unitFork_ι

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

ghost · 2024-07-10T18:22:34Z

This PR/issue depends on:

~~[Merged by Bors] - feat(CategoryTheory): Split equalizers #14170~~
~~[Merged by Bors] - feat(CategoryTheory): Special equalizers associated to a comonad #14171~~
~~[Merged by Bors] - feat(CategoryTheory): (co)limits in the category of coalgebras #14236~~
By Dependent Issues (🤖). Happy coding!

Mathlib/CategoryTheory/Monad/Comonadicity.lean

dagurtomas

Please add comments in the module docstrings of both files Comonadicity and Monadicity to keep them in sync.

You should also merge master and make sure everything works with the new variable incusion mechanism. Otherwise LGTM.

Mathlib/CategoryTheory/Monad/Comonadicity.lean

Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>

dagurtomas · 2024-08-22T06:59:59Z

Thanks!

maintainer merge

github-actions · 2024-08-22T07:00:10Z

🚀 Pull request has been placed on the maintainer queue by dagurtomas.

kim-em · 2024-08-22T07:53:12Z

bors merge

Prove Beck's comonadicity theorem by dualizing everything in [CategoryTheory.Monad.Monadicity](https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Monad/Monadicity.html). This contribution was created as part of the AIM workshop "Formalizing Algebraic Geometry" in June 2024. Co-authored-by: dagurtomas <dagurtomas@gmail.com> Co-authored-by: adamtopaz <github@adamtopaz.com> Co-authored-by: Jack McKoen <104791831+mckoen@users.noreply.github.com>

mathlib-bors · 2024-08-22T09:16:15Z

Pull request successfully merged into master.

Build succeeded:

Prove Beck's comonadicity theorem by dualizing everything in [CategoryTheory.Monad.Monadicity](https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Monad/Monadicity.html). This contribution was created as part of the AIM workshop "Formalizing Algebraic Geometry" in June 2024. Co-authored-by: dagurtomas <dagurtomas@gmail.com> Co-authored-by: adamtopaz <github@adamtopaz.com> Co-authored-by: Jack McKoen <104791831+mckoen@users.noreply.github.com>

mckoen and others added 16 commits June 26, 2024 13:48

splitequalizer

4b47e20

equalizer

3004dd4

change splitequalizer.lean

f210089

dualise limits and fill in comonadicity

428178e

close a sorry

c95407d

close a sorry

b5b9d0f

last sorry in limits file

7e54a6f

wip

a2a8f01

Merge branch 'mckoen/AIM_comonadicity3' of github.com:leanprover-comm…

c88c0fc

…unity/mathlib4 into mckoen/AIM_comonadicity3

kill two sorries

8e8e7d7

kill last sorry

0102303

rename

20bcedd

finish Limits.lean, dualise some of Adjunction.lean

4086109

fix last sorry

72ae623

change some docstrings

b925da1

add to mathlib

873f1b9

mckoen added WIP Work in progress t-category-theory Category theory t-algebraic-geometry Algebraic geometry workshop-AIM-AG-2024 This PR is associated with the 2024 AIM workshop on formalization of algebraic geometry labels Jun 28, 2024

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Jun 28, 2024

lint

5189ff5

ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 28, 2024

mckoen added 2 commits June 28, 2024 14:32

add to mathlib

18530eb

alphabet

3778d48

ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 2, 2024

ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 10, 2024

Merge branch 'master' into mckoen/AIM_comonadicity3

85dd2fa

ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 10, 2024

mckoen added 2 commits July 10, 2024 13:57

add to mathlib

64f9a82

fix docstrings and tidy

c86d3f1

mckoen removed the WIP Work in progress label Jul 10, 2024

mckoen requested a review from adamtopaz July 17, 2024 21:26

mckoen added 2 commits August 21, 2024 13:26

add a few docstrings

163421a

line too long

23f8b80

mckoen requested a review from dagurtomas August 21, 2024 19:55

dagurtomas reviewed Aug 21, 2024

View reviewed changes

Mathlib/CategoryTheory/Monad/Comonadicity.lean Outdated Show resolved Hide resolved

dagurtomas approved these changes Aug 21, 2024

View reviewed changes

mckoen and others added 3 commits August 21, 2024 21:55

Apply suggestions from code review

f8ab655

Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>

Merge branch 'master' into mckoen/AIM_comonadicity3

78c8246

merge mathlib and sync docstrings

37d2a64

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Aug 22, 2024

github-actions bot added the ready-to-merge This PR has been sent to bors. label Aug 22, 2024

mathlib-bors bot changed the title ~~feat(CategoryTheory): Beck's comonadicity theorem~~ [Merged by Bors] - feat(CategoryTheory): Beck's comonadicity theorem Aug 22, 2024

mathlib-bors bot closed this Aug 22, 2024

mathlib-bors bot deleted the mckoen/AIM_comonadicity3 branch August 22, 2024 09:16

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(CategoryTheory): Beck's comonadicity theorem#14238

[Merged by Bors] - feat(CategoryTheory): Beck's comonadicity theorem#14238
mckoen wants to merge 27 commits intomasterfrom
mckoen/AIM_comonadicity3

mckoen commented Jun 28, 2024 •

edited

Loading

Uh oh!

github-actions bot commented Jun 28, 2024 •

edited

Loading

Declarations diff

Uh oh!

ghost commented Jul 10, 2024

Uh oh!

Uh oh!

dagurtomas left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

dagurtomas commented Aug 22, 2024

Uh oh!

github-actions bot commented Aug 22, 2024

Uh oh!

kim-em commented Aug 22, 2024

Uh oh!

mathlib-bors bot commented Aug 22, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

mckoen commented Jun 28, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jun 28, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 37d2a649e9

Import changes for modified files

Declarations diff

Uh oh!

ghost commented Jul 10, 2024

Uh oh!

Uh oh!

dagurtomas left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

dagurtomas commented Aug 22, 2024

Uh oh!

github-actions bot commented Aug 22, 2024

Uh oh!

kim-em commented Aug 22, 2024

Uh oh!

mathlib-bors bot commented Aug 22, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

mckoen commented Jun 28, 2024 •

edited

Loading

github-actions bot commented Jun 28, 2024 •

edited

Loading