mathlib3 documentation

category_theory.monad.limits

Limits and colimits in the category of algebras #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

TODO #

Dualise for the category of coalgebras and comonadic left adjoints.

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

Equations

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

Equations

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

Equations
@[reducible]

(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.

Equations

(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.

Equations

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.