@[simp]
theorem
category_theory.monad.forget_creates_limits.γ_app
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T]
{J : Type v₁}
[category_theory.small_category J]
(D : J ⥤ category_theory.monad.algebra T)
(j : J) :
(category_theory.monad.forget_creates_limits.γ D).app j = (D.obj j).a
def
category_theory.monad.forget_creates_limits.γ
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T]
{J : Type v₁}
[category_theory.small_category J]
(D : J ⥤ category_theory.monad.algebra T) :
D ⋙ category_theory.monad.forget T ⋙ T ⟶ D ⋙ category_theory.monad.forget T
(Impl) The natural transformation used to define the new cone
Equations
- category_theory.monad.forget_creates_limits.γ D = {app := λ (j : J), (D.obj j).a, naturality' := _}
def
category_theory.monad.forget_creates_limits.new_cone
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T]
{J : Type v₁}
[category_theory.small_category J]
(D : J ⥤ category_theory.monad.algebra T) :
(Impl) This new cone is used to construct the algebra structure
Equations
@[simp]
theorem
category_theory.monad.forget_creates_limits.new_cone_X
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T]
{J : Type v₁}
[category_theory.small_category J]
(D : J ⥤ category_theory.monad.algebra T)
(c : category_theory.limits.cone (D ⋙ category_theory.monad.forget T)) :
@[simp]
theorem
category_theory.monad.forget_creates_limits.new_cone_π
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T]
{J : Type v₁}
[category_theory.small_category J]
(D : J ⥤ category_theory.monad.algebra T)
(c : category_theory.limits.cone (D ⋙ category_theory.monad.forget T)) :
@[simp]
theorem
category_theory.monad.forget_creates_limits.cone_point_A
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T]
{J : Type v₁}
[category_theory.small_category J]
(D : J ⥤ category_theory.monad.algebra T)
(c : category_theory.limits.cone (D ⋙ category_theory.monad.forget T))
(t : category_theory.limits.is_limit c) :
def
category_theory.monad.forget_creates_limits.cone_point
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T]
{J : Type v₁}
[category_theory.small_category J]
(D : J ⥤ category_theory.monad.algebra T)
(c : category_theory.limits.cone (D ⋙ category_theory.monad.forget T)) :
The algebra structure which will be the apex of the new limit cone for D.
Equations
- category_theory.monad.forget_creates_limits.cone_point D c t = {A := c.X, a := t.lift (category_theory.monad.forget_creates_limits.new_cone D c), unit' := _, assoc' := _}
@[simp]
theorem
category_theory.monad.forget_creates_limits.cone_point_a
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T]
{J : Type v₁}
[category_theory.small_category J]
(D : J ⥤ category_theory.monad.algebra T)
(c : category_theory.limits.cone (D ⋙ category_theory.monad.forget T))
(t : category_theory.limits.is_limit c) :
def
category_theory.monad.forget_creates_limits.lifted_cone
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T]
{J : Type v₁}
[category_theory.small_category J]
(D : J ⥤ category_theory.monad.algebra T)
(c : category_theory.limits.cone (D ⋙ category_theory.monad.forget T)) :
(Impl) Construct the lifted cone in algebra T which will be limiting.
Equations
- category_theory.monad.forget_creates_limits.lifted_cone D c t = {X := category_theory.monad.forget_creates_limits.cone_point D c t, π := {app := λ (j : J), {f := c.π.app j, h' := _}, naturality' := _}}
@[simp]
theorem
category_theory.monad.forget_creates_limits.lifted_cone_π_app_f
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T]
{J : Type v₁}
[category_theory.small_category J]
(D : J ⥤ category_theory.monad.algebra T)
(c : category_theory.limits.cone (D ⋙ category_theory.monad.forget T))
(t : category_theory.limits.is_limit c)
(j : J) :
@[simp]
theorem
category_theory.monad.forget_creates_limits.lifted_cone_X
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T]
{J : Type v₁}
[category_theory.small_category J]
(D : J ⥤ category_theory.monad.algebra T)
(c : category_theory.limits.cone (D ⋙ category_theory.monad.forget T))
(t : category_theory.limits.is_limit c) :
@[simp]
theorem
category_theory.monad.forget_creates_limits.lifted_cone_is_limit_lift_f
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T]
{J : Type v₁}
[category_theory.small_category J]
(D : J ⥤ category_theory.monad.algebra T)
(c : category_theory.limits.cone (D ⋙ category_theory.monad.forget T))
(t : category_theory.limits.is_limit c)
(s : category_theory.limits.cone D) :
((category_theory.monad.forget_creates_limits.lifted_cone_is_limit D c t).lift s).f = t.lift ((category_theory.monad.forget T).map_cone s)
def
category_theory.monad.forget_creates_limits.lifted_cone_is_limit
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T]
{J : Type v₁}
[category_theory.small_category J]
(D : J ⥤ category_theory.monad.algebra T)
(c : category_theory.limits.cone (D ⋙ category_theory.monad.forget T))
(t : category_theory.limits.is_limit c) :
(Impl) Prove that the lifted cone is limiting.
Equations
- category_theory.monad.forget_creates_limits.lifted_cone_is_limit D c t = {lift := λ (s : category_theory.limits.cone D), {f := t.lift ((category_theory.monad.forget T).map_cone s), h' := _}, fac' := _, uniq' := _}
@[instance]
def
category_theory.monad.forget_creates_limits
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T] :
The forgetful functor from the Eilenberg-Moore category creates limits.
Equations
- category_theory.monad.forget_creates_limits = {creates_limits_of_shape := λ (J : Type v₁) (𝒥 : category_theory.small_category J), {creates_limit := λ (D : J ⥤ category_theory.monad.algebra T), category_theory.creates_limit_of_reflects_iso (λ (c : category_theory.limits.cone (D ⋙ category_theory.monad.forget T)) (t : category_theory.limits.is_limit c), {to_liftable_cone := {lifted_cone := category_theory.monad.forget_creates_limits.lifted_cone D c t, valid_lift := category_theory.limits.cones.ext (category_theory.iso.refl ((category_theory.monad.forget T).map_cone (category_theory.monad.forget_creates_limits.lifted_cone D c t)).X) _}, makes_limit := category_theory.monad.forget_creates_limits.lifted_cone_is_limit D c t})}}
def
category_theory.monad.has_limit_of_comp_forget_has_limit
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T]
{J : Type v₁}
[category_theory.small_category J]
(D : J ⥤ category_theory.monad.algebra T)
[category_theory.limits.has_limit (D ⋙ category_theory.monad.forget T)] :
D ⋙ forget T has a limit, then D has a limit.
def
category_theory.monad.forget_creates_colimits.γ
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T]
{J : Type v₁}
[category_theory.small_category J]
{D : J ⥤ category_theory.monad.algebra T} :
(D ⋙ category_theory.monad.forget T) ⋙ T ⟶ D ⋙ category_theory.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).
Equations
- category_theory.monad.forget_creates_colimits.γ = {app := λ (j : J), (D.obj j).a, naturality' := _}
@[simp]
theorem
category_theory.monad.forget_creates_colimits.γ_app
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T]
{J : Type v₁}
[category_theory.small_category J]
{D : J ⥤ category_theory.monad.algebra T}
(j : J) :
@[simp]
theorem
category_theory.monad.forget_creates_colimits.new_cocone_ι
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T]
{J : Type v₁}
[category_theory.small_category J]
{D : J ⥤ category_theory.monad.algebra T}
(c : category_theory.limits.cocone (D ⋙ category_theory.monad.forget T)) :
def
category_theory.monad.forget_creates_colimits.new_cocone
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T]
{J : Type v₁}
[category_theory.small_category J]
{D : J ⥤ category_theory.monad.algebra T} :
(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
@[simp]
theorem
category_theory.monad.forget_creates_colimits.new_cocone_X
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T]
{J : Type v₁}
[category_theory.small_category J]
{D : J ⥤ category_theory.monad.algebra T}
(c : category_theory.limits.cocone (D ⋙ category_theory.monad.forget T)) :
def
category_theory.monad.forget_creates_colimits.lambda
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T]
{J : Type v₁}
[category_theory.small_category J]
{D : J ⥤ category_theory.monad.algebra T}
(c : category_theory.limits.cocone (D ⋙ category_theory.monad.forget T))
(t : category_theory.limits.is_colimit c)
[category_theory.limits.preserves_colimits_of_shape J T] :
(T.map_cocone c).X ⟶ c.X
(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
category_theory.monad.forget_creates_colimits.commuting
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T]
{J : Type v₁}
[category_theory.small_category J]
{D : J ⥤ category_theory.monad.algebra T}
(c : category_theory.limits.cocone (D ⋙ category_theory.monad.forget T))
(t : category_theory.limits.is_colimit c)
[category_theory.limits.preserves_colimits_of_shape J T]
(j : J) :
(Impl) The key property defining the map λ : TL ⟶ L.
@[simp]
theorem
category_theory.monad.forget_creates_colimits.cocone_point_A
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T]
{J : Type v₁}
[category_theory.small_category J]
{D : J ⥤ category_theory.monad.algebra T}
(c : category_theory.limits.cocone (D ⋙ category_theory.monad.forget T))
(t : category_theory.limits.is_colimit c)
[category_theory.limits.preserves_colimits_of_shape J T] :
def
category_theory.monad.forget_creates_colimits.cocone_point
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T]
{J : Type v₁}
[category_theory.small_category J]
{D : J ⥤ category_theory.monad.algebra T}
(c : category_theory.limits.cocone (D ⋙ category_theory.monad.forget T))
(t : category_theory.limits.is_colimit c)
[category_theory.limits.preserves_colimits_of_shape J 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.
Equations
- category_theory.monad.forget_creates_colimits.cocone_point c t = {A := c.X, a := category_theory.monad.forget_creates_colimits.lambda c t _inst_4, unit' := _, assoc' := _}
@[simp]
theorem
category_theory.monad.forget_creates_colimits.cocone_point_a
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T]
{J : Type v₁}
[category_theory.small_category J]
{D : J ⥤ category_theory.monad.algebra T}
(c : category_theory.limits.cocone (D ⋙ category_theory.monad.forget T))
(t : category_theory.limits.is_colimit c)
[category_theory.limits.preserves_colimits_of_shape J T] :
@[simp]
theorem
category_theory.monad.forget_creates_colimits.lifted_cocone_X
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T]
{J : Type v₁}
[category_theory.small_category J]
{D : J ⥤ category_theory.monad.algebra T}
(c : category_theory.limits.cocone (D ⋙ category_theory.monad.forget T))
(t : category_theory.limits.is_colimit c)
[category_theory.limits.preserves_colimits_of_shape J T] :
def
category_theory.monad.forget_creates_colimits.lifted_cocone
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T]
{J : Type v₁}
[category_theory.small_category J]
{D : J ⥤ category_theory.monad.algebra T}
(c : category_theory.limits.cocone (D ⋙ category_theory.monad.forget T))
(t : category_theory.limits.is_colimit c)
[category_theory.limits.preserves_colimits_of_shape J T] :
(Impl) Construct the lifted cocone in algebra T which will be colimiting.
Equations
- category_theory.monad.forget_creates_colimits.lifted_cocone c t = {X := category_theory.monad.forget_creates_colimits.cocone_point c t _inst_4, ι := {app := λ (j : J), {f := c.ι.app j, h' := _}, naturality' := _}}
@[simp]
theorem
category_theory.monad.forget_creates_colimits.lifted_cocone_ι_app_f
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T]
{J : Type v₁}
[category_theory.small_category J]
{D : J ⥤ category_theory.monad.algebra T}
(c : category_theory.limits.cocone (D ⋙ category_theory.monad.forget T))
(t : category_theory.limits.is_colimit c)
[category_theory.limits.preserves_colimits_of_shape J T]
(j : J) :
@[simp]
theorem
category_theory.monad.forget_creates_colimits.lifted_cocone_is_colimit_desc_f
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T]
{J : Type v₁}
[category_theory.small_category J]
{D : J ⥤ category_theory.monad.algebra T}
(c : category_theory.limits.cocone (D ⋙ category_theory.monad.forget T))
(t : category_theory.limits.is_colimit c)
[category_theory.limits.preserves_colimits_of_shape J T]
(s : category_theory.limits.cocone D) :
def
category_theory.monad.forget_creates_colimits.lifted_cocone_is_colimit
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T]
{J : Type v₁}
[category_theory.small_category J]
{D : J ⥤ category_theory.monad.algebra T}
(c : category_theory.limits.cocone (D ⋙ category_theory.monad.forget T))
(t : category_theory.limits.is_colimit c)
[category_theory.limits.preserves_colimits_of_shape J T] :
(Impl) Prove that the lifted cocone is colimiting.
Equations
- category_theory.monad.forget_creates_colimits.lifted_cocone_is_colimit c t = {desc := λ (s : category_theory.limits.cocone D), {f := t.desc ((category_theory.monad.forget T).map_cocone s), h' := _}, fac' := _, uniq' := _}
@[instance]
def
category_theory.monad.forget_creates_colimits
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T]
{J : Type v₁}
[category_theory.small_category J]
[category_theory.limits.preserves_colimits_of_shape J T] :
The forgetful functor from the Eilenberg-Moore category for a monad creates any colimit which the monad itself preserves.
Equations
- category_theory.monad.forget_creates_colimits = {creates_colimit := λ (D : J ⥤ category_theory.monad.algebra T), category_theory.creates_colimit_of_reflects_iso (λ (c : category_theory.limits.cocone (D ⋙ category_theory.monad.forget T)) (t : category_theory.limits.is_colimit c), {to_liftable_cocone := {lifted_cocone := {X := category_theory.monad.forget_creates_colimits.cocone_point c t _inst_4, ι := {app := λ (j : J), {f := c.ι.app j, h' := _}, naturality' := _}}, valid_lift := category_theory.limits.cocones.ext (category_theory.iso.refl ((category_theory.monad.forget T).map_cocone {X := category_theory.monad.forget_creates_colimits.cocone_point c t _inst_4, ι := {app := λ (j : J), {f := c.ι.app j, h' := _}, naturality' := _}}).X) _}, makes_colimit := category_theory.monad.forget_creates_colimits.lifted_cocone_is_colimit c t _inst_4})}
def
category_theory.monad.forget_creates_colimits_of_monad_preserves
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T]
{J : Type v₁}
[category_theory.small_category J]
[category_theory.limits.preserves_colimits_of_shape J T]
(D : J ⥤ category_theory.monad.algebra T)
[category_theory.limits.has_colimit (D ⋙ category_theory.monad.forget T)] :
For D : J ⥤ algebra T, D ⋙ forget T has a colimit, then D has a colimit provided colimits
of shape J are preserved by T.
@[instance]
def
category_theory.comp_comparison_forget_has_limit
{C : Type u₁}
[category_theory.category C]
{D : Type u₁}
[category_theory.category D]
{J : Type v₁}
[category_theory.small_category J]
(F : J ⥤ D)
(R : D ⥤ C)
[category_theory.monadic_right_adjoint R]
[category_theory.limits.has_limit (F ⋙ R)] :
@[instance]
def
category_theory.comp_comparison_has_limit
{C : Type u₁}
[category_theory.category C]
{D : Type u₁}
[category_theory.category D]
{J : Type v₁}
[category_theory.small_category J]
(F : J ⥤ D)
(R : D ⥤ C)
[category_theory.monadic_right_adjoint R]
[category_theory.limits.has_limit (F ⋙ R)] :
def
category_theory.monadic_creates_limits
{C : Type u₁}
[category_theory.category C]
{D : Type u₁}
[category_theory.category D]
{J : Type v₁}
[category_theory.small_category J]
(F : J ⥤ D)
(R : D ⥤ C)
[category_theory.monadic_right_adjoint R]
[category_theory.limits.has_limit (F ⋙ R)] :
Any monadic functor creates limits.
def
category_theory.has_limits_of_reflective
{C : Type u₁}
[category_theory.category C]
{D : Type u₁}
[category_theory.category D]
(R : D ⥤ C)
[category_theory.limits.has_limits C]
[category_theory.reflective R] :
If C has limits then any reflective subcategory has limits
Equations
- category_theory.has_limits_of_reflective R = {has_limits_of_shape := λ (J : Type v₁) (𝒥 : category_theory.small_category J), {has_limit := λ (F : J ⥤ D), category_theory.monadic_creates_limits F R}}