Limits and the category of (co)cones #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 ⥤ Cis equivalent to the categorycostructured_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₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(c : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.limits.cone.to_costructured_arrow_map
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(c d : category_theory.limits.cone F)
(f : c ⟶ d) :
def
category_theory.limits.cone.to_costructured_arrow
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(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
- category_theory.limits.cone.to_costructured_arrow F = {obj := λ (c : category_theory.limits.cone F), category_theory.costructured_arrow.mk c.π, map := λ (c d : category_theory.limits.cone F) (f : c ⟶ d), category_theory.costructured_arrow.hom_mk f.hom _, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.limits.cone.from_costructured_arrow_obj_π
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(c : category_theory.costructured_arrow (category_theory.functor.const J) F) :
@[simp]
theorem
category_theory.limits.cone.from_costructured_arrow_obj_X
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(c : category_theory.costructured_arrow (category_theory.functor.const J) F) :
@[simp]
theorem
category_theory.limits.cone.from_costructured_arrow_map_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(c d : category_theory.costructured_arrow (category_theory.functor.const J) F)
(f : c ⟶ d) :
def
category_theory.limits.cone.from_costructured_arrow
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(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
- category_theory.limits.cone.from_costructured_arrow F = {obj := λ (c : category_theory.costructured_arrow (category_theory.functor.const J) F), {X := c.left, π := c.hom}, map := λ (c d : category_theory.costructured_arrow (category_theory.functor.const J) F) (f : c ⟶ d), {hom := f.left, w' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.limits.cone.equiv_costructured_arrow_functor_map_right_down_down
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(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₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(X : category_theory.costructured_arrow (category_theory.functor.const J) F) :
((category_theory.limits.cone.equiv_costructured_arrow F).counit_iso.inv.app X).right = 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₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(c : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.limits.cone.equiv_costructured_arrow_counit_iso_hom_app_left
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(X : category_theory.costructured_arrow (category_theory.functor.const J) F) :
@[simp]
theorem
category_theory.limits.cone.equiv_costructured_arrow_unit_iso_hom_app_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(X : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.limits.cone.equiv_costructured_arrow_functor_obj_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(c : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.limits.cone.equiv_costructured_arrow_inverse_obj_π
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(c : category_theory.costructured_arrow (category_theory.functor.const J) F) :
@[simp]
theorem
category_theory.limits.cone.equiv_costructured_arrow_functor_map_left
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(c d : category_theory.limits.cone F)
(f : c ⟶ d) :
def
category_theory.limits.cone.equiv_costructured_arrow
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C) :
The category of cones on F is just the comma category (Δ ↓ F), where Δ is the constant
functor.
Equations
- category_theory.limits.cone.equiv_costructured_arrow F = category_theory.equivalence.mk (category_theory.limits.cone.to_costructured_arrow F) (category_theory.limits.cone.from_costructured_arrow F) (category_theory.nat_iso.of_components category_theory.limits.cones.eta _) (category_theory.nat_iso.of_components (λ (c : category_theory.costructured_arrow (category_theory.functor.const J) F), c.eta.symm) _)
@[simp]
theorem
category_theory.limits.cone.equiv_costructured_arrow_inverse_map_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(c d : category_theory.costructured_arrow (category_theory.functor.const J) F)
(f : c ⟶ d) :
@[simp]
theorem
category_theory.limits.cone.equiv_costructured_arrow_inverse_obj_X
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(c : category_theory.costructured_arrow (category_theory.functor.const J) F) :
@[simp]
theorem
category_theory.limits.cone.equiv_costructured_arrow_counit_iso_inv_app_left
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(X : category_theory.costructured_arrow (category_theory.functor.const J) F) :
@[simp]
theorem
category_theory.limits.cone.equiv_costructured_arrow_counit_iso_hom_app_right
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(X : category_theory.costructured_arrow (category_theory.functor.const J) F) :
@[simp]
theorem
category_theory.limits.cone.equiv_costructured_arrow_unit_iso_inv_app_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(X : category_theory.limits.cone F) :
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.has_limit_iff_has_terminal_cone
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C) :
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
@[simp]
theorem
category_theory.limits.cocone.to_structured_arrow_obj
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(c : category_theory.limits.cocone F) :
def
category_theory.limits.cocone.to_structured_arrow
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(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
- category_theory.limits.cocone.to_structured_arrow F = {obj := λ (c : category_theory.limits.cocone F), category_theory.structured_arrow.mk c.ι, map := λ (c d : category_theory.limits.cocone F) (f : c ⟶ d), category_theory.structured_arrow.hom_mk f.hom _, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.limits.cocone.to_structured_arrow_map
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(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₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(c d : category_theory.structured_arrow F (category_theory.functor.const J))
(f : c ⟶ d) :
def
category_theory.limits.cocone.from_structured_arrow
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(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
- category_theory.limits.cocone.from_structured_arrow F = {obj := λ (c : category_theory.structured_arrow F (category_theory.functor.const J)), {X := c.right, ι := c.hom}, map := λ (c d : category_theory.structured_arrow F (category_theory.functor.const J)) (f : c ⟶ d), {hom := f.right, w' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.limits.cocone.from_structured_arrow_obj_ι
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(c : category_theory.structured_arrow F (category_theory.functor.const J)) :
@[simp]
theorem
category_theory.limits.cocone.from_structured_arrow_obj_X
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(c : category_theory.structured_arrow F (category_theory.functor.const J)) :
def
category_theory.limits.cocone.equiv_structured_arrow
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C) :
The category of cocones on F is just the comma category (F ↓ Δ), where Δ is the constant
functor.
Equations
- category_theory.limits.cocone.equiv_structured_arrow F = category_theory.equivalence.mk (category_theory.limits.cocone.to_structured_arrow F) (category_theory.limits.cocone.from_structured_arrow F) (category_theory.nat_iso.of_components category_theory.limits.cocones.eta _) (category_theory.nat_iso.of_components (λ (c : category_theory.structured_arrow F (category_theory.functor.const J)), c.eta.symm) _)
@[simp]
theorem
category_theory.limits.cocone.equiv_structured_arrow_counit_iso_inv_app_right
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(X : category_theory.structured_arrow F (category_theory.functor.const J)) :
@[simp]
theorem
category_theory.limits.cocone.equiv_structured_arrow_unit_iso_hom_app_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(X : category_theory.limits.cocone F) :
@[simp]
theorem
category_theory.limits.cocone.equiv_structured_arrow_inverse_obj_ι
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(c : category_theory.structured_arrow F (category_theory.functor.const J)) :
@[simp]
theorem
category_theory.limits.cocone.equiv_structured_arrow_functor_map_right
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(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₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(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₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(c : category_theory.limits.cocone F) :
@[simp]
theorem
category_theory.limits.cocone.equiv_structured_arrow_counit_iso_hom_app_left
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(X : category_theory.structured_arrow F (category_theory.functor.const J)) :
@[simp]
theorem
category_theory.limits.cocone.equiv_structured_arrow_unit_iso_inv_app_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(X : category_theory.limits.cocone F) :
@[simp]
theorem
category_theory.limits.cocone.equiv_structured_arrow_inverse_obj_X
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(c : category_theory.structured_arrow F (category_theory.functor.const J)) :
@[simp]
theorem
category_theory.limits.cocone.equiv_structured_arrow_counit_iso_hom_app_right
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(X : category_theory.structured_arrow F (category_theory.functor.const J)) :
@[simp]
theorem
category_theory.limits.cocone.equiv_structured_arrow_functor_obj_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(c : category_theory.limits.cocone F) :
@[simp]
theorem
category_theory.limits.cocone.equiv_structured_arrow_counit_iso_inv_app_left
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(X : category_theory.structured_arrow F (category_theory.functor.const J)) :
((category_theory.limits.cocone.equiv_structured_arrow F).counit_iso.inv.app X).left = 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₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C)
(c d : category_theory.structured_arrow F (category_theory.functor.const J))
(f : c ⟶ d) :
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.has_colimit_iff_has_initial_cocone
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
(F : J ⥤ C) :
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.