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₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] (D : CategoryTheory.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

Equations

• CategoryTheory.Monad.ForgetCreatesLimits.γ D = { app := fun (j : J) => (D.obj j).a, naturality := ⋯ }

@[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 T.Algebra) (j : J) : (CategoryTheory.Monad.ForgetCreatesLimits.γ D).app j = (D.obj j).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 T.Algebra) (c : CategoryTheory.Limits.Cone (D.comp T.forget)) : CategoryTheory.Limits.Cone (D.comp T.forget)

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

Equations

• One or more equations did not get rendered due to their size.

@[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 T.Algebra) (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (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.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 T.Algebra) (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c) : T.Algebra

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

Equations

• CategoryTheory.Monad.ForgetCreatesLimits.conePoint D c t = { A := c.pt, a := t.lift (CategoryTheory.Monad.ForgetCreatesLimits.newCone D c), unit := ⋯, assoc := ⋯ }

@[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 T.Algebra) (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c) : (CategoryTheory.Monad.ForgetCreatesLimits.conePoint D c t).a = t.lift (CategoryTheory.Monad.ForgetCreatesLimits.newCone D c)

@[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 T.Algebra) (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c) : (CategoryTheory.Monad.ForgetCreatesLimits.conePoint D c t).A = c.pt

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 T.Algebra) (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.Cone D

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

Equations

• One or more equations did not get rendered due to their size.

@[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 T.Algebra) (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c) (j : J) : ((CategoryTheory.Monad.ForgetCreatesLimits.liftedCone D c t).π.app j).f = c.π.app j

@[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 T.Algebra) (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c) : (CategoryTheory.Monad.ForgetCreatesLimits.liftedCone D c t).pt = CategoryTheory.Monad.ForgetCreatesLimits.conePoint D c t

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 T.Algebra) (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.IsLimit (CategoryTheory.Monad.ForgetCreatesLimits.liftedCone D c t)

(Impl) Prove that the lifted cone is limiting.

Equations

• CategoryTheory.Monad.ForgetCreatesLimits.liftedConeIsLimit D c t = { lift := fun (s : CategoryTheory.Limits.Cone D) => { f := t.lift (T.forget.mapCone s), h := ⋯ }, fac := ⋯, uniq := ⋯ }

@[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 T.Algebra) (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cone D) : ((CategoryTheory.Monad.ForgetCreatesLimits.liftedConeIsLimit D c t).lift s).f = t.lift (T.forget.mapCone s)

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₁} T.forget

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

Equations

• One or more equations did not get rendered due to their size.

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 T.Algebra) [CategoryTheory.Limits.HasLimit (D.comp T.forget)] : CategoryTheory.Limits.HasLimit D

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

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

Equations

• CategoryTheory.Monad.ForgetCreatesColimits.γ = { app := fun (j : J) => (D.obj j).a, naturality := ⋯ }

@[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 T.Algebra} (j : J) : CategoryTheory.Monad.ForgetCreatesColimits.γ.app j = (D.obj j).a

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 T.Algebra} (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) : CategoryTheory.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.

Equations

• CategoryTheory.Monad.ForgetCreatesColimits.newCocone c = { pt := c.pt, ι := 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 T.Algebra} (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) : (CategoryTheory.Monad.ForgetCreatesColimits.newCocone c).pt = c.pt

@[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 T.Algebra} (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) : (CategoryTheory.Monad.ForgetCreatesColimits.newCocone c).ι = CategoryTheory.CategoryStruct.comp CategoryTheory.Monad.ForgetCreatesColimits.γ c.ι

@[reducible, inline]

noncomputable abbrev 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 T.Algebra} (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.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.

Equations

• CategoryTheory.Monad.ForgetCreatesColimits.lambda c t = (CategoryTheory.Limits.isColimitOfPreserves T.toFunctor t).desc (CategoryTheory.Monad.ForgetCreatesColimits.newCocone c)

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 T.Algebra} (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (D.comp T.forget) 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.

noncomputable 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 T.Algebra} (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] [CategoryTheory.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.

Equations

• CategoryTheory.Monad.ForgetCreatesColimits.coconePoint c t = { A := c.pt, a := CategoryTheory.Monad.ForgetCreatesColimits.lambda c t, unit := ⋯, assoc := ⋯ }

@[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 T.Algebra} (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] [CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] : (CategoryTheory.Monad.ForgetCreatesColimits.coconePoint c t).a = CategoryTheory.Monad.ForgetCreatesColimits.lambda c t

@[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 T.Algebra} (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] [CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] : (CategoryTheory.Monad.ForgetCreatesColimits.coconePoint c t).A = c.pt

noncomputable 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 T.Algebra} (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] [CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] : CategoryTheory.Limits.Cocone D

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

Equations

• One or more equations did not get rendered due to their size.

@[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 T.Algebra} (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] [CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] : (CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone c t).pt = CategoryTheory.Monad.ForgetCreatesColimits.coconePoint c t

@[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 T.Algebra} (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] [CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] (j : J) : ((CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone c t).ι.app j).f = c.ι.app j

noncomputable 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 T.Algebra} (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] [CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] : CategoryTheory.Limits.IsColimit (CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone c t)

(Impl) Prove that the lifted cocone is colimiting.

Equations

• One or more equations did not get rendered due to their size.

@[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 T.Algebra} (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] [CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] (s : CategoryTheory.Limits.Cocone D) : ((CategoryTheory.Monad.ForgetCreatesColimits.liftedCoconeIsColimit c t).desc s).f = t.desc (T.forget.mapCocone s)

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 T.Algebra) [CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] [CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] : CategoryTheory.CreatesColimit D T.forget

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

Equations

• One or more equations did not get rendered due to their size.

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 T.forget

Equations

• CategoryTheory.Monad.forgetCreatesColimitsOfShape = { CreatesColimit := fun {K : CategoryTheory.Functor J T.Algebra} => inferInstance }

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₁} T.forget

Equations

• CategoryTheory.Monad.forgetCreatesColimits = { CreatesColimitsOfShape := fun {J : Type ?u.34} [CategoryTheory.Category.{?u.35, ?u.34} J] => inferInstance }

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 T.Algebra) [CategoryTheory.Limits.HasColimit (D.comp T.forget)] : 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 (F.comp R)] : CategoryTheory.Limits.HasLimit ((F.comp (CategoryTheory.Monad.comparison (CategoryTheory.monadicAdjunction R))).comp (CategoryTheory.monadicAdjunction R).toMonad.forget)

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 (F.comp R)] : CategoryTheory.Limits.HasLimit (F.comp (CategoryTheory.Monad.comparison (CategoryTheory.monadicAdjunction 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.

Equations

• CategoryTheory.monadicCreatesLimits R = CategoryTheory.createsLimitsOfNatIso (CategoryTheory.Monad.comparisonForget (CategoryTheory.monadicAdjunction R))

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 (K.comp R) ((CategoryTheory.monadicLeftAdjoint R).comp R)] [CategoryTheory.Limits.PreservesColimit ((K.comp R).comp ((CategoryTheory.monadicLeftAdjoint R).comp R)) ((CategoryTheory.monadicLeftAdjoint R).comp R)] : CategoryTheory.CreatesColimit K R

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

Equations

• CategoryTheory.monadicCreatesColimitOfPreservesColimit R K = CategoryTheory.createsColimitOfNatIso (CategoryTheory.Monad.comparisonForget (CategoryTheory.monadicAdjunction R))

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

theorem CategoryTheory.leftAdjoint_preservesTerminal_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.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{v + 1}) (CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {T : CategoryTheory.Comonad C} (D : CategoryTheory.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

Equations

• CategoryTheory.Comonad.ForgetCreatesColimits'.γ D = { app := fun (j : J) => (D.obj j).a, naturality := ⋯ }

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

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

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

Equations

• CategoryTheory.Comonad.ForgetCreatesColimits'.coconePoint D c t = { A := c.pt, a := t.desc (CategoryTheory.Comonad.ForgetCreatesColimits'.newCocone D c), counit := ⋯, coassoc := ⋯ }

@[simp]

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

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

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

(Impl) Prove that the lifted cocone is colimiting.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

def CategoryTheory.Comonad.ForgetCreatesLimits'.γ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {T : CategoryTheory.Comonad C} {D : CategoryTheory.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).

Equations

• CategoryTheory.Comonad.ForgetCreatesLimits'.γ = { app := fun (j : J) => (D.obj j).a, naturality := ⋯ }

@[simp]

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

def CategoryTheory.Comonad.ForgetCreatesLimits'.newCone {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {T : CategoryTheory.Comonad C} {D : CategoryTheory.Functor J T.Coalgebra} (c : CategoryTheory.Limits.Cone (D.comp T.forget)) : CategoryTheory.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.

Equations

• CategoryTheory.Comonad.ForgetCreatesLimits'.newCone c = { pt := c.pt, π := CategoryTheory.CategoryStruct.comp c.π CategoryTheory.Comonad.ForgetCreatesLimits'.γ }

@[simp]

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

@[simp]

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.Comonad.ForgetCreatesLimits'.lambda {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {T : CategoryTheory.Comonad C} {D : CategoryTheory.Functor J T.Coalgebra} (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c) [CategoryTheory.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.

Equations

• CategoryTheory.Comonad.ForgetCreatesLimits'.lambda c t = (CategoryTheory.Limits.isLimitOfPreserves T.toFunctor t).lift (CategoryTheory.Comonad.ForgetCreatesLimits'.newCone c)

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

Equations

• CategoryTheory.Comonad.ForgetCreatesLimits'.conePoint c t = { A := c.pt, a := CategoryTheory.Comonad.ForgetCreatesLimits'.lambda c t, counit := ⋯, coassoc := ⋯ }

@[simp]

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

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

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

(Impl) Prove that the lifted cone is limiting.

Equations

• CategoryTheory.Comonad.ForgetCreatesLimits'.liftedConeIsLimit c t = { lift := fun (s : CategoryTheory.Limits.Cone D) => { f := t.lift (T.forget.mapCone s), h := ⋯ }, fac := ⋯, uniq := ⋯ }

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• CategoryTheory.Comonad.forgetCreatesLimitsOfShape = { CreatesLimit := fun {K : CategoryTheory.Functor J T.Coalgebra} => inferInstance }

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

Equations

• CategoryTheory.Comonad.forgetCreatesLimits = { CreatesLimitsOfShape := fun {J : Type ?u.34} [CategoryTheory.Category.{?u.35, ?u.34} J] => inferInstance }

theorem CategoryTheory.Comonad.forget_creates_limits_of_comonad_preserves {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {T : CategoryTheory.Comonad C} [CategoryTheory.Limits.PreservesLimitsOfShape J T.toFunctor] (D : CategoryTheory.Functor J T.Coalgebra) [CategoryTheory.Limits.HasLimit (D.comp T.forget)] : CategoryTheory.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₁} [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.ComonadicLeftAdjoint R] [CategoryTheory.Limits.HasColimit (F.comp R)] : CategoryTheory.Limits.HasColimit ((F.comp (CategoryTheory.Comonad.comparison (CategoryTheory.comonadicAdjunction R))).comp (CategoryTheory.comonadicAdjunction R).toComonad.forget)

instance CategoryTheory.comp_comparison_hasColimit {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.ComonadicLeftAdjoint R] [CategoryTheory.Limits.HasColimit (F.comp R)] : CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.Comonad.comparison (CategoryTheory.comonadicAdjunction R)))

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

Any comonadic functor creates colimits.

Equations

• CategoryTheory.comonadicCreatesColimits R = CategoryTheory.createsColimitsOfNatIso (CategoryTheory.Comonad.comparisonForget (CategoryTheory.comonadicAdjunction R))

noncomputable def CategoryTheory.comonadicCreatesLimitOfPreservesLimit {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.ComonadicLeftAdjoint R] [CategoryTheory.Limits.PreservesLimit (K.comp R) ((CategoryTheory.comonadicRightAdjoint R).comp R)] [CategoryTheory.Limits.PreservesLimit ((K.comp R).comp ((CategoryTheory.comonadicRightAdjoint R).comp R)) ((CategoryTheory.comonadicRightAdjoint R).comp R)] : CategoryTheory.CreatesLimit K R

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

Equations

• CategoryTheory.comonadicCreatesLimitOfPreservesLimit R K = CategoryTheory.createsLimitOfNatIso (CategoryTheory.Comonad.comparisonForget (CategoryTheory.comonadicAdjunction R))

noncomputable def CategoryTheory.comonadicCreatesLimitsOfShapeOfPreservesLimitsOfShape {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.ComonadicLeftAdjoint R] [CategoryTheory.Limits.PreservesLimitsOfShape J R] : CategoryTheory.CreatesLimitsOfShape J R

A comonadic functor creates any limits of shapes it preserves.

Equations

• CategoryTheory.comonadicCreatesLimitsOfShapeOfPreservesLimitsOfShape R = { CreatesLimit := fun {K : CategoryTheory.Functor J D} => CategoryTheory.comonadicCreatesLimitOfPreservesLimit R K }

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

A comonadic functor creates limits if it preserves limits.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.hasColimit_of_coreflective {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.HasColimit (F.comp R)] [CategoryTheory.Coreflective R] : CategoryTheory.Limits.HasColimit F

theorem CategoryTheory.hasColimitsOfShape_of_coreflective {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.HasColimitsOfShape J C] (R : CategoryTheory.Functor D C) [CategoryTheory.Coreflective R] : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (R : CategoryTheory.Functor D C) [CategoryTheory.Limits.HasColimitsOfSize.{v, u, v₁, u₁} C] [CategoryTheory.Coreflective R] : CategoryTheory.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₁} [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.Coreflective R] [CategoryTheory.Limits.HasLimitsOfShape J C] : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (R : CategoryTheory.Functor D C) [CategoryTheory.Coreflective R] [CategoryTheory.Limits.HasLimitsOfSize.{v, u, v₁, u₁} C] : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (R : CategoryTheory.Functor D C) [CategoryTheory.Coreflective R] : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{v + 1}) (CategoryTheory.comonadicRightAdjoint R)

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