Skip to content

[Merged by Bors] - feat(CategoryTheory): Special equalizers associated to a comonad#14171

Closed
mckoen wants to merge 6 commits intomasterfrom
mckoen/AIM_comonadicity2
Closed

[Merged by Bors] - feat(CategoryTheory): Special equalizers associated to a comonad#14171
mckoen wants to merge 6 commits intomasterfrom
mckoen/AIM_comonadicity2

Conversation

@mckoen
Copy link
Copy Markdown
Collaborator

@mckoen mckoen commented Jun 26, 2024 •
edited
Loading

Given a comonad, shows that any coalgebra is an equalizer (in the category of coalgebras) of cofree coalgebras, and shows this equalizer is coreflexive.

Also constructs the Beck fork in the category of coalgebras, and shows the fork is coreflexive as well as a split equalizer (in particular, an equalizer).

This dualises everything in Mathlib.CategoryTheory.Monad.Coequalizer.

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

Open in Gitpod

@mckoen mckoen added the t-category-theory Category theory label Jun 26, 2024
@github-actions 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 26, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 26, 2024 •
edited
Loading

PR summary 2b54da2a7a

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.CategoryTheory.Monad.Equalizer 532

Declarations diff

+ CofreeEqualizer.bottomMap
+ CofreeEqualizer.condition
+ CofreeEqualizer.topMap
+ CofreeEqualizer.ι
+ beckCoalgebraEqualizer
+ beckCoalgebraFork
+ beckEqualizer
+ beckEqualizer_lift
+ beckFork
+ beckFork_ι
+ beckSplitEqualizer
+ instance : IsCoreflexivePair (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X) := by

You can run this locally as follows 
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

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

@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 26, 2024
@joelriou joelriou added the t-algebraic-geometry Algebraic geometry label Jun 26, 2024
@kbuzzard
Copy link
Copy Markdown
Member

kbuzzard commented Jun 28, 2024

Can you add a comment in the first message of this PR saying "This contribution was created as part of the AIM workshop "Formalizing Algebraic Geometry" in June 2024."?

@mckoen mckoen added the workshop-AIM-AG-2024 This PR is associated with the 2024 AIM workshop on formalization of algebraic geometry label Jun 28, 2024
@mckoen mckoen mentioned this pull request Jun 28, 2024
Closed
3 tasks
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 2, 2024
@ghost
Copy link
Copy Markdown

ghost commented Jul 2, 2024

This PR/issue depends on:

dagurtomas
dagurtomas approved these changes Jul 3, 2024
View reviewed changes
@dagurtomas dagurtomas added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jul 3, 2024
mckoen and others added 2 commits July 3, 2024 15:55
@mckoen @dagurtomas
Update Mathlib/CategoryTheory/Monad/Equalizer.lean
ee60b02 
Co-authored-by: Dagur Tómas Ásgeirsson <dagurtomas@gmail.com>
@mckoen @dagurtomas
Update Mathlib/CategoryTheory/Monad/Equalizer.lean
2b54da2 
Co-authored-by: Dagur Tómas Ásgeirsson <dagurtomas@gmail.com>
@mckoen mckoen added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jul 4, 2024
@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Jul 4, 2024

Thanks 🎉

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jul 4, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jul 4, 2024
@mckoen
feat(CategoryTheory): Special equalizers associated to a comonad (#14171
1b306ae 
)

Given a comonad, shows that any coalgebra is an equalizer (in the category of coalgebras) of cofree coalgebras, and shows this equalizer is coreflexive. 

Also constructs the Beck fork in the category of coalgebras, and shows the fork is coreflexive as well as a split equalizer (in particular, an equalizer).

This dualises everything in [Mathlib.CategoryTheory.Monad.Coequalizer](https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Monad/Coequalizer.html).

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



Co-authored-by: Jack <104791831+mckoen@users.noreply.github.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 4, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(CategoryTheory): Special equalizers associated to a comonad [Merged by Bors] - feat(CategoryTheory): Special equalizers associated to a comonad Jul 4, 2024
@mathlib-bors mathlib-bors bot closed this Jul 4, 2024
@mathlib-bors mathlib-bors bot deleted the mckoen/AIM_comonadicity2 branch July 4, 2024 14:23
@adomani adomani mentioned this pull request Aug 1, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@dagurtomas dagurtomas dagurtomas approved these changes

Assignees

No one assigned

Labels

new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! ready-to-merge This PR has been sent to bors. t-algebraic-geometry Algebraic geometry t-category-theory Category theory workshop-AIM-AG-2024 This PR is associated with the 2024 AIM workshop on formalization of algebraic geometry

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@mckoen @kbuzzard @jcommelin @dagurtomas @joelriou