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

Dualise for the category of coalgebras and comonadic left adjoints.

@[simp]

theorem CategoryTheory.Monad.ForgetCreatesLimits.γ_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J (CategoryTheory.Monad.Algebra T)) (j : J) : (CategoryTheory.Monad.ForgetCreatesLimits.γ D).app j = (D.obj j).a

def CategoryTheory.Monad.ForgetCreatesLimits.γ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J (CategoryTheory.Monad.Algebra T)) : CategoryTheory.Functor.comp D (CategoryTheory.Functor.comp (CategoryTheory.Monad.forget T) T.toFunctor) ⟶ CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T)

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

@[simp]

theorem CategoryTheory.Monad.ForgetCreatesLimits.newCone_π_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J (CategoryTheory.Monad.Algebra T)) (c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T))) (X : J) : (CategoryTheory.Monad.ForgetCreatesLimits.newCone D c).π.app X = CategoryTheory.CategoryStruct.comp (T.map (c.π.app X)) (D.obj X).a

def CategoryTheory.Monad.ForgetCreatesLimits.newCone {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J (CategoryTheory.Monad.Algebra T)) (c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T))) : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T))

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

@[simp]

theorem CategoryTheory.Monad.ForgetCreatesLimits.conePoint_A {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J (CategoryTheory.Monad.Algebra T)) (c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T))) (t : CategoryTheory.Limits.IsLimit c) : (CategoryTheory.Monad.ForgetCreatesLimits.conePoint D c t).A = c.pt

@[simp]

theorem CategoryTheory.Monad.ForgetCreatesLimits.conePoint_a {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J (CategoryTheory.Monad.Algebra T)) (c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T))) (t : CategoryTheory.Limits.IsLimit c) : (CategoryTheory.Monad.ForgetCreatesLimits.conePoint D c t).a = CategoryTheory.Limits.IsLimit.lift t (CategoryTheory.Monad.ForgetCreatesLimits.newCone D c)

def CategoryTheory.Monad.ForgetCreatesLimits.conePoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J (CategoryTheory.Monad.Algebra T)) (c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T))) (t : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Monad.Algebra T

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

@[simp]

theorem CategoryTheory.Monad.ForgetCreatesLimits.liftedCone_pt {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J (CategoryTheory.Monad.Algebra T)) (c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T))) (t : CategoryTheory.Limits.IsLimit c) : (CategoryTheory.Monad.ForgetCreatesLimits.liftedCone D c t).pt = CategoryTheory.Monad.ForgetCreatesLimits.conePoint D c t

@[simp]

theorem CategoryTheory.Monad.ForgetCreatesLimits.liftedCone_π_app_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J (CategoryTheory.Monad.Algebra T)) (c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T))) (t : CategoryTheory.Limits.IsLimit c) (j : J) : ((CategoryTheory.Monad.ForgetCreatesLimits.liftedCone D c t).π.app j).f = c.π.app j

def CategoryTheory.Monad.ForgetCreatesLimits.liftedCone {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J (CategoryTheory.Monad.Algebra T)) (c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T))) (t : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.Cone D

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

@[simp]

theorem CategoryTheory.Monad.ForgetCreatesLimits.liftedConeIsLimit_lift_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J (CategoryTheory.Monad.Algebra T)) (c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T))) (t : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cone D) : (CategoryTheory.Limits.IsLimit.lift (CategoryTheory.Monad.ForgetCreatesLimits.liftedConeIsLimit D c t) s).f = CategoryTheory.Limits.IsLimit.lift t ((CategoryTheory.Monad.forget T).mapCone s)

def CategoryTheory.Monad.ForgetCreatesLimits.liftedConeIsLimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J (CategoryTheory.Monad.Algebra T)) (c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T))) (t : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.IsLimit (CategoryTheory.Monad.ForgetCreatesLimits.liftedCone D c t)

(Impl) Prove that the lifted cone is limiting.

noncomputable instance CategoryTheory.Monad.forgetCreatesLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} : CategoryTheory.CreatesLimitsOfSize.{u_1, u_2, v₁, v₁, max u₁ v₁, u₁} (CategoryTheory.Monad.forget T)

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

theorem CategoryTheory.Monad.hasLimit_of_comp_forget_hasLimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J (CategoryTheory.Monad.Algebra T)) [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T))] : CategoryTheory.Limits.HasLimit D

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

@[simp]

theorem CategoryTheory.Monad.ForgetCreatesColimits.γ_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J (CategoryTheory.Monad.Algebra T)} (j : J) : CategoryTheory.Monad.ForgetCreatesColimits.γ.app j = (D.obj j).a

def CategoryTheory.Monad.ForgetCreatesColimits.γ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J (CategoryTheory.Monad.Algebra T)} : CategoryTheory.Functor.comp (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T)) T.toFunctor ⟶ CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T)

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

@[simp]

theorem CategoryTheory.Monad.ForgetCreatesColimits.newCocone_ι {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J (CategoryTheory.Monad.Algebra T)} (c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T))) : (CategoryTheory.Monad.ForgetCreatesColimits.newCocone c).ι = CategoryTheory.CategoryStruct.comp CategoryTheory.Monad.ForgetCreatesColimits.γ c.ι

@[simp]

theorem CategoryTheory.Monad.ForgetCreatesColimits.newCocone_pt {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J (CategoryTheory.Monad.Algebra T)} (c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T))) : (CategoryTheory.Monad.ForgetCreatesColimits.newCocone c).pt = c.pt

def CategoryTheory.Monad.ForgetCreatesColimits.newCocone {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J (CategoryTheory.Monad.Algebra T)} (c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T))) : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T)) T.toFunctor)

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

@[reducible]

def CategoryTheory.Monad.ForgetCreatesColimits.lambda {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J (CategoryTheory.Monad.Algebra T)} (c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T))) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T)) T.toFunctor] : (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.

theorem CategoryTheory.Monad.ForgetCreatesColimits.commuting {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J (CategoryTheory.Monad.Algebra T)} (c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T))) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T)) T.toFunctor] (j : J) : CategoryTheory.CategoryStruct.comp (T.map (c.ι.app j)) (CategoryTheory.Monad.ForgetCreatesColimits.lambda c t) = CategoryTheory.CategoryStruct.comp (D.obj j).a (c.ι.app j)

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

@[simp]

theorem CategoryTheory.Monad.ForgetCreatesColimits.coconePoint_A {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J (CategoryTheory.Monad.Algebra T)} (c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T))) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T)) T.toFunctor] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T)) T.toFunctor) T.toFunctor] : (CategoryTheory.Monad.ForgetCreatesColimits.coconePoint c t).A = c.pt

@[simp]

theorem CategoryTheory.Monad.ForgetCreatesColimits.coconePoint_a {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J (CategoryTheory.Monad.Algebra T)} (c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T))) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T)) T.toFunctor] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T)) T.toFunctor) T.toFunctor] : (CategoryTheory.Monad.ForgetCreatesColimits.coconePoint c t).a = CategoryTheory.Monad.ForgetCreatesColimits.lambda c t

def CategoryTheory.Monad.ForgetCreatesColimits.coconePoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J (CategoryTheory.Monad.Algebra T)} (c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T))) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T)) T.toFunctor] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T)) T.toFunctor) T.toFunctor] : CategoryTheory.Monad.Algebra T

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

@[simp]

theorem CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone_ι_app_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J (CategoryTheory.Monad.Algebra T)} (c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T))) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T)) T.toFunctor] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T)) T.toFunctor) T.toFunctor] (j : J) : ((CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone c t).ι.app j).f = c.ι.app j

@[simp]

theorem CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone_pt {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J (CategoryTheory.Monad.Algebra T)} (c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T))) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T)) T.toFunctor] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T)) T.toFunctor) T.toFunctor] : (CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone c t).pt = CategoryTheory.Monad.ForgetCreatesColimits.coconePoint c t

def CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J (CategoryTheory.Monad.Algebra T)} (c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T))) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T)) T.toFunctor] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T)) T.toFunctor) T.toFunctor] : CategoryTheory.Limits.Cocone D

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

@[simp]

theorem CategoryTheory.Monad.ForgetCreatesColimits.liftedCoconeIsColimit_desc_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J (CategoryTheory.Monad.Algebra T)} (c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T))) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T)) T.toFunctor] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T)) T.toFunctor) T.toFunctor] (s : CategoryTheory.Limits.Cocone D) : (CategoryTheory.Limits.IsColimit.desc (CategoryTheory.Monad.ForgetCreatesColimits.liftedCoconeIsColimit c t) s).f = CategoryTheory.Limits.IsColimit.desc t ((CategoryTheory.Monad.forget T).mapCocone s)

def CategoryTheory.Monad.ForgetCreatesColimits.liftedCoconeIsColimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J (CategoryTheory.Monad.Algebra T)} (c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T))) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T)) T.toFunctor] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T)) T.toFunctor) T.toFunctor] : CategoryTheory.Limits.IsColimit (CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone c t)

(Impl) Prove that the lifted cocone is colimiting.

noncomputable instance CategoryTheory.Monad.forgetCreatesColimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J (CategoryTheory.Monad.Algebra T)) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T)) T.toFunctor] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T)) T.toFunctor) T.toFunctor] : CategoryTheory.CreatesColimit D (CategoryTheory.Monad.forget T)

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₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.PreservesColimitsOfShape J T.toFunctor] : CategoryTheory.CreatesColimitsOfShape J (CategoryTheory.Monad.forget T)

noncomputable instance CategoryTheory.Monad.forgetCreatesColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} [CategoryTheory.Limits.PreservesColimitsOfSize.{v, u, v₁, v₁, u₁, u₁} T.toFunctor] : CategoryTheory.CreatesColimitsOfSize.{v, u, v₁, v₁, max u₁ v₁, u₁} (CategoryTheory.Monad.forget T)

theorem CategoryTheory.Monad.forget_creates_colimits_of_monad_preserves {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.PreservesColimitsOfShape J T.toFunctor] (D : CategoryTheory.Functor J (CategoryTheory.Monad.Algebra T)) [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp D (CategoryTheory.Monad.forget T))] : CategoryTheory.Limits.HasColimit D

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_forget_hasLimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J D) (R : CategoryTheory.Functor D C) [CategoryTheory.MonadicRightAdjoint R] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F R)] : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.Monad.comparison (CategoryTheory.Adjunction.ofRightAdjoint R))) (CategoryTheory.Monad.forget (CategoryTheory.Adjunction.toMonad (CategoryTheory.Adjunction.ofRightAdjoint R))))

instance CategoryTheory.comp_comparison_hasLimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J D) (R : CategoryTheory.Functor D C) [CategoryTheory.MonadicRightAdjoint R] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F R)] : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F (CategoryTheory.Monad.comparison (CategoryTheory.Adjunction.ofRightAdjoint R)))

noncomputable def CategoryTheory.monadicCreatesLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (R : CategoryTheory.Functor D C) [CategoryTheory.MonadicRightAdjoint R] : CategoryTheory.CreatesLimitsOfSize.{v, u, v₂, v₁, u₂, u₁} R

Any monadic functor creates limits.

noncomputable def CategoryTheory.monadicCreatesColimitOfPreservesColimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type u} [CategoryTheory.Category.{v, u} J] (R : CategoryTheory.Functor D C) (K : CategoryTheory.Functor J D) [CategoryTheory.MonadicRightAdjoint R] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp K R) (CategoryTheory.Functor.comp (CategoryTheory.leftAdjoint R) R)] [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp K R) (CategoryTheory.Functor.comp (CategoryTheory.leftAdjoint R) R)) (CategoryTheory.Functor.comp (CategoryTheory.leftAdjoint R) R)] : CategoryTheory.CreatesColimit K R

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

noncomputable def CategoryTheory.monadicCreatesColimitsOfShapeOfPreservesColimitsOfShape {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type u} [CategoryTheory.Category.{v, u} J] (R : CategoryTheory.Functor D C) [CategoryTheory.MonadicRightAdjoint R] [CategoryTheory.Limits.PreservesColimitsOfShape J R] : CategoryTheory.CreatesColimitsOfShape J R

A monadic functor creates any colimits of shapes it preserves.

noncomputable def CategoryTheory.monadicCreatesColimitsOfPreservesColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (R : CategoryTheory.Functor D C) [CategoryTheory.MonadicRightAdjoint R] [CategoryTheory.Limits.PreservesColimitsOfSize.{v, u, v₂, v₁, u₂, u₁} R] : CategoryTheory.CreatesColimitsOfSize.{v, u, v₂, v₁, u₂, u₁} R

A monadic functor creates colimits if it preserves colimits.

theorem CategoryTheory.hasLimit_of_reflective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J D) (R : CategoryTheory.Functor D C) [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F R)] [CategoryTheory.Reflective R] : CategoryTheory.Limits.HasLimit F

theorem CategoryTheory.hasLimitsOfShape_of_reflective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type u} [CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.HasLimitsOfShape J C] (R : CategoryTheory.Functor D C) [CategoryTheory.Reflective R] : CategoryTheory.Limits.HasLimitsOfShape J D

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

theorem CategoryTheory.hasLimits_of_reflective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (R : CategoryTheory.Functor D C) [CategoryTheory.Limits.HasLimitsOfSize.{v, u, v₁, u₁} C] [CategoryTheory.Reflective R] : CategoryTheory.Limits.HasLimitsOfSize.{v, u, v₂, u₂} D

If C has limits then any reflective subcategory has limits.

theorem CategoryTheory.hasColimitsOfShape_of_reflective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type u} [CategoryTheory.Category.{v, u} J] (R : CategoryTheory.Functor D C) [CategoryTheory.Reflective R] [CategoryTheory.Limits.HasColimitsOfShape J C] : CategoryTheory.Limits.HasColimitsOfShape J D

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

theorem CategoryTheory.hasColimits_of_reflective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (R : CategoryTheory.Functor D C) [CategoryTheory.Reflective R] [CategoryTheory.Limits.HasColimitsOfSize.{v, u, v₁, u₁} C] : CategoryTheory.Limits.HasColimitsOfSize.{v, u, v₂, u₂} D

If C has colimits then any reflective subcategory has colimits.

noncomputable def CategoryTheory.leftAdjointPreservesTerminalOfReflective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (R : CategoryTheory.Functor D C) [CategoryTheory.Reflective R] : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{v + 1} ) (CategoryTheory.leftAdjoint R)

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