# Documentation

Mathlib.CategoryTheory.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 terminalComparison G is an isomorphism iff G preserves terminal objects.

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

Instances For
def CategoryTheory.Limits.IsTerminal.isTerminalObj {C : Type u₁} [] {D : Type u₂} [] (G : ) (X : C) :

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

Instances For
def CategoryTheory.Limits.IsTerminal.isTerminalOfObj {C : Type u₁} [] {D : Type u₂} [] (G : ) (X : C) (l : CategoryTheory.Limits.IsTerminal (G.obj X)) :

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

Instances For

Preserving the terminal object implies preserving all limits of the empty diagram.

Instances For

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

Instances For

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.

Instances For
def CategoryTheory.Limits.preservesTerminalOfIsIso {C : Type u₁} [] {D : Type u₂} [] (G : ) (f : G.obj (⊤_ C) ⊤_ D) [i : ] :

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

Instances For
def CategoryTheory.Limits.preservesTerminalOfIso {C : Type u₁} [] {D : Type u₂} [] (G : ) (f : G.obj (⊤_ C) ⊤_ D) :

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

Instances For
def CategoryTheory.Limits.PreservesTerminal.iso {C : Type u₁} [] {D : Type u₂} [] (G : ) :
G.obj (⊤_ C) ⊤_ D

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

Instances For
@[simp]

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

Instances For
def CategoryTheory.Limits.IsInitial.isInitialObj {C : Type u₁} [] {D : Type u₂} [] (G : ) (X : C) :

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

Instances For
def CategoryTheory.Limits.IsInitial.isInitialOfObj {C : Type u₁} [] {D : Type u₂} [] (G : ) (X : C) (l : CategoryTheory.Limits.IsInitial (G.obj X)) :

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

Instances For

Preserving the initial object implies preserving all colimits of the empty diagram.

Instances For

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

Instances For

If C has an initial object and G preserves initial objects, then D has an 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.

Instances For
def CategoryTheory.Limits.preservesInitialOfIsIso {C : Type u₁} [] {D : Type u₂} [] (G : ) (f : ⊥_ D G.obj (⊥_ C)) [i : ] :

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

Instances For
def CategoryTheory.Limits.preservesInitialOfIso {C : Type u₁} [] {D : Type u₂} [] (G : ) (f : ⊥_ D G.obj (⊥_ C)) :

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

Instances For
def CategoryTheory.Limits.PreservesInitial.iso {C : Type u₁} [] {D : Type u₂} [] (G : ) :
G.obj (⊥_ C) ⊥_ D

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

Instances For
@[simp]