# 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) :

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) :

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
@[reducible]
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.

@[reducible]
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_equiv_unique {C : Type u₁} (Y : C) :
category_theory.limits.is_limit {X := Y, π := {app := category_theory.limits.is_terminal_equiv_unique._aux_1 F Y, naturality' := _}} Π (X : C), unique (X Y)

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

Equations
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 (as an instance).

Equations

If α is a preorder with top, then ⊤ is a terminal object.

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_equiv_unique {C : Type u₁} (X : C) :
category_theory.limits.is_colimit {X := X, ι := {app := category_theory.limits.is_initial_equiv_unique._aux_1 F X, naturality' := _}} Π (Y : C), unique (X Y)

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

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 (as an instance).

Equations

If α is a preorder with bot, then ⊥ is an initial object.

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
theorem category_theory.limits.is_terminal.is_split_mono_from {C : Type u₁} {X Y : C} (f : X Y) :

Any morphism from a terminal object is split mono.

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

Any morphism to an initial object is split epi.

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

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

Equations
@[reducible]
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.

@[reducible]
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.is_limit_change_empty_cone (C : Type u₁) {F₁ : C} {F₂ : C} {c₁ : category_theory.limits.cone F₁} (hl : category_theory.limits.is_limit c₁) (c₂ : category_theory.limits.cone F₂) (hi : c₁.X c₂.X) :

Being terminal is independent of the empty diagram, its universe, and the cone over it, as long as the cone points are isomorphic.

Equations
def category_theory.limits.is_limit_empty_cone_equiv (C : Type u₁) {F₁ : C} {F₂ : C} (c₁ : category_theory.limits.cone F₁) (c₂ : category_theory.limits.cone F₂) (h : c₁.X c₂.X) :

Replacing an empty cone in is_limit by another with the same cone point is an equivalence.

Equations
theorem category_theory.limits.has_terminal_change_diagram (C : Type u₁) {F₁ : C} {F₂ : C}  :
def category_theory.limits.is_colimit_change_empty_cocone (C : Type u₁) {F₁ : C} {F₂ : C} {c₁ : category_theory.limits.cocone F₁} (c₂ : category_theory.limits.cocone F₂) (hi : c₁.X c₂.X) :

Being initial is independent of the empty diagram, its universe, and the cocone over it, as long as the cocone points are isomorphic.

Equations
def category_theory.limits.is_colimit_empty_cocone_equiv (C : Type u₁) {F₁ : C} {F₂ : C} (c₁ : category_theory.limits.cocone F₁) (c₂ : category_theory.limits.cocone F₂) (h : c₁.X c₂.X) :

Replacing an empty cocone in is_colimit by another with the same cocone point is an equivalence.

Equations
theorem category_theory.limits.has_initial_change_diagram (C : Type u₁) {F₁ : C} {F₂ : C}  :
@[reducible]
noncomputable 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.

@[reducible]
noncomputable 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.

@[reducible]
noncomputable def category_theory.limits.terminal.from {C : Type u₁} (P : C) :
P ⊤_ C

The map from an object to the terminal object.

@[reducible]
noncomputable def category_theory.limits.initial.to {C : Type u₁} (P : C) :
⊥_ C P

The map to an object from the initial object.

noncomputable def category_theory.limits.terminal_is_terminal {C : Type u₁}  :

A terminal object is terminal.

Equations
noncomputable def category_theory.limits.initial_is_initial {C : Type u₁}  :

An initial object is initial.

Equations
@[protected, instance]
noncomputable def category_theory.limits.unique_to_terminal {C : Type u₁} (P : C) :
Equations
@[protected, instance]
noncomputable 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) :
@[simp]
noncomputable def category_theory.limits.initial_iso_is_initial {C : Type u₁} {P : C}  :
⊥_ C P

The (unique) isomorphism between the chosen initial object and any other initial object.

Equations
@[simp]
noncomputable def category_theory.limits.terminal_iso_is_terminal {C : Type u₁} {P : C}  :
⊤_ C P

The (unique) isomorphism between the chosen terminal object and any other terminal object.

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

Any morphism from a terminal object is split mono.

@[protected, instance]
def category_theory.limits.initial.is_split_epi_to {C : Type u₁} {Y : C} (f : Y ⊥_ C) :

Any morphism to an initial object is split epi.

An initial object is terminal in the opposite category.

Equations

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

Equations

A terminal object is initial in the opposite category.

Equations

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

Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
def category_theory.limits.obj.has_limit {J : Type u_1} {C : Type u_3}  :
@[simp]
noncomputable def category_theory.limits.limit_const_terminal {J : Type u_1} {C : Type u_3}  :

The limit of the constant ⊤_ C functor is ⊤_ C.

Equations
@[simp]
@[simp]
theorem category_theory.limits.limit_const_terminal_inv_π_assoc {J : Type u_1} {C : Type u_3} {j : J} {X' : C} (f' : (⊤_ C)).obj j X') :
@[protected, instance]
def category_theory.limits.obj.has_colimit {J : Type u_1} {C : Type u_3}  :
@[simp]
noncomputable def category_theory.limits.colimit_const_initial {J : Type u_1} {C : Type u_3}  :

The colimit of the constant ⊥_ C functor is ⊥_ C.

Equations
@[simp]
@[simp]
theorem category_theory.limits.ι_colimit_const_initial_hom_assoc {J : Type u_1} {C : Type u_3} {j : J} {X' : C} (f' : ⊥_ C X') :
@[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 of this typeclass
theorem category_theory.limits.is_initial.mono_from {C : Type u₁} {I X : C} (f : I X) :
@[protected, 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.

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.

noncomputable 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
Instances for category_theory.limits.terminal_comparison
noncomputable 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
Instances for category_theory.limits.initial_comparison
def category_theory.limits.cone_of_diagram_initial {C : Type u₁} {J : Type u} {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 u} {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 u} {X : J} (F : J C) :
def category_theory.limits.limit_of_diagram_initial {C : Type u₁} {J : Type u} {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
@[reducible]
noncomputable def category_theory.limits.limit_of_initial {C : Type u₁} {J : Type u} (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.cone_of_diagram_terminal_X {C : Type u₁} {J : Type u} {X : J} (F : J C) [ (i j : J) (f : i j), ] :
noncomputable def category_theory.limits.cone_of_diagram_terminal {C : Type u₁} {J : Type u} {X : J} (F : J C) [ (i j : J) (f : i j), ] :

From a functor F : J ⥤ C, given a terminal object of J, construct a cone for J, provided that the morphisms in the diagram are isomorphisms. In limit_of_diagram_terminal we show it is a limit cone.

Equations
@[simp]
theorem category_theory.limits.cone_of_diagram_terminal_π_app {C : Type u₁} {J : Type u} {X : J} (F : J C) [ (i j : J) (f : i j), ] (i : J) :
def category_theory.limits.limit_of_diagram_terminal {C : Type u₁} {J : Type u} {X : J} (F : J C) [ (i j : J) (f : i j), ] :

From a functor F : J ⥤ C, given a terminal object of J and that the morphisms in the diagram are isomorphisms, show the cone cone_of_diagram_terminal is a limit.

Equations
@[reducible]
noncomputable def category_theory.limits.limit_of_terminal {C : Type u₁} {J : Type u} (F : J C) [ (i j : J) (f : i j), ] :
F.obj (⊤_ J)

For a functor F : J ⥤ C, if J has a terminal object and all the morphisms in the diagram are isomorphisms, then the image of the terminal object is isomorphic to the limit of F.

Equations
@[simp]
theorem category_theory.limits.cocone_of_diagram_terminal_ι_app {C : Type u₁} {J : Type u} {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 u} {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 u} {X : J} (F : J C) :
def category_theory.limits.colimit_of_diagram_terminal {C : Type u₁} {J : Type u} {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
@[reducible]
noncomputable def category_theory.limits.colimit_of_terminal {C : Type u₁} {J : Type u} (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
@[simp]
theorem category_theory.limits.cocone_of_diagram_initial_X {C : Type u₁} {J : Type u} {X : J} (F : J C) [ (i j : J) (f : i j), ] :
noncomputable def category_theory.limits.cocone_of_diagram_initial {C : Type u₁} {J : Type u} {X : J} (F : J C) [ (i j : J) (f : i j), ] :

From a functor F : J ⥤ C, given an initial object of J, construct a cocone for J, provided that the morphisms in the diagram are isomorphisms. In colimit_of_diagram_initial we show it is a colimit cocone.

Equations
@[simp]
theorem category_theory.limits.cocone_of_diagram_initial_ι_app {C : Type u₁} {J : Type u} {X : J} (F : J C) [ (i j : J) (f : i j), ] (i : J) :
def category_theory.limits.colimit_of_diagram_initial {C : Type u₁} {J : Type u} {X : J} (F : J C) [ (i j : J) (f : i j), ] :

From a functor F : J ⥤ C, given an initial object of J and that the morphisms in the diagram are isomorphisms, show the cone cocone_of_diagram_initial is a colimit.

Equations
@[reducible]
noncomputable def category_theory.limits.colimit_of_initial {C : Type u₁} {J : Type u} (F : J C) [ (i j : J) (f : i j), ] :
F.obj (⊥_ J)

For a functor F : J ⥤ C, if J has an initial object and all the morphisms in the diagram are isomorphisms, then the image of the initial object is isomorphic to the colimit of F.

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

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

@[protected, instance]
def category_theory.limits.is_iso_π_initial {C : Type u₁} {J : Type u} (F : J C)  :
theorem category_theory.limits.is_iso_π_of_is_terminal {C : Type u₁} {J : Type u} {j : J} (F : J C) [ (i j : J) (f : i j), ] :
@[protected, instance]
def category_theory.limits.is_iso_π_terminal {C : Type u₁} {J : Type u} (F : J C) [ (i j : J) (f : i j), ] :
theorem category_theory.limits.is_iso_ι_of_is_terminal {C : Type u₁} {J : Type u} {j : J} (F : J C)  :

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

@[protected, instance]
def category_theory.limits.is_iso_ι_terminal {C : Type u₁} {J : Type u} (F : J C)  :
theorem category_theory.limits.is_iso_ι_of_is_initial {C : Type u₁} {J : Type u} {j : J} (F : J C) [ (i j : J) (f : i j), ] :
@[protected, instance]
def category_theory.limits.is_iso_ι_initial {C : Type u₁} {J : Type u} (F : J C) [ (i j : J) (f : i j), ] :