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

@[simp]
theorem CategoryTheory.Monad.ForgetCreatesLimits.γ_app {C : Type u₁} [] {T : } {J : Type u} (j : J) :
= (D.obj j).a
def CategoryTheory.Monad.ForgetCreatesLimits.γ {C : Type u₁} [] {T : } {J : Type u} :

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

Instances For
@[simp]
theorem CategoryTheory.Monad.ForgetCreatesLimits.newCone_π_app {C : Type u₁} [] {T : } {J : Type u} (X : J) :
.app X = CategoryTheory.CategoryStruct.comp (T.map (c.app X)) (D.obj X).a

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

Instances For
@[simp]
theorem CategoryTheory.Monad.ForgetCreatesLimits.conePoint_A {C : Type u₁} [] {T : } {J : Type u} :
= c.pt
@[simp]

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

Instances For
@[simp]
@[simp]
theorem CategoryTheory.Monad.ForgetCreatesLimits.liftedCone_π_app_f {C : Type u₁} [] {T : } {J : Type u} (j : J) :
(.app j).f = c.app j

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

Instances For
@[simp]

(Impl) Prove that the lifted cone is limiting.

Instances For
noncomputable instance CategoryTheory.Monad.forgetCreatesLimits {C : Type u₁} [] {T : } :

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

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

@[simp]
theorem CategoryTheory.Monad.ForgetCreatesColimits.γ_app {C : Type u₁} [] {T : } {J : Type u} (j : J) :
def CategoryTheory.Monad.ForgetCreatesColimits.γ {C : Type u₁} [] {T : } {J : Type u} :

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

Instances For
@[simp]
theorem CategoryTheory.Monad.ForgetCreatesColimits.newCocone_ι {C : Type u₁} [] {T : } {J : Type u} :
@[simp]

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

Instances For
@[reducible]
def CategoryTheory.Monad.ForgetCreatesColimits.lambda {C : Type u₁} [] {T : } {J : Type u} [] :
(T.mapCocone c).pt c.pt

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

Instances For
theorem CategoryTheory.Monad.ForgetCreatesColimits.commuting {C : Type u₁} [] {T : } {J : Type u} [] (j : J) :
CategoryTheory.CategoryStruct.comp (T.map (c.app j)) () = CategoryTheory.CategoryStruct.comp (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.

Instances For
@[simp]
theorem CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone_ι_app_f {C : Type u₁} [] {T : } {J : Type u} [] [CategoryTheory.Limits.PreservesColimit () T.toFunctor] (j : J) :
().f = c.app j

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

Instances For

(Impl) Prove that the lifted cocone is colimiting.

Instances For
noncomputable instance CategoryTheory.Monad.forgetCreatesColimit {C : Type u₁} [] {T : } {J : Type u} [] [CategoryTheory.Limits.PreservesColimit () T.toFunctor] :

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

noncomputable instance CategoryTheory.Monad.forgetCreatesColimitsOfShape {C : Type u₁} [] {T : } {J : Type u} [CategoryTheory.Limits.PreservesColimitsOfShape J T.toFunctor] :
noncomputable instance CategoryTheory.Monad.forgetCreatesColimits {C : Type u₁} [] {T : } [] :

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.

instance CategoryTheory.comp_comparison_hasLimit {C : Type u₁} [] {D : Type u₂} [] {J : Type u} (F : ) (R : ) :
noncomputable def CategoryTheory.monadicCreatesLimits {C : Type u₁} [] {D : Type u₂} [] (R : ) :

Instances For
noncomputable def CategoryTheory.monadicCreatesColimitOfPreservesColimit {C : Type u₁} [] {D : Type u₂} [] {J : Type u} (R : ) (K : ) :

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

Instances For
noncomputable def CategoryTheory.monadicCreatesColimitsOfShapeOfPreservesColimitsOfShape {C : Type u₁} [] {D : Type u₂} [] {J : Type u} (R : ) :

A monadic functor creates any colimits of shapes it preserves.

Instances For
noncomputable def CategoryTheory.monadicCreatesColimitsOfPreservesColimits {C : Type u₁} [] {D : Type u₂} [] (R : ) [] :

A monadic functor creates colimits if it preserves colimits.

Instances For
theorem CategoryTheory.hasLimit_of_reflective {C : Type u₁} [] {D : Type u₂} [] {J : Type u} (F : ) (R : ) :
theorem CategoryTheory.hasLimitsOfShape_of_reflective {C : Type u₁} [] {D : Type u₂} [] {J : Type u} (R : ) :

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

theorem CategoryTheory.hasLimits_of_reflective {C : Type u₁} [] {D : Type u₂} [] (R : ) [] :

If C has limits then any reflective subcategory has limits.

theorem CategoryTheory.hasColimitsOfShape_of_reflective {C : Type u₁} [] {D : Type u₂} [] {J : Type u} (R : ) :

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

theorem CategoryTheory.hasColimits_of_reflective {C : Type u₁} [] {D : Type u₂} [] (R : ) [] :

If C has colimits then any reflective subcategory has colimits.

noncomputable def CategoryTheory.leftAdjointPreservesTerminalOfReflective {C : Type u₁} [] {D : Type u₂} [] (R : ) :

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

Instances For