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

## Main results #

• The category of cones on F : J ⥤ C is equivalent to the category costructured_arrow (const J) F.
• 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.
@[simp]
theorem category_theory.limits.cone.to_costructured_arrow_obj {J : Type u₁} {C : Type u₃} (F : J C)  :
@[simp]
theorem category_theory.limits.cone.to_costructured_arrow_map {J : Type u₁} {C : Type u₃} (F : J C) (c d : category_theory.limits.cone F) (f : c d) :
def category_theory.limits.cone.to_costructured_arrow {J : Type u₁} {C : Type u₃} (F : J C) :

Construct an object of the category (Δ ↓ F) from a cone on F. This is part of an equivalence, see cone.equiv_costructured_arrow.

Equations
@[simp]
theorem category_theory.limits.cone.from_costructured_arrow_obj_π {J : Type u₁} {C : Type u₃} (F : J C)  :
@[simp]
theorem category_theory.limits.cone.from_costructured_arrow_obj_X {J : Type u₁} {C : Type u₃} (F : J C)  :
@[simp]
theorem category_theory.limits.cone.from_costructured_arrow_map_hom {J : Type u₁} {C : Type u₃} (F : J C) (f : c d) :
def category_theory.limits.cone.from_costructured_arrow {J : Type u₁} {C : Type u₃} (F : J C) :

Construct a cone on F from an object of the category (Δ ↓ F). This is part of an equivalence, see cone.equiv_costructured_arrow.

Equations
@[simp]
theorem category_theory.limits.cone.equiv_costructured_arrow_functor_map_right_down_down {J : Type u₁} {C : Type u₃} (F : J C) (c d : category_theory.limits.cone F) (f : c d) :
_ = _
@[simp]
theorem category_theory.limits.cone.equiv_costructured_arrow_counit_iso_inv_app_right {J : Type u₁} {C : Type u₃} (F : J C)  :
= category_theory.eq_to_hom category_theory.costructured_arrow.iso_mk._proof_1
@[simp]
theorem category_theory.limits.cone.equiv_costructured_arrow_functor_obj_left {J : Type u₁} {C : Type u₃} (F : J C)  :
@[simp]
theorem category_theory.limits.cone.equiv_costructured_arrow_counit_iso_hom_app_left {J : Type u₁} {C : Type u₃} (F : J C)  :
@[simp]
theorem category_theory.limits.cone.equiv_costructured_arrow_unit_iso_hom_app_hom {J : Type u₁} {C : Type u₃} (F : J C)  :
@[simp]
theorem category_theory.limits.cone.equiv_costructured_arrow_functor_obj_hom {J : Type u₁} {C : Type u₃} (F : J C)  :
@[simp]
theorem category_theory.limits.cone.equiv_costructured_arrow_inverse_obj_π {J : Type u₁} {C : Type u₃} (F : J C)  :
@[simp]
theorem category_theory.limits.cone.equiv_costructured_arrow_functor_map_left {J : Type u₁} {C : Type u₃} (F : J C) (c d : category_theory.limits.cone F) (f : c d) :
def category_theory.limits.cone.equiv_costructured_arrow {J : Type u₁} {C : Type u₃} (F : J C) :

The category of cones on F is just the comma category (Δ ↓ F), where Δ is the constant functor.

Equations
@[simp]
theorem category_theory.limits.cone.equiv_costructured_arrow_inverse_map_hom {J : Type u₁} {C : Type u₃} (F : J C) (f : c d) :
@[simp]
theorem category_theory.limits.cone.equiv_costructured_arrow_inverse_obj_X {J : Type u₁} {C : Type u₃} (F : J C)  :
@[simp]
theorem category_theory.limits.cone.equiv_costructured_arrow_counit_iso_inv_app_left {J : Type u₁} {C : Type u₃} (F : J C)  :
@[simp]
theorem category_theory.limits.cone.equiv_costructured_arrow_counit_iso_hom_app_right {J : Type u₁} {C : Type u₃} (F : J C)  :
@[simp]
theorem category_theory.limits.cone.equiv_costructured_arrow_unit_iso_inv_app_hom {J : Type u₁} {C : Type u₃} (F : J C)  :
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.has_limit_iff_has_terminal_cone {J : Type u₁} {C : Type u₃} (F : J C) :
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
@[simp]
theorem category_theory.limits.cocone.to_structured_arrow_obj {J : Type u₁} {C : Type u₃} (F : J C)  :
def category_theory.limits.cocone.to_structured_arrow {J : Type u₁} {C : Type u₃} (F : J C) :

Construct an object of the category (F ↓ Δ) from a cocone on F. This is part of an equivalence, see cocone.equiv_structured_arrow.

Equations
@[simp]
theorem category_theory.limits.cocone.to_structured_arrow_map {J : Type u₁} {C : Type u₃} (F : J C) (c d : category_theory.limits.cocone F) (f : c d) :
@[simp]
theorem category_theory.limits.cocone.from_structured_arrow_map_hom {J : Type u₁} {C : Type u₃} (F : J C) (f : c d) :
def category_theory.limits.cocone.from_structured_arrow {J : Type u₁} {C : Type u₃} (F : J C) :

Construct a cocone on F from an object of the category (F ↓ Δ). This is part of an equivalence, see cocone.equiv_structured_arrow.

Equations
@[simp]
theorem category_theory.limits.cocone.from_structured_arrow_obj_ι {J : Type u₁} {C : Type u₃} (F : J C)  :
@[simp]
theorem category_theory.limits.cocone.from_structured_arrow_obj_X {J : Type u₁} {C : Type u₃} (F : J C)  :
def category_theory.limits.cocone.equiv_structured_arrow {J : Type u₁} {C : Type u₃} (F : J C) :

The category of cocones on F is just the comma category (F ↓ Δ), where Δ is the constant functor.

Equations
@[simp]
theorem category_theory.limits.cocone.equiv_structured_arrow_counit_iso_inv_app_right {J : Type u₁} {C : Type u₃} (F : J C)  :
@[simp]
theorem category_theory.limits.cocone.equiv_structured_arrow_unit_iso_hom_app_hom {J : Type u₁} {C : Type u₃} (F : J C)  :
@[simp]
theorem category_theory.limits.cocone.equiv_structured_arrow_inverse_obj_ι {J : Type u₁} {C : Type u₃} (F : J C)  :
@[simp]
theorem category_theory.limits.cocone.equiv_structured_arrow_functor_map_right {J : Type u₁} {C : Type u₃} (F : J C) (c d : category_theory.limits.cocone F) (f : c d) :
@[simp]
theorem category_theory.limits.cocone.equiv_structured_arrow_functor_map_left_down_down {J : Type u₁} {C : Type u₃} (F : J C) (c d : category_theory.limits.cocone F) (f : c d) :
_ = _
@[simp]
theorem category_theory.limits.cocone.equiv_structured_arrow_functor_obj_right {J : Type u₁} {C : Type u₃} (F : J C)  :
@[simp]
theorem category_theory.limits.cocone.equiv_structured_arrow_counit_iso_hom_app_left {J : Type u₁} {C : Type u₃} (F : J C)  :
@[simp]
theorem category_theory.limits.cocone.equiv_structured_arrow_unit_iso_inv_app_hom {J : Type u₁} {C : Type u₃} (F : J C)  :
@[simp]
theorem category_theory.limits.cocone.equiv_structured_arrow_inverse_obj_X {J : Type u₁} {C : Type u₃} (F : J C)  :
@[simp]
theorem category_theory.limits.cocone.equiv_structured_arrow_counit_iso_hom_app_right {J : Type u₁} {C : Type u₃} (F : J C)  :
@[simp]
theorem category_theory.limits.cocone.equiv_structured_arrow_functor_obj_hom {J : Type u₁} {C : Type u₃} (F : J C)  :
@[simp]
theorem category_theory.limits.cocone.equiv_structured_arrow_counit_iso_inv_app_left {J : Type u₁} {C : Type u₃} (F : J C)  :
= category_theory.eq_to_hom category_theory.structured_arrow.iso_mk._proof_1
@[simp]
theorem category_theory.limits.cocone.equiv_structured_arrow_inverse_map_hom {J : Type u₁} {C : Type u₃} (F : J C) (f : c d) :
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.has_colimit_iff_has_initial_cocone {J : Type u₁} {C : Type u₃} (F : J C) :
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