# mathlibdocumentation

category_theory.limits.shapes.terminal

# Initial and terminal objects in a category. #

## References #

@[simp]
theorem category_theory.limits.as_empty_cone_π_app {C : Type u} (X : C)  :
= category_theory.limits.as_empty_cone._aux_1 X X_1
@[simp]
theorem category_theory.limits.as_empty_cone_X {C : Type u} (X : C) :
def category_theory.limits.as_empty_cone {C : Type u} (X : C) :

Construct a cone for the empty diagram given an object.

Equations
@[simp]
theorem category_theory.limits.as_empty_cocone_X {C : Type u} (X : C) :
def category_theory.limits.as_empty_cocone {C : Type u} (X : C) :

Construct a cocone for the empty diagram given an object.

Equations
@[simp]
theorem category_theory.limits.as_empty_cocone_ι_app {C : Type u} (X : C)  :
= category_theory.limits.as_empty_cocone._aux_1 X X_1
def category_theory.limits.is_terminal {C : Type u} (X : C) :
Type (max u v)

X is terminal if the cone it induces on the empty diagram is limiting.

def category_theory.limits.is_initial {C : Type u} (X : C) :
Type (max u v)

X is initial if the cocone it induces on the empty diagram is colimiting.

def category_theory.limits.is_terminal.of_unique {C : Type u} (Y : C) [h : Π (X : C), unique (X Y)] :

An object Y is terminal if for every X there is a unique morphism X ⟶ Y.

Equations
def category_theory.limits.is_terminal.of_iso {C : Type u} {Y Z : C} (i : Y Z) :

Transport a term of type is_terminal across an isomorphism.

Equations
def category_theory.limits.is_initial.of_unique {C : Type u} (X : C) [h : Π (Y : C), unique (X Y)] :

An object X is initial if for every Y there is a unique morphism X ⟶ Y.

Equations
def category_theory.limits.is_initial.of_iso {C : Type u} {X Y : C} (i : X Y) :

Transport a term of type is_initial across an isomorphism.

Equations
def category_theory.limits.is_terminal.from {C : Type u} {X : C} (Y : C) :
Y X

Give the morphism to a terminal object from any other.

Equations
theorem category_theory.limits.is_terminal.hom_ext {C : Type u} {X Y : C} (f g : Y X) :
f = g

Any two morphisms to a terminal object are equal.

@[simp]
theorem category_theory.limits.is_terminal.comp_from {C : Type u} {Z : C} {X Y : C} (f : X Y) :
f t.from Y = t.from X
@[simp]
theorem category_theory.limits.is_terminal.from_self {C : Type u} {X : C}  :
t.from X = 𝟙 X
def category_theory.limits.is_initial.to {C : Type u} {X : C} (Y : C) :
X Y

Give the morphism from an initial object to any other.

Equations
theorem category_theory.limits.is_initial.hom_ext {C : Type u} {X Y : C} (f g : X Y) :
f = g

Any two morphisms from an initial object are equal.

@[simp]
theorem category_theory.limits.is_initial.to_comp {C : Type u} {X : C} {Y Z : C} (f : Y Z) :
t.to Y f = t.to Z
@[simp]
theorem category_theory.limits.is_initial.to_self {C : Type u} {X : C}  :
t.to X = 𝟙 X
def category_theory.limits.is_terminal.split_mono_from {C : Type u} {X Y : C} (f : X Y) :

Any morphism from a terminal object is split mono.

Equations
def category_theory.limits.is_initial.split_epi_to {C : Type u} {X Y : C} (f : Y X) :

Any morphism to an initial object is split epi.

Equations
theorem category_theory.limits.is_terminal.mono_from {C : Type u} {X Y : C} (f : X Y) :

Any morphism from a terminal object is mono.

theorem category_theory.limits.is_initial.epi_to {C : Type u} {X Y : C} (f : Y X) :

Any morphism to an initial object is epi.

If T and T' are terminal, they are isomorphic.

Equations
@[simp]

If I and I' are initial, they are isomorphic.

Equations
@[simp]
def category_theory.limits.has_terminal (C : Type u)  :
Prop

A category has a terminal object if it has a limit over the empty diagram. Use has_terminal_of_unique to construct instances.

def category_theory.limits.has_initial (C : Type u)  :
Prop

A category has an initial object if it has a colimit over the empty diagram. Use has_initial_of_unique to construct instances.

def category_theory.limits.terminal (C : Type u)  :
C

An arbitrary choice of terminal object, if one exists. You can use the notation ⊤_ C. This object is characterized by having a unique morphism from any object.

def category_theory.limits.initial (C : Type u)  :
C

An arbitrary choice of initial object, if one exists. You can use the notation ⊥_ C. This object is characterized by having a unique morphism to any object.

theorem category_theory.limits.has_terminal_of_unique {C : Type u} (X : C) [h : Π (Y : C), unique (Y X)] :

We can more explicitly show that a category has a terminal object by specifying the object, and showing there is a unique morphism to it from any other object.

theorem category_theory.limits.has_initial_of_unique {C : Type u} (X : C) [h : Π (Y : C), unique (X Y)] :

We can more explicitly show that a category has an initial object by specifying the object, and showing there is a unique morphism from it to any other object.

def category_theory.limits.terminal.from {C : Type u} (P : C) :
P ⊤_ C

The map from an object to the terminal object.

def category_theory.limits.initial.to {C : Type u} (P : C) :
⊥_ C P

The map to an object from the initial object.

@[instance]
def category_theory.limits.unique_to_terminal {C : Type u} (P : C) :
Equations
@[instance]
def category_theory.limits.unique_from_initial {C : Type u} (P : C) :
Equations
@[simp]
theorem category_theory.limits.terminal.comp_from {C : Type u} {P Q : C} (f : P Q) :
@[simp]
theorem category_theory.limits.initial.to_comp {C : Type u} {P Q : C} (f : P Q) :

A terminal object is terminal.

Equations

An initial object is initial.

Equations
@[instance]
def category_theory.limits.terminal.split_mono_from {C : Type u} {Y : C} (f : ⊤_ C Y) :

Any morphism from a terminal object is split mono.

Equations
@[instance]
def category_theory.limits.initial.split_epi_to {C : Type u} {Y : C} (f : Y ⊥_ C) :

Any morphism to an initial object is split epi.

Equations
def category_theory.limits.terminal_op_of_initial {C : Type u} {X : C}  :

An initial object is terminal in the opposite category.

Equations

An initial object in the opposite category is terminal in the original category.

Equations
def category_theory.limits.initial_op_of_terminal {C : Type u} {X : C}  :

A terminal object is initial in the opposite category.

Equations

A terminal object in the opposite category is initial in the original category.

Equations
@[class]
structure category_theory.limits.initial_mono_class (C : Type u)  :
Prop

A category is a initial_mono_class if the canonical morphism of an initial object is a monomorphism. In practice, this is most useful when given an arbitrary morphism out of the chosen initial object, see initial.mono_from. Given a terminal object, this is equivalent to the assumption that the unique morphism from initial to terminal is a monomorphism, which is the second of Freyd's axioms for an AT category.

TODO: This is a condition satisfied by categories with zero objects and morphisms.

Instances
theorem category_theory.limits.is_initial.mono_from {C : Type u} {I X : C} (f : I X) :
@[instance]
def category_theory.limits.initial.mono_from {C : Type u} (X : C) (f : ⊥_ C X) :
theorem category_theory.limits.initial_mono_class.of_is_initial {C : Type u} {I : C} (h : ∀ (X : C), category_theory.mono (hI.to X)) :

To show a category is a initial_mono_class it suffices to give an initial object such that every morphism out of it is a monomorphism.

theorem category_theory.limits.initial_mono_class.of_initial {C : Type u} (h : ∀ (X : C), ) :

To show a category is a initial_mono_class it suffices to show every morphism out of the initial object is a monomorphism.

To show a category is a initial_mono_class it suffices to show the unique morphism from an initial object to a terminal object is a monomorphism.

To show a category is a initial_mono_class it suffices to show the unique morphism from the initial object to a terminal object is a monomorphism.

def category_theory.limits.terminal_comparison {C : Type u} {D : Type u₂} (G : C D)  :
G.obj (⊤_ C) ⊤_ D

The comparison morphism from the image of a terminal object to the terminal object in the target category. This is an isomorphism iff G preserves terminal objects, see category_theory.limits.preserves_terminal.of_iso_comparison.

Equations
def category_theory.limits.initial_comparison {C : Type u} {D : Type u₂} (G : C D)  :
⊥_ D G.obj (⊥_ C)

The comparison morphism from the initial object in the target category to the image of the initial object.

Equations
def category_theory.limits.cone_of_diagram_initial {C : Type u} {J : Type v} {X : J} (F : J C) :

From a functor F : J ⥤ C, given an initial object of J, construct a cone for J. In limit_of_diagram_initial we show it is a limit cone.

Equations
@[simp]
theorem category_theory.limits.cone_of_diagram_initial_π_app {C : Type u} {J : Type v} {X : J} (F : J C) (j : J) :
= F.map (tX.to j)
@[simp]
theorem category_theory.limits.cone_of_diagram_initial_X {C : Type u} {J : Type v} {X : J} (F : J C) :
def category_theory.limits.limit_of_diagram_initial {C : Type u} {J : Type v} {X : J} (F : J C) :

From a functor F : J ⥤ C, given an initial object of J, show the cone cone_of_diagram_initial is a limit.

Equations
def category_theory.limits.limit_of_initial {C : Type u} {J : Type v} (F : J C)  :
F.obj (⊥_ J)

For a functor F : J ⥤ C, if J has an initial object then the image of it is isomorphic to the limit of F.

Equations
@[simp]
theorem category_theory.limits.cocone_of_diagram_terminal_ι_app {C : Type u} {J : Type v} {X : J} (F : J C) (j : J) :
= F.map (tX.from j)
def category_theory.limits.cocone_of_diagram_terminal {C : Type u} {J : Type v} {X : J} (F : J C) :

From a functor F : J ⥤ C, given a terminal object of J, construct a cocone for J. In colimit_of_diagram_terminal we show it is a colimit cocone.

Equations
@[simp]
theorem category_theory.limits.cocone_of_diagram_terminal_X {C : Type u} {J : Type v} {X : J} (F : J C) :
def category_theory.limits.colimit_of_diagram_terminal {C : Type u} {J : Type v} {X : J} (F : J C) :

From a functor F : J ⥤ C, given a terminal object of J, show the cocone cocone_of_diagram_terminal is a colimit.

Equations
def category_theory.limits.colimit_of_terminal {C : Type u} {J : Type v} (F : J C)  :
F.obj (⊤_ J)

For a functor F : J ⥤ C, if J has a terminal object then the image of it is isomorphic to the colimit of F.

Equations
theorem category_theory.limits.is_iso_π_of_is_initial {C : Type u} {J : Type v} {j : J} (F : J C)  :

If j is initial in the index category, then the map limit.π F j is an isomorphism.

@[instance]
def category_theory.limits.is_iso_π_initial {C : Type u} {J : Type v} (F : J C)  :
theorem category_theory.limits.is_iso_ι_of_is_terminal {C : Type u} {J : Type v} {j : J} (F : J C)  :

If j is terminal in the index category, then the map colimit.ι F j is an isomorphism.

@[instance]
def category_theory.limits.is_iso_ι_terminal {C : Type u} {J : Type v} (F : J C)  :