Initial and terminal objects in a category.

In this file we define the predicates IsTerminal and IsInitial as well as the class InitialMonoClass.

The classes HasTerminal and HasInitial and the associated notations for terminal and initial objects are defined in Terminal.lean.

References

• Stacks: Initial and final objects

def CategoryTheory.Limits.asEmptyCone {C : Type u₁} [Category.{v₁, u₁} C] (X : C) : Cone (Functor.empty C)

Construct a cone for the empty diagram given an object.

@[simp]

theorem CategoryTheory.Limits.asEmptyCone_pt {C : Type u₁} [Category.{v₁, u₁} C] (X : C) : (asEmptyCone X).pt = X

@[simp]

theorem CategoryTheory.Limits.asEmptyCone_π_app {C : Type u₁} [Category.{v₁, u₁} C] (X : C) (X_1 : Discrete PEmpty.{1}) : (asEmptyCone X).π.app X_1 = id (Discrete.casesOn X_1 fun (as : PEmpty.{1}) => ⋯.elim)

def CategoryTheory.Limits.asEmptyCocone {C : Type u₁} [Category.{v₁, u₁} C] (X : C) : Cocone (Functor.empty C)

Construct a cocone for the empty diagram given an object.

@[simp]

theorem CategoryTheory.Limits.asEmptyCocone_pt {C : Type u₁} [Category.{v₁, u₁} C] (X : C) : (asEmptyCocone X).pt = X

@[simp]

theorem CategoryTheory.Limits.asEmptyCocone_ι_app {C : Type u₁} [Category.{v₁, u₁} C] (X : C) (X_1 : Discrete PEmpty.{1}) : (asEmptyCocone X).ι.app X_1 = id (Discrete.casesOn X_1 fun (as : PEmpty.{1}) => ⋯.elim)

@[reducible, inline]

abbrev CategoryTheory.Limits.IsTerminal {C : Type u₁} [Category.{v₁, u₁} C] (X : C) : Type (max u₁ v₁)

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

@[reducible, inline]

abbrev CategoryTheory.Limits.IsInitial {C : Type u₁} [Category.{v₁, u₁} C] (X : C) : Type (max u₁ v₁)

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

def CategoryTheory.Limits.isTerminalEquivUnique {C : Type u₁} [Category.{v₁, u₁} C] (F : Functor (Discrete PEmpty.{1}) C) (Y : C) : IsLimit { pt := Y, π := { app := fun (X : Discrete PEmpty.{1}) => id (Discrete.casesOn X fun (as : PEmpty.{1}) => ⋯.elim), naturality := ⋯ } } ≃ ((X : C) → Unique (X ⟶ Y))

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

def CategoryTheory.Limits.IsTerminal.ofUnique {C : Type u₁} [Category.{v₁, u₁} C] (Y : C) [h : (X : C) → Unique (X ⟶ Y)] : IsTerminal Y

An object Y is terminal if for every X there is a unique morphism X ⟶ Y (as an instance).

def CategoryTheory.Limits.IsTerminal.ofUniqueHom {C : Type u₁} [Category.{v₁, u₁} C] {Y : C} (h : (X : C) → X ⟶ Y) (uniq : ∀ (X : C) (m : X ⟶ Y), m = h X) : IsTerminal Y

An object Y is terminal if for every X there is a unique morphism X ⟶ Y (as explicit arguments).

def CategoryTheory.Limits.isTerminalTop {α : Type u_1} [Preorder α] [OrderTop α] : IsTerminal ⊤

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

def CategoryTheory.Limits.IsTerminal.ofIso {C : Type u₁} [Category.{v₁, u₁} C] {Y Z : C} (hY : IsTerminal Y) (i : Y ≅ Z) : IsTerminal Z

Transport a term of type IsTerminal across an isomorphism.

def CategoryTheory.Limits.IsTerminal.equivOfIso {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (e : X ≅ Y) : IsTerminal X ≃ IsTerminal Y

If X and Y are isomorphic, then X is terminal iff Y is.

def CategoryTheory.Limits.isInitialEquivUnique {C : Type u₁} [Category.{v₁, u₁} C] (F : Functor (Discrete PEmpty.{1}) C) (X : C) : IsColimit { pt := X, ι := { app := fun (X_1 : Discrete PEmpty.{1}) => id (Discrete.casesOn X_1 fun (as : PEmpty.{1}) => ⋯.elim), naturality := ⋯ } } ≃ ((Y : C) → Unique (X ⟶ Y))

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

def CategoryTheory.Limits.IsInitial.ofUnique {C : Type u₁} [Category.{v₁, u₁} C] (X : C) [h : (Y : C) → Unique (X ⟶ Y)] : IsInitial X

An object X is initial if for every Y there is a unique morphism X ⟶ Y (as an instance).

def CategoryTheory.Limits.IsInitial.ofUniqueHom {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (h : (Y : C) → X ⟶ Y) (uniq : ∀ (Y : C) (m : X ⟶ Y), m = h Y) : IsInitial X

An object X is initial if for every Y there is a unique morphism X ⟶ Y (as explicit arguments).

def CategoryTheory.Limits.isInitialBot {α : Type u_1} [Preorder α] [OrderBot α] : IsInitial ⊥

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

def CategoryTheory.Limits.IsInitial.ofIso {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (hX : IsInitial X) (i : X ≅ Y) : IsInitial Y

Transport a term of type is_initial across an isomorphism.

def CategoryTheory.Limits.IsInitial.equivOfIso {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (e : X ≅ Y) : IsInitial X ≃ IsInitial Y

If X and Y are isomorphic, then X is initial iff Y is.

def CategoryTheory.Limits.IsTerminal.from {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (t : IsTerminal X) (Y : C) : Y ⟶ X

Give the morphism to a terminal object from any other.

theorem CategoryTheory.Limits.IsTerminal.hom_ext {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (t : IsTerminal X) (f g : Y ⟶ X) : f = g

Any two morphisms to a terminal object are equal.

@[simp]

theorem CategoryTheory.Limits.IsTerminal.comp_from {C : Type u₁} [Category.{v₁, u₁} C] {Z : C} (t : IsTerminal Z) {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp f (t.from Y) = t.from X

@[simp]

theorem CategoryTheory.Limits.IsTerminal.from_self {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (t : IsTerminal X) : t.from X = CategoryStruct.id X

def CategoryTheory.Limits.IsInitial.to {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (t : IsInitial X) (Y : C) : X ⟶ Y

Give the morphism from an initial object to any other.

theorem CategoryTheory.Limits.IsInitial.hom_ext {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (t : IsInitial X) (f g : X ⟶ Y) : f = g

Any two morphisms from an initial object are equal.

@[simp]

theorem CategoryTheory.Limits.IsInitial.to_comp {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (t : IsInitial X) {Y Z : C} (f : Y ⟶ Z) : CategoryStruct.comp (t.to Y) f = t.to Z

@[simp]

theorem CategoryTheory.Limits.IsInitial.to_self {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (t : IsInitial X) : t.to X = CategoryStruct.id X

theorem CategoryTheory.Limits.IsTerminal.isSplitMono_from {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (t : IsTerminal X) (f : X ⟶ Y) : IsSplitMono f

Any morphism from a terminal object is split mono.

theorem CategoryTheory.Limits.IsInitial.isSplitEpi_to {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (t : IsInitial X) (f : Y ⟶ X) : IsSplitEpi f

Any morphism to an initial object is split epi.

theorem CategoryTheory.Limits.IsTerminal.mono_from {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (t : IsTerminal X) (f : X ⟶ Y) : Mono f

Any morphism from a terminal object is mono.

theorem CategoryTheory.Limits.IsInitial.epi_to {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (t : IsInitial X) (f : Y ⟶ X) : Epi f

Any morphism to an initial object is epi.

def CategoryTheory.Limits.IsTerminal.uniqueUpToIso {C : Type u₁} [Category.{v₁, u₁} C] {T T' : C} (hT : IsTerminal T) (hT' : IsTerminal T') : T ≅ T'

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

@[simp]

theorem CategoryTheory.Limits.IsTerminal.uniqueUpToIso_inv {C : Type u₁} [Category.{v₁, u₁} C] {T T' : C} (hT : IsTerminal T) (hT' : IsTerminal T') : (hT.uniqueUpToIso hT').inv = hT.from T'

@[simp]

theorem CategoryTheory.Limits.IsTerminal.uniqueUpToIso_hom {C : Type u₁} [Category.{v₁, u₁} C] {T T' : C} (hT : IsTerminal T) (hT' : IsTerminal T') : (hT.uniqueUpToIso hT').hom = hT'.from T

def CategoryTheory.Limits.IsInitial.uniqueUpToIso {C : Type u₁} [Category.{v₁, u₁} C] {I I' : C} (hI : IsInitial I) (hI' : IsInitial I') : I ≅ I'

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

@[simp]

theorem CategoryTheory.Limits.IsInitial.uniqueUpToIso_inv {C : Type u₁} [Category.{v₁, u₁} C] {I I' : C} (hI : IsInitial I) (hI' : IsInitial I') : (hI.uniqueUpToIso hI').inv = hI'.to I

@[simp]

theorem CategoryTheory.Limits.IsInitial.uniqueUpToIso_hom {C : Type u₁} [Category.{v₁, u₁} C] {I I' : C} (hI : IsInitial I) (hI' : IsInitial I') : (hI.uniqueUpToIso hI').hom = hI.to I'

def CategoryTheory.Limits.isLimitChangeEmptyCone (C : Type u₁) [Category.{v₁, u₁} C] {F₁ : Functor (Discrete PEmpty.{w + 1}) C} {F₂ : Functor (Discrete PEmpty.{w' + 1}) C} {c₁ : Cone F₁} (hl : IsLimit c₁) (c₂ : Cone F₂) (hi : c₁.pt ≅ c₂.pt) : IsLimit c₂

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

def CategoryTheory.Limits.isLimitEmptyConeEquiv (C : Type u₁) [Category.{v₁, u₁} C] {F₁ : Functor (Discrete PEmpty.{w + 1}) C} {F₂ : Functor (Discrete PEmpty.{w' + 1}) C} (c₁ : Cone F₁) (c₂ : Cone F₂) (h : c₁.pt ≅ c₂.pt) : IsLimit c₁ ≃ IsLimit c₂

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

noncomputable def CategoryTheory.Limits.isLimitEquivIsTerminalOfIsEmpty (C : Type u₁) [Category.{v₁, u₁} C] {J : Type u_1} [Category.{u_2, u_1} J] [IsEmpty J] {F : Functor J C} (c : Cone F) : IsLimit c ≃ IsTerminal c.pt

If F is an empty diagram, then a cone over F is limiting iff the cone point is terminal.

def CategoryTheory.Limits.isColimitChangeEmptyCocone (C : Type u₁) [Category.{v₁, u₁} C] {F₁ : Functor (Discrete PEmpty.{w + 1}) C} {F₂ : Functor (Discrete PEmpty.{w' + 1}) C} {c₁ : Cocone F₁} (hl : IsColimit c₁) (c₂ : Cocone F₂) (hi : c₁.pt ≅ c₂.pt) : IsColimit c₂

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

def CategoryTheory.Limits.isColimitEmptyCoconeEquiv (C : Type u₁) [Category.{v₁, u₁} C] {F₁ : Functor (Discrete PEmpty.{w + 1}) C} {F₂ : Functor (Discrete PEmpty.{w' + 1}) C} (c₁ : Cocone F₁) (c₂ : Cocone F₂) (h : c₁.pt ≅ c₂.pt) : IsColimit c₁ ≃ IsColimit c₂

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

noncomputable def CategoryTheory.Limits.isColimitEquivIsInitialOfIsEmpty (C : Type u₁) [Category.{v₁, u₁} C] {J : Type u_1} [Category.{u_2, u_1} J] [IsEmpty J] {F : Functor J C} (c : Cocone F) : IsColimit c ≃ IsInitial c.pt

If F is an empty diagram, then a cocone over F is colimiting iff the cocone point is initial.

def CategoryTheory.Limits.terminalOpOfInitial {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (t : IsInitial X) : IsTerminal (Opposite.op X)

An initial object is terminal in the opposite category.

def CategoryTheory.Limits.terminalUnopOfInitial {C : Type u₁} [Category.{v₁, u₁} C] {X : Cᵒᵖ} (t : IsInitial X) : IsTerminal (Opposite.unop X)

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

def CategoryTheory.Limits.initialOpOfTerminal {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (t : IsTerminal X) : IsInitial (Opposite.op X)

A terminal object is initial in the opposite category.

def CategoryTheory.Limits.initialUnopOfTerminal {C : Type u₁} [Category.{v₁, u₁} C] {X : Cᵒᵖ} (t : IsTerminal X) : IsInitial (Opposite.unop X)

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

class CategoryTheory.Limits.InitialMonoClass (C : Type u₁) [Category.{v₁, u₁} C] : Prop

A category is an InitialMonoClass 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.

• isInitial_mono_from {I : C} (X : C) (hI : IsInitial I) : Mono (hI.to X)

  The map from the (any as stated) initial object to any other object is a monomorphism

theorem CategoryTheory.Limits.IsInitial.mono_from {C : Type u₁} [Category.{v₁, u₁} C] [InitialMonoClass C] {I X : C} (hI : IsInitial I) (f : I ⟶ X) : Mono f

theorem CategoryTheory.Limits.InitialMonoClass.of_isInitial {C : Type u₁} [Category.{v₁, u₁} C] {I : C} (hI : IsInitial I) (h : ∀ (X : C), Mono (hI.to X)) : InitialMonoClass C

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

theorem CategoryTheory.Limits.InitialMonoClass.of_isTerminal {C : Type u₁} [Category.{v₁, u₁} C] {I T : C} (hI : IsInitial I) (hT : IsTerminal T) : Mono (hI.to T) → InitialMonoClass C

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

def CategoryTheory.Limits.coneOfDiagramInitial {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {X : J} (tX : IsInitial X) (F : Functor J C) : Cone F

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

@[simp]

theorem CategoryTheory.Limits.coneOfDiagramInitial_pt {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {X : J} (tX : IsInitial X) (F : Functor J C) : (coneOfDiagramInitial tX F).pt = F.obj X

@[simp]

theorem CategoryTheory.Limits.coneOfDiagramInitial_π_app {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {X : J} (tX : IsInitial X) (F : Functor J C) (j : J) : (coneOfDiagramInitial tX F).π.app j = F.map (tX.to j)

def CategoryTheory.Limits.limitOfDiagramInitial {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {X : J} (tX : IsInitial X) (F : Functor J C) : IsLimit (coneOfDiagramInitial tX F)

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

def CategoryTheory.Limits.coneOfDiagramTerminal {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {X : J} (hX : IsTerminal X) (F : Functor J C) [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : Cone F

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 limitOfDiagramTerminal we show it is a limit cone.

@[simp]

theorem CategoryTheory.Limits.coneOfDiagramTerminal_π_app {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {X : J} (hX : IsTerminal X) (F : Functor J C) [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] (x✝ : J) : (coneOfDiagramTerminal hX F).π.app x✝ = inv (F.map (hX.from x✝))

@[simp]

theorem CategoryTheory.Limits.coneOfDiagramTerminal_pt {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {X : J} (hX : IsTerminal X) (F : Functor J C) [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : (coneOfDiagramTerminal hX F).pt = F.obj X

def CategoryTheory.Limits.limitOfDiagramTerminal {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {X : J} (hX : IsTerminal X) (F : Functor J C) [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : IsLimit (coneOfDiagramTerminal hX F)

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

def CategoryTheory.Limits.coconeOfDiagramTerminal {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {X : J} (tX : IsTerminal X) (F : Functor J C) : Cocone F

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

@[simp]

theorem CategoryTheory.Limits.coconeOfDiagramTerminal_pt {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {X : J} (tX : IsTerminal X) (F : Functor J C) : (coconeOfDiagramTerminal tX F).pt = F.obj X

@[simp]

theorem CategoryTheory.Limits.coconeOfDiagramTerminal_ι_app {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {X : J} (tX : IsTerminal X) (F : Functor J C) (j : J) : (coconeOfDiagramTerminal tX F).ι.app j = F.map (tX.from j)

def CategoryTheory.Limits.colimitOfDiagramTerminal {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {X : J} (tX : IsTerminal X) (F : Functor J C) : IsColimit (coconeOfDiagramTerminal tX F)

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

theorem CategoryTheory.Limits.IsColimit.isIso_ι_app_of_isTerminal {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {F : Functor J C} {c : Cocone F} (hc : IsColimit c) (X : J) (hX : IsTerminal X) : IsIso (c.ι.app X)

def CategoryTheory.Limits.coconeOfDiagramInitial {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {X : J} (hX : IsInitial X) (F : Functor J C) [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : Cocone F

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 colimitOfDiagramInitial we show it is a colimit cocone.

@[simp]

theorem CategoryTheory.Limits.coconeOfDiagramInitial_ι_app {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {X : J} (hX : IsInitial X) (F : Functor J C) [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] (x✝ : J) : (coconeOfDiagramInitial hX F).ι.app x✝ = inv (F.map (hX.to x✝))

@[simp]

theorem CategoryTheory.Limits.coconeOfDiagramInitial_pt {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {X : J} (hX : IsInitial X) (F : Functor J C) [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : (coconeOfDiagramInitial hX F).pt = F.obj X

def CategoryTheory.Limits.colimitOfDiagramInitial {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {X : J} (hX : IsInitial X) (F : Functor J C) [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : IsColimit (coconeOfDiagramInitial hX F)

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

theorem CategoryTheory.Limits.IsLimit.isIso_π_app_of_isInitial {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {F : Functor J C} {c : Cone F} (hc : IsLimit c) (X : J) (hX : IsInitial X) : IsIso (c.π.app X)

theorem CategoryTheory.Limits.isIso_of_isTerminal {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (hX : IsTerminal X) (hY : IsTerminal Y) (f : X ⟶ Y) : IsIso f

Any morphism between terminal objects is an isomorphism.

theorem CategoryTheory.Limits.isIso_of_isInitial {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (hX : IsInitial X) (hY : IsInitial Y) (f : X ⟶ Y) : IsIso f

Any morphism between initial objects is an isomorphism.