mathlib documentation

category_theory.limits.shapes.terminal

Initial and terminal objects in a category.

References

source
def category_theory.limits.as_empty_cone {C : Type u} [category_theory.category C] (X : C) :
category_theory.limits.cone (category_theory.functor.empty C)

Construct a cone for the empty diagram given an object.

Equations
source
def category_theory.limits.as_empty_cocone {C : Type u} [category_theory.category C] (X : C) :
category_theory.limits.cocone (category_theory.functor.empty C)

Construct a cocone for the empty diagram given an object.

Equations
source
def category_theory.limits.is_terminal {C : Type u} [category_theory.category C] (X : C) :
Type (max u v)

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

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

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

source
def category_theory.limits.is_terminal.from {C : Type u} [category_theory.category C] {X : C} (t : category_theory.limits.is_terminal X) (Y : C) :
Y ⟶ X

Give the morphism to a terminal object from any other.

Equations
source
theorem category_theory.limits.is_terminal.hom_ext {C : Type u} [category_theory.category C] {X Y : C} (t : category_theory.limits.is_terminal X) (f g : Y ⟶ X) :
f = g

Any two morphisms to a terminal object are equal.

source
def category_theory.limits.is_initial.to {C : Type u} [category_theory.category C] {X : C} (t : category_theory.limits.is_initial X) (Y : C) :
X ⟶ Y

Give the morphism from an initial object to any other.

Equations
source
theorem category_theory.limits.is_initial.hom_ext {C : Type u} [category_theory.category C] {X Y : C} (t : category_theory.limits.is_initial X) (f g : X ⟶ Y) :
f = g

Any two morphisms from an initial object are equal.

source
theorem category_theory.limits.is_terminal.mono_from {C : Type u} [category_theory.category C] {X Y : C} (t : category_theory.limits.is_terminal X) (f : X ⟶ Y) :
category_theory.mono f

Any morphism from a terminal object is mono.

source
theorem category_theory.limits.is_initial.epi_to {C : Type u} [category_theory.category C] {X Y : C} (t : category_theory.limits.is_initial X) (f : Y ⟶ X) :
category_theory.epi f

Any morphism to an initial object is epi.

source
def category_theory.limits.has_terminal (C : Type u) [category_theory.category C] :
Prop

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

source
def category_theory.limits.has_initial (C : Type u) [category_theory.category C] :
Prop

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

Instances
source
def category_theory.limits.terminal (C : Type u) [category_theory.category C] [category_theory.limits.has_terminal C] :
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.

source
def category_theory.limits.initial (C : Type u) [category_theory.category C] [category_theory.limits.has_initial C] :
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.

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

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.

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

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.

source
def category_theory.limits.terminal.from {C : Type u} [category_theory.category C] [category_theory.limits.has_terminal C] (P : C) :
P ⟶ ⊤_C

The map from an object to the terminal object.

source
def category_theory.limits.initial.to {C : Type u} [category_theory.category C] [category_theory.limits.has_initial C] (P : C) :
⊥_C ⟶ P

The map to an object from the initial object.

source
@[instance]
def category_theory.limits.unique_to_terminal {C : Type u} [category_theory.category C] [category_theory.limits.has_terminal C] (P : C) :
unique (P ⟶ ⊤_C)

Equations
source
@[instance]
def category_theory.limits.unique_from_initial {C : Type u} [category_theory.category C] [category_theory.limits.has_initial C] (P : C) :
unique (⊥_C ⟶ P)

Equations
source
def category_theory.limits.terminal_is_terminal {C : Type u} [category_theory.category C] [category_theory.limits.has_terminal C] :
category_theory.limits.is_terminal (⊤_C)

A terminal object is terminal.

Equations
source
def category_theory.limits.initial_is_initial {C : Type u} [category_theory.category C] [category_theory.limits.has_initial C] :
category_theory.limits.is_initial (⊥_C)

An initial object is initial.

Equations
source
@[instance]
def category_theory.limits.terminal.mono_from {C : Type u} [category_theory.category C] {Y : C} [category_theory.limits.has_terminal C] (f : ⊤_C ⟶ Y) :
category_theory.mono f

Any morphism from a terminal object is mono.

source
@[instance]
def category_theory.limits.initial.epi_to {C : Type u} [category_theory.category C] {Y : C} [category_theory.limits.has_initial C] (f : Y ⟶ ⊥_C) :
category_theory.epi f

Any morphism to an initial object is epi.