mathlibdocumentation

category_theory.limits.cone_category

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₁} {C : Type u₃} {F : J C}  :

A cone is a limit cone iff it is terminal.

Equations
theorem category_theory.limits.is_terminal.from_eq_lift_cone_morphism {J : Type u₁} {C : Type u₃} {F : J C}  :
hc.from s =
def category_theory.limits.is_limit.of_preserves_cone_terminal {J : Type u₁} {K : Type u₂} {C : Type u₃} {D : Type u₄} {F : J C} {F' : K D}  :

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₁} {K : Type u₂} {C : Type u₃} {D : Type u₄} {F : J C} {F' : K D} (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₁} {C : Type u₃} {F : J C}  :

A cocone is a colimit cocone iff it is initial.

Equations
theorem category_theory.limits.is_initial.to_eq_desc_cocone_morphism {J : Type u₁} {C : Type u₃} {F : J C}  :
hc.to s =
def category_theory.limits.is_colimit.of_preserves_cocone_initial {J : Type u₁} {K : Type u₂} {C : Type u₃} {D : Type u₄} {F : J C} {F' : K D}  :

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₁} {K : Type u₂} {C : Type u₃} {D : Type u₄} {F : J C} {F' : K D} (hc : category_theory.limits.is_colimit (G.obj c)) :

If G : cocone F ⥤ cocone F' reflects initial objects, it reflects colimit cocones.

Equations