Preserving terminal object #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
The property of preserving terminal objects expressed in terms of is_terminal.
The property of reflecting terminal objects expressed in terms of is_terminal.
Preserving the terminal object implies preserving all limits of the empty diagram.
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 is an isomorphism.
The map of an empty cocone is a colimit iff the mapped object is initial.
The property of preserving initial objects expressed in terms of is_initial.
The property of reflecting initial objects expressed in terms of is_initial.
Preserving the initial object implies preserving all colimits of the empty diagram.
If G preserves the initial object and C has a initial object, then the image of the initial
object is initial.
If C has a initial object and G preserves initial objects, then D has a initial object
also.
Note this property is somewhat unique to colimits of the empty diagram: for general J, if C
has colimits of shape J and G preserves them, then D does not necessarily have colimits of
shape J.
If the initial comparison map for G is an isomorphism, then G preserves initial objects.
Equations
- category_theory.limits.preserves_initial.of_iso_comparison G = category_theory.limits.preserves_colimit_of_preserves_colimit_cocone category_theory.limits.initial_is_initial (⇑((category_theory.limits.is_colimit_map_cocone_empty_cocone_equiv G (⊥_ C)).symm) (category_theory.limits.colimit.is_colimit (category_theory.functor.empty D)).of_point_iso)
If there is any isomorphism ⊥ ⟶ G.obj ⊥, then G preserves initial objects.
If there is any isomorphism ⊥ ≅ G.obj ⊥, then G preserves initial objects.
If G preserves initial objects, then the initial comparison map for G is an isomorphism.