Limits and the category of (co)cones #
This files contains results that stem from the limit API. For the definition and the category
instance of cone, please refer to category_theory/limits/cones.lean.
A cone is limiting iff it is terminal in the category of cones. As a corollary, an equivalence of categories of cones preserves limiting properties. We also provide the dual.
def
category_theory.limits.cone.is_limit_equiv_is_terminal
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cone F) :
A cone is a limit cone iff it is terminal.
Equations
- c.is_limit_equiv_is_terminal = category_theory.limits.is_limit.iso_unique_cone_morphism.to_equiv.trans {to_fun := λ (h : Π (s : category_theory.limits.cone F), unique (s ⟶ c)), category_theory.limits.is_terminal.of_unique c, inv_fun := λ (h : category_theory.limits.is_terminal c) (s : category_theory.limits.cone F), {to_inhabited := {default := h.from s}, uniq := _}, left_inv := _, right_inv := _}
theorem
category_theory.limits.is_limit.lift_cone_morphism_eq_is_terminal_from
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{c : category_theory.limits.cone F}
(hc : category_theory.limits.is_limit c)
(s : category_theory.limits.cone F) :
hc.lift_cone_morphism s = (⇑(c.is_limit_equiv_is_terminal) hc).from s
theorem
category_theory.limits.is_terminal.from_eq_lift_cone_morphism
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{c : category_theory.limits.cone F}
(hc : category_theory.limits.is_terminal c)
(s : category_theory.limits.cone F) :
hc.from s = (⇑(c.is_limit_equiv_is_terminal.symm) hc).lift_cone_morphism s
def
category_theory.limits.is_limit.of_preserves_cone_terminal
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
{F' : K ⥤ D}
(G : category_theory.limits.cone F ⥤ category_theory.limits.cone F')
[category_theory.limits.preserves_limit (category_theory.functor.empty (category_theory.limits.cone F)) G]
{c : category_theory.limits.cone F}
(hc : category_theory.limits.is_limit c) :
If G : cone F ⥤ cone F' preserves terminal objects, it preserves limit cones.
Equations
def
category_theory.limits.is_limit.of_reflects_cone_terminal
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
{F' : K ⥤ D}
(G : category_theory.limits.cone F ⥤ category_theory.limits.cone F')
[category_theory.limits.reflects_limit (category_theory.functor.empty (category_theory.limits.cone F)) G]
{c : category_theory.limits.cone F}
(hc : category_theory.limits.is_limit (G.obj c)) :
If G : cone F ⥤ cone F' reflects terminal objects, it reflects limit cones.
Equations
def
category_theory.limits.cocone.is_colimit_equiv_is_initial
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(c : category_theory.limits.cocone F) :
A cocone is a colimit cocone iff it is initial.
Equations
- c.is_colimit_equiv_is_initial = category_theory.limits.is_colimit.iso_unique_cocone_morphism.to_equiv.trans {to_fun := λ (h : Π (s : category_theory.limits.cocone F), unique (c ⟶ s)), category_theory.limits.is_initial.of_unique c, inv_fun := λ (h : category_theory.limits.is_initial c) (s : category_theory.limits.cocone F), {to_inhabited := {default := h.to s}, uniq := _}, left_inv := _, right_inv := _}
theorem
category_theory.limits.is_colimit.desc_cocone_morphism_eq_is_initial_to
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{c : category_theory.limits.cocone F}
(hc : category_theory.limits.is_colimit c)
(s : category_theory.limits.cocone F) :
hc.desc_cocone_morphism s = (⇑(c.is_colimit_equiv_is_initial) hc).to s
theorem
category_theory.limits.is_initial.to_eq_desc_cocone_morphism
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{c : category_theory.limits.cocone F}
(hc : category_theory.limits.is_initial c)
(s : category_theory.limits.cocone F) :
hc.to s = (⇑(c.is_colimit_equiv_is_initial.symm) hc).desc_cocone_morphism s
def
category_theory.limits.is_colimit.of_preserves_cocone_initial
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
{F' : K ⥤ D}
(G : category_theory.limits.cocone F ⥤ category_theory.limits.cocone F')
[category_theory.limits.preserves_colimit (category_theory.functor.empty (category_theory.limits.cocone F)) G]
{c : category_theory.limits.cocone F}
(hc : category_theory.limits.is_colimit c) :
If G : cocone F ⥤ cocone F' preserves initial objects, it preserves colimit cocones.
Equations
def
category_theory.limits.is_colimit.of_reflects_cocone_initial
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{D : Type u₄}
[category_theory.category D]
{F : J ⥤ C}
{F' : K ⥤ D}
(G : category_theory.limits.cocone F ⥤ category_theory.limits.cocone F')
[category_theory.limits.reflects_colimit (category_theory.functor.empty (category_theory.limits.cocone F)) G]
{c : category_theory.limits.cocone F}
(hc : category_theory.limits.is_colimit (G.obj c)) :
If G : cocone F ⥤ cocone F' reflects initial objects, it reflects colimit cocones.