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.
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 := _}
If G : cone F ⥤ cone F'
preserves terminal objects, it preserves limit cones.
Equations
If G : cone F ⥤ cone F'
reflects terminal objects, it reflects limit cones.
Equations
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 := _}
If G : cocone F ⥤ cocone F'
preserves initial objects, it preserves colimit cocones.
Equations
If G : cocone F ⥤ cocone F'
reflects initial objects, it reflects colimit cocones.