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.

---

• [x] depends on: #14170