mathlib3 documentation

category_theory.monad.limits

Limits and colimits in the category of algebras #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

TODO #

Dualise for the category of coalgebras and comonadic left adjoints.

def category_theory.monad.forget_creates_limits.γ {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {J : Type u} [category_theory.category J] (D : J ⥤ T.algebra) :

D ⋙ T.forget ⋙ ↑T ⟶ D ⋙ T.forget

(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' := _}

@[simp]

theorem category_theory.monad.forget_creates_limits.γ_app {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {J : Type u} [category_theory.category J] (D : J ⥤ T.algebra) (j : J) :

(category_theory.monad.forget_creates_limits.γ D).app j = (D.obj j).a

def category_theory.monad.forget_creates_limits.new_cone {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {J : Type u} [category_theory.category J] (D : J ⥤ T.algebra) (c : category_theory.limits.cone (D ⋙ T.forget)) :

category_theory.limits.cone (D ⋙ T.forget)

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

Equations

category_theory.monad.forget_creates_limits.new_cone D c = {X := T.to_functor.obj c.X, π := (category_theory.functor.const_comp J c.X ↑T).inv ≫ category_theory.whisker_right c.π ↑T ≫ category_theory.monad.forget_creates_limits.γ D}

@[simp]

theorem category_theory.monad.forget_creates_limits.new_cone_π_app {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {J : Type u} [category_theory.category J] (D : J ⥤ T.algebra) (c : category_theory.limits.cone (D ⋙ T.forget)) (X : J) :

(category_theory.monad.forget_creates_limits.new_cone D c).π.app X = ↑T.map (c.π.app X) ≫ (D.obj X).a

def category_theory.monad.forget_creates_limits.cone_point {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {J : Type u} [category_theory.category J] (D : J ⥤ T.algebra) (c : category_theory.limits.cone (D ⋙ T.forget)) (t : category_theory.limits.is_limit c) :

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 : category_theory.monad C} {J : Type u} [category_theory.category J] (D : J ⥤ T.algebra) (c : category_theory.limits.cone (D ⋙ T.forget)) (t : category_theory.limits.is_limit c) :

(category_theory.monad.forget_creates_limits.cone_point D c t).a = t.lift (category_theory.monad.forget_creates_limits.new_cone D c)

@[simp]

theorem category_theory.monad.forget_creates_limits.cone_point_A {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {J : Type u} [category_theory.category J] (D : J ⥤ T.algebra) (c : category_theory.limits.cone (D ⋙ T.forget)) (t : category_theory.limits.is_limit c) :

(category_theory.monad.forget_creates_limits.cone_point D c t).A = c.X

def category_theory.monad.forget_creates_limits.lifted_cone {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {J : Type u} [category_theory.category J] (D : J ⥤ T.algebra) (c : category_theory.limits.cone (D ⋙ T.forget)) (t : category_theory.limits.is_limit c) :

category_theory.limits.cone D

(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 : category_theory.monad C} {J : Type u} [category_theory.category J] (D : J ⥤ T.algebra) (c : category_theory.limits.cone (D ⋙ T.forget)) (t : category_theory.limits.is_limit c) (j : J) :

((category_theory.monad.forget_creates_limits.lifted_cone D c t).π.app j).f = c.π.app j

@[simp]

theorem category_theory.monad.forget_creates_limits.lifted_cone_X {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {J : Type u} [category_theory.category J] (D : J ⥤ T.algebra) (c : category_theory.limits.cone (D ⋙ T.forget)) (t : category_theory.limits.is_limit c) :

(category_theory.monad.forget_creates_limits.lifted_cone D c t).X = category_theory.monad.forget_creates_limits.cone_point D c t

@[simp]

theorem category_theory.monad.forget_creates_limits.lifted_cone_is_limit_lift_f {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {J : Type u} [category_theory.category J] (D : J ⥤ T.algebra) (c : category_theory.limits.cone (D ⋙ T.forget)) (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 (T.forget.map_cone s)

def category_theory.monad.forget_creates_limits.lifted_cone_is_limit {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {J : Type u} [category_theory.category J] (D : J ⥤ T.algebra) (c : category_theory.limits.cone (D ⋙ T.forget)) (t : category_theory.limits.is_limit c) :

category_theory.limits.is_limit (category_theory.monad.forget_creates_limits.lifted_cone D c t)

(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 (T.forget.map_cone s), h' := _}, fac' := _, uniq' := _}

@[protected, instance]

noncomputable def category_theory.monad.forget_creates_limits {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} :

category_theory.creates_limits_of_size T.forget

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

Equations

category_theory.monad.forget_creates_limits = {creates_limits_of_shape := λ (J : Type u_2) (𝒥 : category_theory.category J), {creates_limit := λ (D : J ⥤ T.algebra), category_theory.creates_limit_of_reflects_iso (λ (c : category_theory.limits.cone (D ⋙ T.forget)) (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 (T.forget.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})}}

theorem category_theory.monad.has_limit_of_comp_forget_has_limit {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {J : Type u} [category_theory.category J] (D : J ⥤ T.algebra) [category_theory.limits.has_limit (D ⋙ T.forget)] :

category_theory.limits.has_limit D

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

@[simp]

theorem category_theory.monad.forget_creates_colimits.γ_app {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {J : Type u} [category_theory.category J] {D : J ⥤ T.algebra} (j : J) :

category_theory.monad.forget_creates_colimits.γ.app j = (D.obj j).a

def category_theory.monad.forget_creates_colimits.γ {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {J : Type u} [category_theory.category J] {D : J ⥤ T.algebra} :

(D ⋙ T.forget) ⋙ ↑T ⟶ D ⋙ T.forget

(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.new_cocone_X {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {J : Type u} [category_theory.category J] {D : J ⥤ T.algebra} (c : category_theory.limits.cocone (D ⋙ T.forget)) :

(category_theory.monad.forget_creates_colimits.new_cocone c).X = c.X

@[simp]

theorem category_theory.monad.forget_creates_colimits.new_cocone_ι {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {J : Type u} [category_theory.category J] {D : J ⥤ T.algebra} (c : category_theory.limits.cocone (D ⋙ T.forget)) :

(category_theory.monad.forget_creates_colimits.new_cocone c).ι = category_theory.monad.forget_creates_colimits.γ ≫ c.ι

def category_theory.monad.forget_creates_colimits.new_cocone {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {J : Type u} [category_theory.category J] {D : J ⥤ T.algebra} (c : category_theory.limits.cocone (D ⋙ T.forget)) :

category_theory.limits.cocone ((D ⋙ T.forget) ⋙ ↑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

category_theory.monad.forget_creates_colimits.new_cocone c = {X := c.X, ι := category_theory.monad.forget_creates_colimits.γ ≫ c.ι}

@[reducible]

def category_theory.monad.forget_creates_colimits.lambda {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {J : Type u} [category_theory.category J] {D : J ⥤ T.algebra} (c : category_theory.limits.cocone (D ⋙ T.forget)) (t : category_theory.limits.is_colimit c) [category_theory.limits.preserves_colimit (D ⋙ T.forget) ↑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.

Equations

category_theory.monad.forget_creates_colimits.lambda c t = (category_theory.limits.is_colimit_of_preserves ↑T t).desc (category_theory.monad.forget_creates_colimits.new_cocone c)

theorem category_theory.monad.forget_creates_colimits.commuting {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {J : Type u} [category_theory.category J] {D : J ⥤ T.algebra} (c : category_theory.limits.cocone (D ⋙ T.forget)) (t : category_theory.limits.is_colimit c) [category_theory.limits.preserves_colimit (D ⋙ T.forget) ↑T] (j : J) :

↑T.map (c.ι.app j) ≫ category_theory.monad.forget_creates_colimits.lambda c t = (D.obj j).a ≫ c.ι.app j

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

def category_theory.monad.forget_creates_colimits.cocone_point {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {J : Type u} [category_theory.category J] {D : J ⥤ T.algebra} (c : category_theory.limits.cocone (D ⋙ T.forget)) (t : category_theory.limits.is_colimit c) [category_theory.limits.preserves_colimit (D ⋙ T.forget) ↑T] [category_theory.limits.preserves_colimit ((D ⋙ T.forget) ⋙ ↑T) ↑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_3, unit' := _, assoc' := _}

@[simp]

theorem category_theory.monad.forget_creates_colimits.cocone_point_A {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {J : Type u} [category_theory.category J] {D : J ⥤ T.algebra} (c : category_theory.limits.cocone (D ⋙ T.forget)) (t : category_theory.limits.is_colimit c) [category_theory.limits.preserves_colimit (D ⋙ T.forget) ↑T] [category_theory.limits.preserves_colimit ((D ⋙ T.forget) ⋙ ↑T) ↑T] :

(category_theory.monad.forget_creates_colimits.cocone_point c t).A = c.X

@[simp]

theorem category_theory.monad.forget_creates_colimits.cocone_point_a {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {J : Type u} [category_theory.category J] {D : J ⥤ T.algebra} (c : category_theory.limits.cocone (D ⋙ T.forget)) (t : category_theory.limits.is_colimit c) [category_theory.limits.preserves_colimit (D ⋙ T.forget) ↑T] [category_theory.limits.preserves_colimit ((D ⋙ T.forget) ⋙ ↑T) ↑T] :

(category_theory.monad.forget_creates_colimits.cocone_point c t).a = category_theory.monad.forget_creates_colimits.lambda c t

@[simp]

theorem category_theory.monad.forget_creates_colimits.lifted_cocone_X {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {J : Type u} [category_theory.category J] {D : J ⥤ T.algebra} (c : category_theory.limits.cocone (D ⋙ T.forget)) (t : category_theory.limits.is_colimit c) [category_theory.limits.preserves_colimit (D ⋙ T.forget) ↑T] [category_theory.limits.preserves_colimit ((D ⋙ T.forget) ⋙ ↑T) ↑T] :

(category_theory.monad.forget_creates_colimits.lifted_cocone c t).X = category_theory.monad.forget_creates_colimits.cocone_point c t

@[simp]

theorem category_theory.monad.forget_creates_colimits.lifted_cocone_ι_app_f {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {J : Type u} [category_theory.category J] {D : J ⥤ T.algebra} (c : category_theory.limits.cocone (D ⋙ T.forget)) (t : category_theory.limits.is_colimit c) [category_theory.limits.preserves_colimit (D ⋙ T.forget) ↑T] [category_theory.limits.preserves_colimit ((D ⋙ T.forget) ⋙ ↑T) ↑T] (j : J) :

((category_theory.monad.forget_creates_colimits.lifted_cocone c t).ι.app j).f = c.ι.app j

def category_theory.monad.forget_creates_colimits.lifted_cocone {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {J : Type u} [category_theory.category J] {D : J ⥤ T.algebra} (c : category_theory.limits.cocone (D ⋙ T.forget)) (t : category_theory.limits.is_colimit c) [category_theory.limits.preserves_colimit (D ⋙ T.forget) ↑T] [category_theory.limits.preserves_colimit ((D ⋙ T.forget) ⋙ ↑T) ↑T] :

category_theory.limits.cocone D

(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' := _}}

def category_theory.monad.forget_creates_colimits.lifted_cocone_is_colimit {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {J : Type u} [category_theory.category J] {D : J ⥤ T.algebra} (c : category_theory.limits.cocone (D ⋙ T.forget)) (t : category_theory.limits.is_colimit c) [category_theory.limits.preserves_colimit (D ⋙ T.forget) ↑T] [category_theory.limits.preserves_colimit ((D ⋙ T.forget) ⋙ ↑T) ↑T] :

category_theory.limits.is_colimit (category_theory.monad.forget_creates_colimits.lifted_cocone c 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 (T.forget.map_cocone s), h' := _}, fac' := _, uniq' := _}

@[simp]

theorem category_theory.monad.forget_creates_colimits.lifted_cocone_is_colimit_desc_f {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {J : Type u} [category_theory.category J] {D : J ⥤ T.algebra} (c : category_theory.limits.cocone (D ⋙ T.forget)) (t : category_theory.limits.is_colimit c) [category_theory.limits.preserves_colimit (D ⋙ T.forget) ↑T] [category_theory.limits.preserves_colimit ((D ⋙ T.forget) ⋙ ↑T) ↑T] (s : category_theory.limits.cocone D) :

((category_theory.monad.forget_creates_colimits.lifted_cocone_is_colimit c t).desc s).f = t.desc (T.forget.map_cocone s)

@[protected, instance]

noncomputable def category_theory.monad.forget_creates_colimit {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {J : Type u} [category_theory.category J] (D : J ⥤ T.algebra) [category_theory.limits.preserves_colimit (D ⋙ T.forget) ↑T] [category_theory.limits.preserves_colimit ((D ⋙ T.forget) ⋙ ↑T) ↑T] :

category_theory.creates_colimit D T.forget

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_colimit D = category_theory.creates_colimit_of_reflects_iso (λ (c : category_theory.limits.cocone (D ⋙ T.forget)) (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 (T.forget.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})

@[protected, instance]

noncomputable def category_theory.monad.forget_creates_colimits_of_shape {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {J : Type u} [category_theory.category J] [category_theory.limits.preserves_colimits_of_shape J ↑T] :

category_theory.creates_colimits_of_shape J T.forget

Equations

category_theory.monad.forget_creates_colimits_of_shape = {creates_colimit := λ (K : J ⥤ T.algebra), category_theory.monad.forget_creates_colimit K}

@[protected, instance]

noncomputable def category_theory.monad.forget_creates_colimits {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} [category_theory.limits.preserves_colimits_of_size ↑T] :

category_theory.creates_colimits_of_size T.forget

Equations

category_theory.monad.forget_creates_colimits = {creates_colimits_of_shape := λ (J : Type u) (𝒥₁ : category_theory.category J), category_theory.monad.forget_creates_colimits_of_shape}

theorem category_theory.monad.forget_creates_colimits_of_monad_preserves {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {J : Type u} [category_theory.category J] [category_theory.limits.preserves_colimits_of_shape J ↑T] (D : J ⥤ T.algebra) [category_theory.limits.has_colimit (D ⋙ T.forget)] :

category_theory.limits.has_colimit 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.

@[protected, 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 u} [category_theory.category J] (F : J ⥤ D) (R : D ⥤ C) [category_theory.monadic_right_adjoint R] [category_theory.limits.has_limit (F ⋙ R)] :

category_theory.limits.has_limit ((F ⋙ category_theory.monad.comparison (category_theory.adjunction.of_right_adjoint R)) ⋙ (category_theory.adjunction.of_right_adjoint R).to_monad.forget)

@[protected, instance]

def category_theory.comp_comparison_has_limit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type u} [category_theory.category J] (F : J ⥤ D) (R : D ⥤ C) [category_theory.monadic_right_adjoint R] [category_theory.limits.has_limit (F ⋙ R)] :

category_theory.limits.has_limit (F ⋙ category_theory.monad.comparison (category_theory.adjunction.of_right_adjoint R))

noncomputable def category_theory.monadic_creates_limits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (R : D ⥤ C) [category_theory.monadic_right_adjoint R] :

category_theory.creates_limits_of_size R

Any monadic functor creates limits.

Equations

category_theory.monadic_creates_limits R = category_theory.creates_limits_of_nat_iso (category_theory.monad.comparison_forget (category_theory.adjunction.of_right_adjoint R))

noncomputable def category_theory.monadic_creates_colimit_of_preserves_colimit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type u} [category_theory.category J] (R : D ⥤ C) (K : J ⥤ D) [category_theory.monadic_right_adjoint R] [category_theory.limits.preserves_colimit (K ⋙ R) (category_theory.left_adjoint R ⋙ R)] [category_theory.limits.preserves_colimit ((K ⋙ R) ⋙ category_theory.left_adjoint R ⋙ R) (category_theory.left_adjoint R ⋙ R)] :

category_theory.creates_colimit K R

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

Equations

category_theory.monadic_creates_colimit_of_preserves_colimit R K = category_theory.creates_colimit_of_nat_iso (category_theory.monad.comparison_forget (category_theory.adjunction.of_right_adjoint R))

noncomputable def category_theory.monadic_creates_colimits_of_shape_of_preserves_colimits_of_shape {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type u} [category_theory.category J] (R : D ⥤ C) [category_theory.monadic_right_adjoint R] [category_theory.limits.preserves_colimits_of_shape J R] :

category_theory.creates_colimits_of_shape J R

A monadic functor creates any colimits of shapes it preserves.

Equations

category_theory.monadic_creates_colimits_of_shape_of_preserves_colimits_of_shape R = {creates_colimit := λ (K : J ⥤ D), category_theory.monadic_creates_colimit_of_preserves_colimit R K}

noncomputable def category_theory.monadic_creates_colimits_of_preserves_colimits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (R : D ⥤ C) [category_theory.monadic_right_adjoint R] [category_theory.limits.preserves_colimits_of_size R] :

category_theory.creates_colimits_of_size R

A monadic functor creates colimits if it preserves colimits.

Equations

category_theory.monadic_creates_colimits_of_preserves_colimits R = {creates_colimits_of_shape := λ (J : Type u) (𝒥₁ : category_theory.category J), category_theory.monadic_creates_colimits_of_shape_of_preserves_colimits_of_shape R}

theorem category_theory.has_limit_of_reflective {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type u} [category_theory.category J] (F : J ⥤ D) (R : D ⥤ C) [category_theory.limits.has_limit (F ⋙ R)] [category_theory.reflective R] :

category_theory.limits.has_limit F

theorem category_theory.has_limits_of_shape_of_reflective {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type u} [category_theory.category J] [category_theory.limits.has_limits_of_shape J C] (R : D ⥤ C) [category_theory.reflective R] :

category_theory.limits.has_limits_of_shape J D

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

theorem 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_of_size C] [category_theory.reflective R] :

category_theory.limits.has_limits_of_size D

If C has limits then any reflective subcategory has limits.

theorem category_theory.has_colimits_of_shape_of_reflective {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {J : Type u} [category_theory.category J] (R : D ⥤ C) [category_theory.reflective R] [category_theory.limits.has_colimits_of_shape J C] :

category_theory.limits.has_colimits_of_shape J D

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

theorem category_theory.has_colimits_of_reflective {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (R : D ⥤ C) [category_theory.reflective R] [category_theory.limits.has_colimits_of_size C] :

category_theory.limits.has_colimits_of_size D

If C has colimits then any reflective subcategory has colimits.

noncomputable def category_theory.left_adjoint_preserves_terminal_of_reflective {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (R : D ⥤ C) [category_theory.reflective R] :

category_theory.limits.preserves_limits_of_shape (category_theory.discrete pempty) (category_theory.left_adjoint R)

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

Equations

category_theory.left_adjoint_preserves_terminal_of_reflective R = {preserves_limit := λ (K : category_theory.discrete pempty ⥤ C), let F : category_theory.discrete pempty ⥤ D := category_theory.functor.empty D in category_theory.limits.preserves_limit_of_iso_diagram (category_theory.left_adjoint R) ((F ⋙ R).empty_ext K)}