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

## TODO #

def category_theory.monad.forget_creates_limits.γ {C : Type u₁} {T : category_theory.monad C} {J : Type u} (D : J T.algebra) :

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

Equations
@[simp]
theorem category_theory.monad.forget_creates_limits.γ_app {C : Type u₁} {T : category_theory.monad C} {J : Type u} (D : J T.algebra) (j : J) :
= (D.obj j).a

(Impl) This new cone is used to construct the algebra structure

Equations
@[simp]
theorem category_theory.monad.forget_creates_limits.new_cone_π_app {C : Type u₁} {T : category_theory.monad C} {J : Type u} (D : J T.algebra) (c : category_theory.limits.cone (D T.forget)) (X : J) :
= T.map (c.π.app X) (D.obj X).a

The algebra structure which will be the apex of the new limit cone for D.

Equations
@[simp]
@[simp]

(Impl) Construct the lifted cone in algebra T which will be limiting.

Equations
@[simp]
theorem category_theory.monad.forget_creates_limits.lifted_cone_π_app_f {C : Type u₁} {T : category_theory.monad C} {J : Type u} (D : J T.algebra) (c : category_theory.limits.cone (D T.forget)) (j : J) :
.f = c.π.app j
@[simp]

(Impl) Prove that the lifted cone is limiting.

Equations
@[protected, instance]
noncomputable def category_theory.monad.forget_creates_limits {C : Type u₁} {T : category_theory.monad C} :

The forgetful functor from the Eilenberg-Moore category creates limits.

Equations
theorem category_theory.monad.has_limit_of_comp_forget_has_limit {C : Type u₁} {T : category_theory.monad C} {J : Type u} (D : J T.algebra)  :

D ⋙ forget T has a limit, then D has a limit.

@[simp]
theorem category_theory.monad.forget_creates_colimits.γ_app {C : Type u₁} {T : category_theory.monad C} {J : Type u} {D : J T.algebra} (j : J) :
def category_theory.monad.forget_creates_colimits.γ {C : Type u₁} {T : category_theory.monad C} {J : Type u} {D : J T.algebra} :

(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
theorem category_theory.monad.forget_creates_colimits.commuting {C : Type u₁} {T : category_theory.monad C} {J : Type u} {D : J T.algebra} (c : category_theory.limits.cocone (D T.forget)) (j : J) :
= (D.obj j).a c.ι.app j

(Impl) The key property defining the map λ : TL ⟶ L.

(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
@[simp]
@[simp]
@[simp]
theorem category_theory.monad.forget_creates_colimits.lifted_cocone_ι_app_f {C : Type u₁} {T : category_theory.monad C} {J : Type u} {D : J T.algebra} (c : category_theory.limits.cocone (D T.forget)) [ T] (j : J) :
= c.ι.app j

(Impl) Construct the lifted cocone in algebra T which will be colimiting.

Equations

(Impl) Prove that the lifted cocone is colimiting.

Equations
@[protected, instance]
noncomputable def category_theory.monad.forget_creates_colimit {C : Type u₁} {T : category_theory.monad C} {J : Type u} (D : J T.algebra) [ T] :

The forgetful functor from the Eilenberg-Moore category for a monad creates any colimit which the monad itself preserves.

Equations
@[protected, instance]
noncomputable def category_theory.monad.forget_creates_colimits_of_shape {C : Type u₁} {T : category_theory.monad C} {J : Type u}  :
Equations
@[protected, instance]
noncomputable def category_theory.monad.forget_creates_colimits {C : Type u₁} {T : category_theory.monad C}  :
Equations
theorem category_theory.monad.forget_creates_colimits_of_monad_preserves {C : Type u₁} {T : category_theory.monad C} {J : Type u} (D : J T.algebra)  :

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.

@[protected, instance]
def category_theory.comp_comparison_forget_has_limit {C : Type u₁} {D : Type u₂} {J : Type u} (F : J D) (R : D C)  :
@[protected, instance]
def category_theory.comp_comparison_has_limit {C : Type u₁} {D : Type u₂} {J : Type u} (F : J D) (R : D C)  :
noncomputable def category_theory.monadic_creates_limits {C : Type u₁} {D : Type u₂} (R : D C)  :

Equations
noncomputable def category_theory.monadic_creates_colimit_of_preserves_colimit {C : Type u₁} {D : Type u₂} {J : Type u} (R : D C) (K : J D) [ ] :

The forgetful functor from the Eilenberg-Moore category for a monad creates any colimit which the monad itself preserves.

Equations
noncomputable def category_theory.monadic_creates_colimits_of_shape_of_preserves_colimits_of_shape {C : Type u₁} {D : Type u₂} {J : Type u} (R : D C)  :

A monadic functor creates any colimits of shapes it preserves.

Equations
noncomputable def category_theory.monadic_creates_colimits_of_preserves_colimits {C : Type u₁} {D : Type u₂} (R : D C)  :

A monadic functor creates colimits if it preserves colimits.

Equations
theorem category_theory.has_limit_of_reflective {C : Type u₁} {D : Type u₂} {J : Type u} (F : J D) (R : D C)  :
theorem category_theory.has_limits_of_shape_of_reflective {C : Type u₁} {D : Type u₂} {J : Type u} (R : D C)  :

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

theorem category_theory.has_limits_of_reflective {C : Type u₁} {D : Type u₂} (R : D C)  :

If C has limits then any reflective subcategory has limits.

theorem category_theory.has_colimits_of_shape_of_reflective {C : Type u₁} {D : Type u₂} {J : Type u} (R : D C)  :

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

theorem category_theory.has_colimits_of_reflective {C : Type u₁} {D : Type u₂} (R : D C)  :

If C has colimits then any reflective subcategory has colimits.

noncomputable def category_theory.left_adjoint_preserves_terminal_of_reflective {C : Type u₁} {D : Type u₂} (R : D C)  :

The reflector always preserves terminal objects. Note this in general doesn't apply to any other limit.

Equations