# mathlibdocumentation

category_theory.limits.preserves.shapes.terminal

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

def category_theory.limits.is_limit_map_cone_empty_cone_equiv {C : Type u₁} {D : Type u₂} (G : C D) (X : C) :

The map of an empty cone is a limit iff the mapped object is terminal.

Equations
def category_theory.limits.is_terminal.is_terminal_obj {C : Type u₁} {D : Type u₂} (G : C D) (X : C)  :

The property of preserving terminal objects expressed in terms of is_terminal.

Equations
def category_theory.limits.is_terminal.is_terminal_of_obj {C : Type u₁} {D : Type u₂} (G : C D) (X : C) (l : category_theory.limits.is_terminal (G.obj X)) :

The property of reflecting terminal objects expressed in terms of is_terminal.

Equations
noncomputable def category_theory.limits.is_limit_of_has_terminal_of_preserves_limit {C : Type u₁} {D : Type u₂} (G : C D)  :

If G preserves the terminal object and C has a terminal object, then the image of the terminal object is terminal.

Equations
theorem category_theory.limits.has_terminal_of_has_terminal_of_preserves_limit {C : Type u₁} {D : Type u₂} (G : C D)  :

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.

noncomputable def category_theory.limits.preserves_terminal.of_iso_comparison {C : Type u₁} {D : Type u₂} (G : C D)  :

If the terminal comparison map for G is an isomorphism, then G preserves terminal objects.

Equations
noncomputable def category_theory.limits.preserves_terminal_of_is_iso {C : Type u₁} {D : Type u₂} (G : C D) (f : G.obj (⊤_ C) ⊤_ D) [i : category_theory.is_iso f] :

If there is any isomorphism G.obj ⊤ ⟶ ⊤, then G preserves terminal objects.

Equations
noncomputable def category_theory.limits.preserves_terminal_of_iso {C : Type u₁} {D : Type u₂} (G : C D) (f : G.obj (⊤_ C) ⊤_ D) :

If there is any isomorphism G.obj ⊤ ≅ ⊤, then G preserves terminal objects.

Equations
noncomputable def category_theory.limits.preserves_terminal.iso {C : Type u₁} {D : Type u₂} (G : C D)  :
G.obj (⊤_ C) ⊤_ D

If G preserves terminal objects, then the terminal comparison map for G is an isomorphism.

Equations
@[simp]
@[protected, instance]
def category_theory.limits.is_colimit_map_cocone_empty_cocone_equiv {C : Type u₁} {D : Type u₂} (G : C D) (X : C) :

The map of an empty cocone is a colimit iff the mapped object is initial.

Equations
def category_theory.limits.is_initial.is_initial_obj {C : Type u₁} {D : Type u₂} (G : C D) (X : C)  :

The property of preserving initial objects expressed in terms of is_initial.

Equations
def category_theory.limits.is_initial.is_initial_of_obj {C : Type u₁} {D : Type u₂} (G : C D) (X : C) (l : category_theory.limits.is_initial (G.obj X)) :

The property of reflecting initial objects expressed in terms of is_initial.

Equations
noncomputable def category_theory.limits.is_colimit_of_has_initial_of_preserves_colimit {C : Type u₁} {D : Type u₂} (G : C D)  :

If G preserves the initial object and C has a initial object, then the image of the initial object is initial.

Equations
theorem category_theory.limits.has_initial_of_has_initial_of_preserves_colimit {C : Type u₁} {D : Type u₂} (G : C D)  :

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.

noncomputable def category_theory.limits.preserves_initial.of_iso_comparison {C : Type u₁} {D : Type u₂} (G : C D)  :

If the initial comparison map for G is an isomorphism, then G preserves initial objects.

Equations
noncomputable def category_theory.limits.preserves_initial_of_is_iso {C : Type u₁} {D : Type u₂} (G : C D) (f : ⊥_ D G.obj (⊥_ C)) [i : category_theory.is_iso f] :

If there is any isomorphism ⊥ ⟶ G.obj ⊥, then G preserves initial objects.

Equations
noncomputable def category_theory.limits.preserves_initial_of_iso {C : Type u₁} {D : Type u₂} (G : C D) (f : ⊥_ D G.obj (⊥_ C)) :

If there is any isomorphism ⊥ ≅ G.obj ⊥, then G preserves initial objects.

Equations
noncomputable def category_theory.limits.preserves_initial.iso {C : Type u₁} {D : Type u₂} (G : C D)  :
G.obj (⊥_ C) ⊥_ D

If G preserves initial objects, then the initial comparison map for G is an isomorphism.

Equations
@[simp]
@[protected, instance]