mathlib documentation

category_theory.monad.limits

(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

(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 limits then any reflective subcategory has limits.