mathlib documentation


Limits and colimits in the category of algebras #

This file shows that the forgetful functor forget T : algebra T ⥤ C for a monad T : C ⥤ C creates limits and creates any colimits which T preserves. This is used to show that algebra T has any limits which C has, and any colimits which C has and T preserves. This is generalised to the case of a monadic functor D ⥤ C.


Dualise for the category of coalgebras and comonadic left adjoints.

(Impl) The natural transformation used to define the new cone


(Impl) The natural transformation given by the algebra structure maps, used to construct a cocone c with apex colimit (D ⋙ forget T).


(Impl) A cocone for the diagram (D ⋙ forget T) ⋙ T found by composing the natural transformation γ with the colimiting cocone for D ⋙ forget T.


(Impl) Define the map λ : TL ⟶ L, which will serve as the structure of the coalgebra on L, and we will show is the colimiting object. We use the cocone constructed by c and the fact that T preserves colimits to produce this morphism.


(Impl) Construct the colimiting algebra from the map λ : TL ⟶ L given by lambda. We are required to show it satisfies the two algebra laws, which follow from the algebra laws for the image of D and our commuting lemma.


For D : J ⥤ algebra T, D ⋙ forget T has a colimit, then D has a colimit provided colimits of shape J are preserved by T.

If C has limits of shape J then any reflective subcategory has limits of shape J.

If C has colimits of shape J then any reflective subcategory has colimits of shape J.