[Merged by Bors] - feat(CategoryTheory): (co)limits in the category of coalgebras#14236
[Merged by Bors] - feat(CategoryTheory): (co)limits in the category of coalgebras#14236
Conversation
…unity/mathlib4 into mckoen/AIM_comonadicity3
PR summary cf2493aad9
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers | 381 | 382 | +1 (+0.26%) |
Import changes for all files
| Files | Import difference |
|---|---|
| Too many changes (271)! |
Declarations diff
+ coconePoint
+ commuting
+ comonadicCreatesColimits
+ comonadicCreatesLimitOfPreservesLimit
+ comonadicCreatesLimitsOfPreservesLimits
+ comonadicCreatesLimitsOfShapeOfPreservesLimitsOfShape
+ comp_comparison_forget_hasColimit
+ comp_comparison_hasColimit
+ comparison_essSurj
+ comparison_full
+ conePoint
+ forgetCreatesColimit
+ forgetCreatesLimit
+ forgetCreatesLimits
+ forgetCreatesLimitsOfShape
+ forget_creates_limits_of_comonad_preserves
+ hasColimit_of_comp_forget_hasColimit
+ hasColimit_of_coreflective
+ hasColimitsOfShape_of_coreflective
+ hasColimits_of_coreflective
+ hasLimitsOfShape_of_coreflective
+ hasLimits_of_coreflective
+ instance (priority := 1) preservesSplitEqualizers (f g : X ⟶ Y) [HasSplitEqualizer f g] :
+ instance (priority := 100) comonadicOfCoreflective [Coreflective R] :
+ instance [Coreflective R] (X : (coreflectorAdjunction R).toComonad.Coalgebra) :
+ instance δ_iso_of_coreflective [Coreflective R] : IsIso (coreflectorAdjunction R).toComonad.δ := by
+ liftedCocone
+ liftedCoconeIsColimit
+ liftedCone
+ liftedConeIsLimit
+ newCocone
+ newCone
+ rightAdjointPreservesInitialOfCoreflective
++ γ
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>|
This PR/issue depends on:
|
Shows that the forgetful functor `forget T : Coalgebra T ⥤ C` for a comonad `T : C ⥤ C` creates colimits and creates any limits which `T` preserves. This is used to show that `Coalgebra T` has any colimits which `C` has, and any limits which `C` has and `T` preserves. This is generalised to the case of a comonadic functor `D ⥤ C`. Dualises everything currently in [Mathlib.CategoryTheory.Monad.Limits](https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Monad/Limits.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>
|
Pull request successfully merged into master. Build succeeded: |
Shows that the forgetful functor
forget T : Coalgebra T ⥤ Cfor a comonadT : C ⥤ Ccreates colimits and creates any limits whichTpreserves. This is used to show thatCoalgebra Thas any colimits whichChas, and any limits whichChas andTpreserves. This is generalised to the case of a comonadic functorD ⥤ C.Dualises everything currently in Mathlib.CategoryTheory.Monad.Limits.
This contribution was created as part of the AIM workshop "Formalizing Algebraic Geometry" in June 2024.