Preserving terminal object #
Constructions to relate the notions of preserving terminal objects and reflecting terminal objects to concrete objects.
In particular, we show that terminal_comparison G
is an isomorphism iff G
preserves terminal
objects.
The map of an empty cone is a limit iff the mapped object is terminal.
Equations
- category_theory.limits.is_limit_map_cone_empty_cone_equiv G X = (category_theory.limits.is_limit.postcompose_hom_equiv ((category_theory.functor.empty C ⋙ G).empty_ext (category_theory.functor.empty D)) (G.map_cone (category_theory.limits.as_empty_cone X))).symm.trans (category_theory.limits.is_limit.equiv_iso_limit (category_theory.limits.cones.ext (category_theory.iso.refl ((category_theory.limits.cones.postcompose ((category_theory.functor.empty C ⋙ G).empty_ext (category_theory.functor.empty D)).hom).obj (G.map_cone (category_theory.limits.as_empty_cone X))).X) _))
The property of preserving terminal objects expressed in terms of is_terminal
.
The property of reflecting terminal objects expressed in terms of is_terminal
.
If G
preserves the terminal object and C
has a terminal object, then the image of the terminal
object is terminal.
If C
has a terminal object and G
preserves terminal objects, then D
has a terminal object
also.
Note this property is somewhat unique to (co)limits of the empty diagram: for general J
, if C
has limits of shape J
and G
preserves them, then D
does not necessarily have limits of shape
J
.
If the terminal comparison map for G
is an isomorphism, then G
preserves terminal objects.
Equations
- category_theory.limits.preserves_terminal.of_iso_comparison G = category_theory.limits.preserves_limit_of_preserves_limit_cone category_theory.limits.terminal_is_terminal (⇑((category_theory.limits.is_limit_map_cone_empty_cone_equiv G (⊤_C)).symm) (category_theory.limits.limit.is_limit (category_theory.functor.empty D)).of_point_iso)
If there is any isomorphism G.obj ⊤ ⟶ ⊤
, then G
preserves terminal objects.
If there is any isomorphism G.obj ⊤ ≅ ⊤
, then G
preserves terminal objects.
If G
preserves terminal objects, then the terminal comparison map for G
an isomorphism.