[Merged by Bors] - feat(CategoryTheory): (co)limits in the category of coalgebras

[mckoen]

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.

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

[github-actions]

PR summary cf2493aad9

Import changes for modified files

Dependency changes

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>

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(CategoryTheory): Split equalizers #14170
  By Dependent Issues (🤖). Happy coding!

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style