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] (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} [category_theory.category C] (X : C) :
Type (max u v)

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

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

Equations

Transport a term of type is_terminal across an isomorphism.

Equations

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

Equations

Transport a term of type is_initial across an isomorphism.

Equations

Give the morphism to a terminal object from any other.

Equations

Any two morphisms to a terminal object are equal.

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

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.

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

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.

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

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

Equations

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

Equations

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

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