Limits and colimits in the category of (co)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.

Dually, this file shows that the forgetful functor forget T : Coalgebra T ⥤ C for a comonad T : C ⥤ C creates colimits and creates any limits which T preserves. This is used to show that Coalgebra T has any colimits which C has, and any limits which C has and T preserves. This is generalised to the case of a comonadic functor D ⥤ C.

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

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

@[simp]

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

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

(Impl) Prove that the lifted cone is limiting.

@[simp]

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

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

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

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

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

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.Monad.ForgetCreatesColimits.lambda {C : Type u₁} [Category.{v₁, u₁} C] {T : Monad C} {J : Type u} [Category.{v, u} J] {D : Functor J T.Algebra} (c : Limits.Cocone (D.comp T.forget)) (t : Limits.IsColimit c) [Limits.PreservesColimit (D.comp T.forget) 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₁} [Category.{v₁, u₁} C] {T : Monad C} {J : Type u} [Category.{v, u} J] {D : Functor J T.Algebra} (c : Limits.Cocone (D.comp T.forget)) (t : Limits.IsColimit c) [Limits.PreservesColimit (D.comp T.forget) T.toFunctor] (j : J) : CategoryStruct.comp (T.map (c.ι.app j)) (lambda c t) = CategoryStruct.comp (D.obj j).a (c.ι.app j)

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

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

(Impl) Prove that the lifted cocone is colimiting.

@[simp]

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

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

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

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

theorem CategoryTheory.Monad.forget_creates_colimits_of_monad_preserves {C : Type u₁} [Category.{v₁, u₁} C] {T : Monad C} {J : Type u} [Category.{v, u} J] [Limits.PreservesColimitsOfShape J T.toFunctor] (D : Functor J T.Algebra) [Limits.HasColimit (D.comp T.forget)] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type u} [Category.{v, u} J] (F : Functor J D) (R : Functor D C) [MonadicRightAdjoint R] [Limits.HasLimit (F.comp R)] : Limits.HasLimit ((F.comp (Monad.comparison (monadicAdjunction R))).comp (monadicAdjunction R).toMonad.forget)

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

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

Any monadic functor creates limits.

noncomputable def CategoryTheory.monadicCreatesColimitOfPreservesColimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type u} [Category.{v, u} J] (R : Functor D C) (K : Functor J D) [MonadicRightAdjoint R] [Limits.PreservesColimit (K.comp R) ((monadicLeftAdjoint R).comp R)] [Limits.PreservesColimit ((K.comp R).comp ((monadicLeftAdjoint R).comp R)) ((monadicLeftAdjoint R).comp R)] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type u} [Category.{v, u} J] (R : Functor D C) [MonadicRightAdjoint R] [Limits.PreservesColimitsOfShape J R] : CreatesColimitsOfShape J R

A monadic functor creates any colimits of shapes it preserves.

noncomputable def CategoryTheory.monadicCreatesColimitsOfPreservesColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (R : Functor D C) [MonadicRightAdjoint R] [Limits.PreservesColimitsOfSize.{v, u, v₂, v₁, u₂, u₁} R] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type u} [Category.{v, u} J] (F : Functor J D) (R : Functor D C) [Limits.HasLimit (F.comp R)] [Reflective R] : Limits.HasLimit F

theorem CategoryTheory.hasLimitsOfShape_of_reflective {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type u} [Category.{v, u} J] [Limits.HasLimitsOfShape J C] (R : Functor D C) [Reflective R] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (R : Functor D C) [Limits.HasLimitsOfSize.{v, u, v₁, u₁} C] [Reflective R] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type u} [Category.{v, u} J] (R : Functor D C) [Reflective R] [Limits.HasColimitsOfShape J C] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (R : Functor D C) [Reflective R] [Limits.HasColimitsOfSize.{v, u, v₁, u₁} C] : Limits.HasColimitsOfSize.{v, u, v₂, u₂} D

If C has colimits then any reflective subcategory has colimits.

theorem CategoryTheory.leftAdjoint_preservesTerminal_of_reflective {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (R : Functor D C) [Reflective R] : Limits.PreservesLimitsOfShape (Discrete PEmpty.{v + 1}) (monadicLeftAdjoint R)

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

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

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

@[simp]

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

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

(Impl) This new cocone is used to construct the coalgebra structure

@[simp]

theorem CategoryTheory.Comonad.ForgetCreatesColimits'.newCocone_ι_app {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {T : Comonad C} (D : Functor J T.Coalgebra) (c : Limits.Cocone (D.comp T.forget)) (X : J) : (newCocone D c).ι.app X = CategoryStruct.comp (D.obj X).a (T.map (c.ι.app X))

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

The coalgebra structure which will be the point of the new colimit cone for D.

@[simp]

theorem CategoryTheory.Comonad.ForgetCreatesColimits'.coconePoint_a {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {T : Comonad C} (D : Functor J T.Coalgebra) (c : Limits.Cocone (D.comp T.forget)) (t : Limits.IsColimit c) : (coconePoint D c t).a = t.desc (newCocone D c)

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

(Impl) Prove that the lifted cocone is colimiting.

@[simp]

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

noncomputable instance CategoryTheory.Comonad.forgetCreatesColimit {C : Type u₁} [Category.{v₁, u₁} C] {T : Comonad C} : CreatesColimitsOfSize.{u_1, u_2, v₁, v₁, max u₁ v₁, u₁} T.forget

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

theorem CategoryTheory.Comonad.hasColimit_of_comp_forget_hasColimit {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {T : Comonad C} (D : Functor J T.Coalgebra) [Limits.HasColimit (D.comp T.forget)] : Limits.HasColimit D

If D ⋙ forget T has a colimit, then D has a colimit.

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

(Impl) The natural transformation given by the coalgebra structure maps, used to construct a cone c with point limit (D ⋙ forget T).

@[simp]

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

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

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

@[simp]

theorem CategoryTheory.Comonad.ForgetCreatesLimits'.newCone_pt {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {T : Comonad C} {D : Functor J T.Coalgebra} (c : Limits.Cone (D.comp T.forget)) : (newCone c).pt = c.pt

@[simp]

theorem CategoryTheory.Comonad.ForgetCreatesLimits'.newCone_π {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {T : Comonad C} {D : Functor J T.Coalgebra} (c : Limits.Cone (D.comp T.forget)) : (newCone c).π = CategoryStruct.comp c.π γ

@[reducible, inline]

noncomputable abbrev CategoryTheory.Comonad.ForgetCreatesLimits'.lambda {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {T : Comonad C} {D : Functor J T.Coalgebra} (c : Limits.Cone (D.comp T.forget)) (t : Limits.IsLimit c) [Limits.PreservesLimit (D.comp T.forget) T.toFunctor] : c.pt ⟶ (T.mapCone c).pt

(Impl) Define the map λ : L ⟶ TL, which will serve as the structure of the algebra on L, and we will show is the limiting object. We use the cone constructed by c and the fact that T preserves limits to produce this morphism.

theorem CategoryTheory.Comonad.ForgetCreatesLimits'.commuting {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {T : Comonad C} {D : Functor J T.Coalgebra} (c : Limits.Cone (D.comp T.forget)) (t : Limits.IsLimit c) [Limits.PreservesLimit (D.comp T.forget) T.toFunctor] (j : J) : CategoryStruct.comp (lambda c t) (T.map (c.π.app j)) = CategoryStruct.comp (c.π.app j) (D.obj j).a

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

noncomputable def CategoryTheory.Comonad.ForgetCreatesLimits'.conePoint {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {T : Comonad C} {D : Functor J T.Coalgebra} (c : Limits.Cone (D.comp T.forget)) (t : Limits.IsLimit c) [Limits.PreservesLimit (D.comp T.forget) T.toFunctor] [Limits.PreservesLimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] : T.Coalgebra

(Impl) Construct the limiting coalgebra from the map λ : L ⟶ TL given by lambda. We are required to show it satisfies the two coalgebra laws, which follow from the coalgebra laws for the image of D and our commuting lemma.

@[simp]

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

@[simp]

theorem CategoryTheory.Comonad.ForgetCreatesLimits'.conePoint_a {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {T : Comonad C} {D : Functor J T.Coalgebra} (c : Limits.Cone (D.comp T.forget)) (t : Limits.IsLimit c) [Limits.PreservesLimit (D.comp T.forget) T.toFunctor] [Limits.PreservesLimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] : (conePoint c t).a = lambda c t

noncomputable def CategoryTheory.Comonad.ForgetCreatesLimits'.liftedCone {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {T : Comonad C} {D : Functor J T.Coalgebra} (c : Limits.Cone (D.comp T.forget)) (t : Limits.IsLimit c) [Limits.PreservesLimit (D.comp T.forget) T.toFunctor] [Limits.PreservesLimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] : Limits.Cone D

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

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.Comonad.ForgetCreatesLimits'.liftedConeIsLimit {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {T : Comonad C} {D : Functor J T.Coalgebra} (c : Limits.Cone (D.comp T.forget)) (t : Limits.IsLimit c) [Limits.PreservesLimit (D.comp T.forget) T.toFunctor] [Limits.PreservesLimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] : Limits.IsLimit (liftedCone c t)

(Impl) Prove that the lifted cone is limiting.

@[simp]

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

noncomputable instance CategoryTheory.Comonad.forgetCreatesLimit {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {T : Comonad C} (D : Functor J T.Coalgebra) [Limits.PreservesLimit (D.comp T.forget) T.toFunctor] [Limits.PreservesLimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] : CreatesLimit D T.forget

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

noncomputable instance CategoryTheory.Comonad.forgetCreatesLimitsOfShape {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {T : Comonad C} [Limits.PreservesLimitsOfShape J T.toFunctor] : CreatesLimitsOfShape J T.forget

noncomputable instance CategoryTheory.Comonad.forgetCreatesLimits {C : Type u₁} [Category.{v₁, u₁} C] {T : Comonad C} [Limits.PreservesLimitsOfSize.{v, u, v₁, v₁, u₁, u₁} T.toFunctor] : CreatesLimitsOfSize.{v, u, v₁, v₁, max u₁ v₁, u₁} T.forget

theorem CategoryTheory.Comonad.forget_creates_limits_of_comonad_preserves {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {T : Comonad C} [Limits.PreservesLimitsOfShape J T.toFunctor] (D : Functor J T.Coalgebra) [Limits.HasLimit (D.comp T.forget)] : Limits.HasLimit D

For D : J ⥤ Coalgebra T, D ⋙ forget T has a limit, then D has a limit provided limits of shape J are preserved by T.

instance CategoryTheory.comp_comparison_forget_hasColimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type u} [Category.{v, u} J] (F : Functor J D) (R : Functor D C) [ComonadicLeftAdjoint R] [Limits.HasColimit (F.comp R)] : Limits.HasColimit ((F.comp (Comonad.comparison (comonadicAdjunction R))).comp (comonadicAdjunction R).toComonad.forget)

instance CategoryTheory.comp_comparison_hasColimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type u} [Category.{v, u} J] (F : Functor J D) (R : Functor D C) [ComonadicLeftAdjoint R] [Limits.HasColimit (F.comp R)] : Limits.HasColimit (F.comp (Comonad.comparison (comonadicAdjunction R)))

noncomputable def CategoryTheory.comonadicCreatesColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (R : Functor D C) [ComonadicLeftAdjoint R] : CreatesColimitsOfSize.{v, u, v₂, v₁, u₂, u₁} R

Any comonadic functor creates colimits.

noncomputable def CategoryTheory.comonadicCreatesLimitOfPreservesLimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type u} [Category.{v, u} J] (R : Functor D C) (K : Functor J D) [ComonadicLeftAdjoint R] [Limits.PreservesLimit (K.comp R) ((comonadicRightAdjoint R).comp R)] [Limits.PreservesLimit ((K.comp R).comp ((comonadicRightAdjoint R).comp R)) ((comonadicRightAdjoint R).comp R)] : CreatesLimit K R

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

noncomputable def CategoryTheory.comonadicCreatesLimitsOfShapeOfPreservesLimitsOfShape {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type u} [Category.{v, u} J] (R : Functor D C) [ComonadicLeftAdjoint R] [Limits.PreservesLimitsOfShape J R] : CreatesLimitsOfShape J R

A comonadic functor creates any limits of shapes it preserves.

noncomputable def CategoryTheory.comonadicCreatesLimitsOfPreservesLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (R : Functor D C) [ComonadicLeftAdjoint R] [Limits.PreservesLimitsOfSize.{v, u, v₂, v₁, u₂, u₁} R] : CreatesLimitsOfSize.{v, u, v₂, v₁, u₂, u₁} R

A comonadic functor creates limits if it preserves limits.

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

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

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

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

If C has colimits then any coreflective subcategory has colimits.

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

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

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

If C has limits then any coreflective subcategory has limits.

theorem CategoryTheory.rightAdjoint_preservesInitial_of_coreflective {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (R : Functor D C) [Coreflective R] : Limits.PreservesColimitsOfShape (Discrete PEmpty.{v + 1}) (comonadicRightAdjoint R)

The coreflector always preserves initial objects. Note this in general doesn't apply to any other colimit.