Commit 2024-07-10 17:26 825cb2cd

feat(CategoryTheory): (co)limits in the category of coalgebras (#14236) 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.