mathlib documentation

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} [category_theory.category C] (X : C) (X_1 : category_theory.discrete pempty) :
(category_theory.limits.as_empty_cone X).π.app X_1 = category_theory.limits.as_empty_cone._aux_1 X X_1

Construct a cone for the empty diagram given an object.

Equations

Construct a cocone for the empty diagram given an object.

Equations
@[simp]
theorem category_theory.limits.as_empty_cocone_ι_app {C : Type u} [category_theory.category C] (X : C) (X_1 : category_theory.discrete pempty) :
(category_theory.limits.as_empty_cocone X).ι.app X_1 = category_theory.limits.as_empty_cocone._aux_1 X X_1

def category_theory.limits.is_terminal {C : Type u} [category_theory.category C] :
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} [category_theory.category C] :
C → Type (max u v)

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

Give the morphism to a terminal object from any other.

Equations

Any two morphisms to a terminal object are equal.

Give the morphism from an initial object to any other.

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

Any morphism from a terminal object is mono.

Any morphism to an initial object is epi.

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

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

Instances

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.

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.

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.

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.

The map from an object to the terminal object.

The map to an object from the initial object.

@[instance]

Any morphism from a terminal object is mono.

@[instance]

Any morphism to an initial object is epi.

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

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

Equations

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

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

Equations