Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

CategoryTheory.Limits.asEmptyCone definition

(X : C) : Cone (Functor.empty.{0} C)

Full source

/-- Construct a cone for the empty diagram given an object. -/
@[simps]
def asEmptyCone (X : C) : Cone (Functor.empty.{0} C) :=
  { pt := X
    π :=
    { app := by aesop_cat } }

Cone over empty diagram with apex $X$

Informal description

Given an object $X$ in a category $C$, the construction `asEmptyCone X` produces a cone over the empty diagram (i.e., the unique functor from the empty category to $C$) with apex $X$. The natural transformation component is defined trivially since the diagram is empty.

CategoryTheory.Limits.asEmptyCocone definition

(X : C) : Cocone (Functor.empty.{0} C)

Full source

/-- Construct a cocone for the empty diagram given an object. -/
@[simps]
def asEmptyCocone (X : C) : Cocone (Functor.empty.{0} C) :=
  { pt := X
    ι :=
    { app := by aesop_cat } }

Cocone for empty diagram

Informal description

Given an object $X$ in a category $C$, this constructs a cocone for the empty diagram with $X$ as the cocone's apex. The cocone's natural transformation is defined trivially since there are no objects in the empty diagram.

CategoryTheory.Limits.IsTerminal abbrev

(X : C)

Full source

/-- `X` is terminal if the cone it induces on the empty diagram is limiting. -/
abbrev IsTerminal (X : C) :=
  IsLimit (asEmptyCone X)

Definition of Terminal Object in a Category

Informal description

An object $X$ in a category $\mathcal{C}$ is called *terminal* if for every object $Y$ in $\mathcal{C}$, there exists a unique morphism from $Y$ to $X$.

CategoryTheory.Limits.IsInitial abbrev

(X : C)

Full source

/-- `X` is initial if the cocone it induces on the empty diagram is colimiting. -/
abbrev IsInitial (X : C) :=
  IsColimit (asEmptyCocone X)

Definition of Initial Object in a Category

Informal description

An object $X$ in a category $\mathcal{C}$ is called *initial* if for every object $Y$ in $\mathcal{C}$, there exists a unique morphism from $X$ to $Y$.

CategoryTheory.Limits.isTerminalEquivUnique definition

 (F : Discrete.{0} PEmpty.{1} ⥤ C) (Y : C) : IsLimit (⟨Y, by aesop_cat, by simp⟩ : Cone F) ≃ ∀ X : C, Unique (X ⟶ Y)

Full source

/-- An object `Y` is terminal iff for every `X` there is a unique morphism `X ⟶ Y`. -/
def isTerminalEquivUnique (F : DiscreteDiscrete.{0} PEmpty.{1} ⥤ C) (Y : C) :
    IsLimitIsLimit (⟨Y, by aesop_cat, by simp⟩ : Cone F) ≃ ∀ X : C, Unique (X ⟶ Y) where
  toFun t X :=
    { default := t.lift ⟨X, ⟨by aesop_cat, by simp⟩⟩
      uniq := fun f =>
        t.uniq ⟨X, ⟨by aesop_cat, by simp⟩⟩ f (by simp) }
  invFun u :=
    { lift := fun s => (u s.pt).default
      uniq := fun s _ _ => (u s.pt).2 _ }
  left_inv := by dsimp [Function.LeftInverse]; intro x; simp only [eq_iff_true_of_subsingleton]
  right_inv := by
    dsimp [Function.RightInverse,Function.LeftInverse]
    intro u; funext X; simp only

Equivalence between limit cone condition and unique morphism condition for terminal objects

Informal description

Given a functor $F$ from the discrete category on the empty type to a category $\mathcal{C}$ and an object $Y$ in $\mathcal{C}$, there is an equivalence between the following two statements: 1. The cone over $F$ with apex $Y$ is a limit cone. 2. For every object $X$ in $\mathcal{C}$, there exists a unique morphism from $X$ to $Y$.

CategoryTheory.Limits.IsTerminal.ofUnique definition

(Y : C) [h : ∀ X : C, Unique (X ⟶ Y)] : IsTerminal Y

Full source

/-- An object `Y` is terminal if for every `X` there is a unique morphism `X ⟶ Y`
    (as an instance). -/
def IsTerminal.ofUnique (Y : C) [h : ∀ X : C, Unique (X ⟶ Y)] : IsTerminal Y where
  lift s := (h s.pt).default
  fac := fun _ ⟨j⟩ => j.elim

Terminal object characterized by unique morphisms

Informal description

Given an object $Y$ in a category $\mathcal{C}$ such that for every object $X$ in $\mathcal{C}$ there exists a unique morphism from $X$ to $Y$, then $Y$ is a terminal object in $\mathcal{C}$.

CategoryTheory.Limits.IsTerminal.ofUniqueHom definition

{Y : C} (h : ∀ X : C, X ⟶ Y) (uniq : ∀ (X : C) (m : X ⟶ Y), m = h X) : IsTerminal Y

Full source

/-- An object `Y` is terminal if for every `X` there is a unique morphism `X ⟶ Y`
    (as explicit arguments). -/
def IsTerminal.ofUniqueHom {Y : C} (h : ∀ X : C, X ⟶ Y) (uniq : ∀ (X : C) (m : X ⟶ Y), m = h X) :
    IsTerminal Y :=
  have : ∀ X : C, Unique (X ⟶ Y) := fun X ↦ ⟨⟨h X⟩, uniq X⟩
  IsTerminal.ofUnique Y

Terminal object characterized by universal morphism

Informal description

Given an object $Y$ in a category $\mathcal{C}$ and a function $h$ that assigns to each object $X$ in $\mathcal{C}$ a morphism $h_X : X \to Y$, if every morphism $m : X \to Y$ satisfies $m = h_X$, then $Y$ is a terminal object in $\mathcal{C}$.

CategoryTheory.Limits.isTerminalTop definition

{α : Type*} [Preorder α] [OrderTop α] : IsTerminal (⊤ : α)

Full source

/-- If `α` is a preorder with top, then `⊤` is a terminal object. -/
def isTerminalTop {α : Type*} [Preorder α] [OrderTop α] : IsTerminal (⊤ : α) :=
  IsTerminal.ofUnique _

Top element as terminal object in a preorder category

Informal description

In a preorder category $\alpha$ with a top element $\top$, the top element $\top$ is a terminal object. That is, for every object $X$ in $\alpha$, there exists a unique morphism from $X$ to $\top$.

CategoryTheory.Limits.IsTerminal.ofIso definition

{Y Z : C} (hY : IsTerminal Y) (i : Y ≅ Z) : IsTerminal Z

Full source

/-- Transport a term of type `IsTerminal` across an isomorphism. -/
def IsTerminal.ofIso {Y Z : C} (hY : IsTerminal Y) (i : Y ≅ Z) : IsTerminal Z :=
  IsLimit.ofIsoLimit hY
    { hom := { hom := i.hom }
      inv := { hom := i.inv } }

Terminal object preserved under isomorphism

Informal description

Given objects $Y$ and $Z$ in a category $\mathcal{C}$, if $Y$ is a terminal object and there exists an isomorphism $i: Y \cong Z$, then $Z$ is also a terminal object.

CategoryTheory.Limits.IsTerminal.equivOfIso definition

{X Y : C} (e : X ≅ Y) : IsTerminal X ≃ IsTerminal Y

Full source

/-- If `X` and `Y` are isomorphic, then `X` is terminal iff `Y` is. -/
def IsTerminal.equivOfIso {X Y : C} (e : X ≅ Y) :
    IsTerminalIsTerminal X ≃ IsTerminal Y where
  toFun h := IsTerminal.ofIso h e
  invFun h := IsTerminal.ofIso h e.symm
  left_inv _ := Subsingleton.elim _ _
  right_inv _ := Subsingleton.elim _ _

Equivalence of terminality under isomorphism

Informal description

Given an isomorphism $e \colon X \cong Y$ between objects $X$ and $Y$ in a category $\mathcal{C}$, there is an equivalence between the properties that $X$ is terminal and that $Y$ is terminal. The equivalence is constructed by mapping a proof that $X$ is terminal to a proof that $Y$ is terminal via the isomorphism $e$, and vice versa via the inverse isomorphism $e^{-1}$.

CategoryTheory.Limits.isInitialEquivUnique definition

 (F : Discrete.{0} PEmpty.{1} ⥤ C) (X : C) :
  IsColimit (⟨X, ⟨by aesop_cat, by simp⟩⟩ : Cocone F) ≃ ∀ Y : C, Unique (X ⟶ Y)

Full source

/-- An object `X` is initial iff for every `Y` there is a unique morphism `X ⟶ Y`. -/
def isInitialEquivUnique (F : DiscreteDiscrete.{0} PEmpty.{1} ⥤ C) (X : C) :
    IsColimitIsColimit (⟨X, ⟨by aesop_cat, by simp⟩⟩ : Cocone F) ≃ ∀ Y : C, Unique (X ⟶ Y) where
  toFun t X :=
    { default := t.desc ⟨X, ⟨by aesop_cat, by simp⟩⟩
      uniq := fun f => t.uniq ⟨X, ⟨by aesop_cat, by simp⟩⟩ f (by simp) }
  invFun u :=
    { desc := fun s => (u s.pt).default
      uniq := fun s _ _ => (u s.pt).2 _ }
  left_inv := by dsimp [Function.LeftInverse]; intro; simp only [eq_iff_true_of_subsingleton]
  right_inv := by
    dsimp [Function.RightInverse,Function.LeftInverse]
    intro; funext; simp only

Equivalence between colimit condition and unique morphism property for initial objects

Informal description

For any functor $F$ from the discrete category on the empty type to a category $C$, and for any object $X$ in $C$, the property that $X$ is a colimit of $F$ is equivalent to the property that for every object $Y$ in $C$, there exists a unique morphism from $X$ to $Y$.

CategoryTheory.Limits.IsInitial.ofUnique definition

(X : C) [h : ∀ Y : C, Unique (X ⟶ Y)] : IsInitial X

Full source

/-- An object `X` is initial if for every `Y` there is a unique morphism `X ⟶ Y`
    (as an instance). -/
def IsInitial.ofUnique (X : C) [h : ∀ Y : C, Unique (X ⟶ Y)] : IsInitial X where
  desc s := (h s.pt).default
  fac := fun _ ⟨j⟩ => j.elim

Initial object characterized by unique morphisms

Informal description

Given an object $X$ in a category $\mathcal{C}$ such that for every object $Y$ in $\mathcal{C}$ there exists a unique morphism from $X$ to $Y$, then $X$ is an initial object in $\mathcal{C}$.

CategoryTheory.Limits.IsInitial.ofUniqueHom definition

{X : C} (h : ∀ Y : C, X ⟶ Y) (uniq : ∀ (Y : C) (m : X ⟶ Y), m = h Y) : IsInitial X

Full source

/-- An object `X` is initial if for every `Y` there is a unique morphism `X ⟶ Y`
    (as explicit arguments). -/
def IsInitial.ofUniqueHom {X : C} (h : ∀ Y : C, X ⟶ Y) (uniq : ∀ (Y : C) (m : X ⟶ Y), m = h Y) :
    IsInitial X :=
  have : ∀ Y : C, Unique (X ⟶ Y) := fun Y ↦ ⟨⟨h Y⟩, uniq Y⟩
  IsInitial.ofUnique X

Initial object characterized by universal morphism property

Informal description

Given an object $X$ in a category $\mathcal{C}$ and a function $h$ that assigns to every object $Y$ in $\mathcal{C}$ a morphism $h(Y) : X \to Y$, if every morphism $m : X \to Y$ satisfies $m = h(Y)$, then $X$ is an initial object in $\mathcal{C}$.

CategoryTheory.Limits.isInitialBot definition

{α : Type*} [Preorder α] [OrderBot α] : IsInitial (⊥ : α)

Full source

/-- If `α` is a preorder with bot, then `⊥` is an initial object. -/
def isInitialBot {α : Type*} [Preorder α] [OrderBot α] : IsInitial (⊥ : α) :=
  IsInitial.ofUnique _

Bottom element as initial object in a preorder category

Informal description

In a preorder category $\alpha$ with a bottom element $\bot$, the bottom element $\bot$ is an initial object.

CategoryTheory.Limits.IsInitial.ofIso definition

{X Y : C} (hX : IsInitial X) (i : X ≅ Y) : IsInitial Y

Full source

/-- Transport a term of type `is_initial` across an isomorphism. -/
def IsInitial.ofIso {X Y : C} (hX : IsInitial X) (i : X ≅ Y) : IsInitial Y :=
  IsColimit.ofIsoColimit hX
    { hom := { hom := i.hom }
      inv := { hom := i.inv } }

Transport of initiality along an isomorphism

Informal description

Given an initial object $X$ in a category $\mathcal{C}$ and an isomorphism $i : X \cong Y$ between $X$ and another object $Y$, the object $Y$ is also initial. This transports the initiality property across the isomorphism.

CategoryTheory.Limits.IsInitial.equivOfIso definition

{X Y : C} (e : X ≅ Y) : IsInitial X ≃ IsInitial Y

Full source

/-- If `X` and `Y` are isomorphic, then `X` is initial iff `Y` is. -/
def IsInitial.equivOfIso {X Y : C} (e : X ≅ Y) :
    IsInitialIsInitial X ≃ IsInitial Y where
  toFun h := IsInitial.ofIso h e
  invFun h := IsInitial.ofIso h e.symm
  left_inv _ := Subsingleton.elim _ _
  right_inv _ := Subsingleton.elim _ _

Equivalence of initiality under isomorphism

Informal description

Given an isomorphism $e \colon X \cong Y$ between objects $X$ and $Y$ in a category $\mathcal{C}$, there is an equivalence between the propositions "$X$ is initial" and "$Y$ is initial". The equivalence is constructed by transporting the initiality property along the isomorphism $e$ and its inverse $e^{-1}$.

CategoryTheory.Limits.IsTerminal.from definition

{X : C} (t : IsTerminal X) (Y : C) : Y ⟶ X

Full source

/-- Give the morphism to a terminal object from any other. -/
def IsTerminal.from {X : C} (t : IsTerminal X) (Y : C) : Y ⟶ X :=
  t.lift (asEmptyCone Y)

Unique morphism to a terminal object

Informal description

Given a terminal object $X$ in a category $\mathcal{C}$ and any object $Y$ in $\mathcal{C}$, the morphism $\text{from}_t(Y) : Y \to X$ is the unique morphism from $Y$ to $X$ guaranteed by the terminality of $X$.

CategoryTheory.Limits.IsTerminal.hom_ext theorem

{X Y : C} (t : IsTerminal X) (f g : Y ⟶ X) : f = g

Full source

/-- Any two morphisms to a terminal object are equal. -/
theorem IsTerminal.hom_ext {X Y : C} (t : IsTerminal X) (f g : Y ⟶ X) : f = g :=
  IsLimit.hom_ext t (by simp)

Uniqueness of Morphisms to a Terminal Object

Informal description

For any terminal object $X$ in a category $\mathcal{C}$ and any two morphisms $f, g : Y \to X$ from an object $Y$ to $X$, we have $f = g$.

CategoryTheory.Limits.IsTerminal.comp_from theorem

{Z : C} (t : IsTerminal Z) {X Y : C} (f : X ⟶ Y) : f ≫ t.from Y = t.from X

Full source

@[simp]
theorem IsTerminal.comp_from {Z : C} (t : IsTerminal Z) {X Y : C} (f : X ⟶ Y) :
    f ≫ t.from Y = t.from X :=
  t.hom_ext _ _

Composition with Unique Morphism to Terminal Object Preserves Uniqueness

Informal description

Let $Z$ be a terminal object in a category $\mathcal{C}$ (as witnessed by $t : \text{IsTerminal } Z$). For any objects $X, Y$ in $\mathcal{C}$ and any morphism $f : X \to Y$, the composition of $f$ with the unique morphism $\text{from}_t(Y) : Y \to Z$ equals the unique morphism $\text{from}_t(X) : X \to Z$. In other words, $f \circ \text{from}_t(Y) = \text{from}_t(X)$.

CategoryTheory.Limits.IsTerminal.from_self theorem

{X : C} (t : IsTerminal X) : t.from X = 𝟙 X

Full source

@[simp]
theorem IsTerminal.from_self {X : C} (t : IsTerminal X) : t.from X = 𝟙 X :=
  t.hom_ext _ _

Identity Morphism as Unique Endomorphism of Terminal Object

Informal description

For any terminal object $X$ in a category $\mathcal{C}$, the unique morphism from $X$ to itself is the identity morphism $\text{id}_X$.

CategoryTheory.Limits.IsInitial.to definition

{X : C} (t : IsInitial X) (Y : C) : X ⟶ Y

Full source

/-- Give the morphism from an initial object to any other. -/
def IsInitial.to {X : C} (t : IsInitial X) (Y : C) : X ⟶ Y :=
  t.desc (asEmptyCocone Y)

Unique morphism from initial object

Informal description

Given an initial object $X$ in a category $\mathcal{C}$ (as witnessed by $t : \text{IsInitial } X$) and any other object $Y$ in $\mathcal{C}$, this defines the unique morphism from $X$ to $Y$.

CategoryTheory.Limits.IsInitial.hom_ext theorem

{X Y : C} (t : IsInitial X) (f g : X ⟶ Y) : f = g

Full source

/-- Any two morphisms from an initial object are equal. -/
theorem IsInitial.hom_ext {X Y : C} (t : IsInitial X) (f g : X ⟶ Y) : f = g :=
  IsColimit.hom_ext t (by simp)

Uniqueness of Morphisms from Initial Object

Informal description

For any initial object $X$ in a category $\mathcal{C}$ and any object $Y$ in $\mathcal{C}$, any two morphisms $f, g: X \to Y$ are equal.

CategoryTheory.Limits.IsInitial.to_comp theorem

{X : C} (t : IsInitial X) {Y Z : C} (f : Y ⟶ Z) : t.to Y ≫ f = t.to Z

Full source

@[simp]
theorem IsInitial.to_comp {X : C} (t : IsInitial X) {Y Z : C} (f : Y ⟶ Z) : t.to Y ≫ f = t.to Z :=
  t.hom_ext _ _

Composition with Unique Morphism from Initial Object

Informal description

Let $X$ be an initial object in a category $\mathcal{C}$ (as witnessed by $t : \text{IsInitial } X$), and let $Y, Z$ be objects in $\mathcal{C}$. For any morphism $f : Y \to Z$, the composition of the unique morphism $t.to Y : X \to Y$ with $f$ equals the unique morphism $t.to Z : X \to Z$. In other words, the following diagram commutes: \[ \begin{tikzcd} X \arrow[r, "t.to Y"] \arrow[dr, "t.to Z"'] & Y \arrow[d, "f"] \\ & Z \end{tikzcd} \]

CategoryTheory.Limits.IsInitial.to_self theorem

{X : C} (t : IsInitial X) : t.to X = 𝟙 X

Full source

@[simp]
theorem IsInitial.to_self {X : C} (t : IsInitial X) : t.to X = 𝟙 X :=
  t.hom_ext _ _

Identity Morphism as Unique Endomorphism of Initial Object

Informal description

For any initial object $X$ in a category $\mathcal{C}$ (as witnessed by $t : \text{IsInitial } X$), the unique morphism from $X$ to itself is the identity morphism on $X$, i.e., $t.to X = \text{id}_X$.

CategoryTheory.Limits.IsTerminal.isSplitMono_from theorem

{X Y : C} (t : IsTerminal X) (f : X ⟶ Y) : IsSplitMono f

Full source

/-- Any morphism from a terminal object is split mono. -/
theorem IsTerminal.isSplitMono_from {X Y : C} (t : IsTerminal X) (f : X ⟶ Y) : IsSplitMono f :=
  IsSplitMono.mk' ⟨t.from _, t.hom_ext _ _⟩

Morphisms from Terminal Objects are Split Monomorphisms

Informal description

Let $X$ be a terminal object in a category $\mathcal{C}$ (as witnessed by $t : \text{IsTerminal } X$), and let $Y$ be any object in $\mathcal{C}$. For any morphism $f : X \to Y$, $f$ is a split monomorphism (i.e., there exists a morphism $g : Y \to X$ such that $g \circ f = \text{id}_X$).

CategoryTheory.Limits.IsInitial.isSplitEpi_to theorem

{X Y : C} (t : IsInitial X) (f : Y ⟶ X) : IsSplitEpi f

Full source

/-- Any morphism to an initial object is split epi. -/
theorem IsInitial.isSplitEpi_to {X Y : C} (t : IsInitial X) (f : Y ⟶ X) : IsSplitEpi f :=
  IsSplitEpi.mk' ⟨t.to _, t.hom_ext _ _⟩

Morphisms to Initial Objects are Split Epimorphisms

Informal description

Let $X$ be an initial object in a category $\mathcal{C}$ (as witnessed by $t : \text{IsInitial } X$). Then for any object $Y$ in $\mathcal{C}$ and any morphism $f : Y \to X$, $f$ is a split epimorphism (i.e., there exists a morphism $g : X \to Y$ such that $f \circ g = \text{id}_X$).

CategoryTheory.Limits.IsTerminal.mono_from theorem

{X Y : C} (t : IsTerminal X) (f : X ⟶ Y) : Mono f

Full source

/-- Any morphism from a terminal object is mono. -/
theorem IsTerminal.mono_from {X Y : C} (t : IsTerminal X) (f : X ⟶ Y) : Mono f := by
  haveI := t.isSplitMono_from f; infer_instance

Morphisms from Terminal Objects are Monomorphisms

Informal description

Let $X$ be a terminal object in a category $\mathcal{C}$ (as witnessed by $t : \text{IsTerminal } X$), and let $Y$ be any object in $\mathcal{C}$. Then any morphism $f : X \to Y$ is a monomorphism.

CategoryTheory.Limits.IsInitial.epi_to theorem

{X Y : C} (t : IsInitial X) (f : Y ⟶ X) : Epi f

Full source

/-- Any morphism to an initial object is epi. -/
theorem IsInitial.epi_to {X Y : C} (t : IsInitial X) (f : Y ⟶ X) : Epi f := by
  haveI := t.isSplitEpi_to f; infer_instance

Morphisms to Initial Objects are Epimorphisms

Informal description

Let $X$ be an initial object in a category $\mathcal{C}$ (as witnessed by $t : \text{IsInitial } X$). Then for any object $Y$ in $\mathcal{C}$ and any morphism $f : Y \to X$, $f$ is an epimorphism.

CategoryTheory.Limits.IsTerminal.uniqueUpToIso definition

{T T' : C} (hT : IsTerminal T) (hT' : IsTerminal T') : T ≅ T'

Full source

/-- If `T` and `T'` are terminal, they are isomorphic. -/
@[simps]
def IsTerminal.uniqueUpToIso {T T' : C} (hT : IsTerminal T) (hT' : IsTerminal T') : T ≅ T' where
  hom := hT'.from _
  inv := hT.from _

Isomorphism between terminal objects

Informal description

For any two terminal objects $T$ and $T'$ in a category $\mathcal{C}$, there exists a unique isomorphism between them, where the morphisms are given by the unique morphisms from each terminal object to the other.

CategoryTheory.Limits.IsInitial.uniqueUpToIso definition

{I I' : C} (hI : IsInitial I) (hI' : IsInitial I') : I ≅ I'

Full source

/-- If `I` and `I'` are initial, they are isomorphic. -/
@[simps]
def IsInitial.uniqueUpToIso {I I' : C} (hI : IsInitial I) (hI' : IsInitial I') : I ≅ I' where
  hom := hI.to _
  inv := hI'.to _

Isomorphism between initial objects

Informal description

For any two initial objects $I$ and $I'$ in a category $\mathcal{C}$, there exists a unique isomorphism between them, where the morphisms are given by the unique morphisms from each initial object to the other.

CategoryTheory.Limits.isLimitChangeEmptyCone definition

{c₁ : Cone F₁} (hl : IsLimit c₁) (c₂ : Cone F₂) (hi : c₁.pt ≅ c₂.pt) : IsLimit c₂

Full source

/-- Being terminal is independent of the empty diagram, its universe, and the cone over it,
    as long as the cone points are isomorphic. -/
def isLimitChangeEmptyCone {c₁ : Cone F₁} (hl : IsLimit c₁) (c₂ : Cone F₂) (hi : c₁.pt ≅ c₂.pt) :
    IsLimit c₂ where
  lift c := hl.lift ⟨c.pt, by aesop_cat, by simp⟩ ≫ hi.hom
  uniq c f _ := by
    dsimp
    rw [← hl.uniq _ (f ≫ hi.inv) _]
    · simp only [Category.assoc, Iso.inv_hom_id, Category.comp_id]
    · simp

Limit preservation under apex isomorphism

Informal description

Given a cone `c₁` over a diagram `F₁` that is a limit, and another cone `c₂` over a diagram `F₂` with an isomorphism `hi : c₁.pt ≅ c₂.pt` between their apexes, then `c₂` is also a limit. The limit structure on `c₂` is constructed by precomposing the limit structure of `c₁` with the isomorphism `hi.hom`.

CategoryTheory.Limits.isLimitEmptyConeEquiv definition

(c₁ : Cone F₁) (c₂ : Cone F₂) (h : c₁.pt ≅ c₂.pt) : IsLimit c₁ ≃ IsLimit c₂

Full source

/-- Replacing an empty cone in `IsLimit` by another with the same cone point
    is an equivalence. -/
def isLimitEmptyConeEquiv (c₁ : Cone F₁) (c₂ : Cone F₂) (h : c₁.pt ≅ c₂.pt) :
    IsLimitIsLimit c₁ ≃ IsLimit c₂ where
  toFun hl := isLimitChangeEmptyCone C hl c₂ h
  invFun hl := isLimitChangeEmptyCone C hl c₁ h.symm
  left_inv := by dsimp [Function.LeftInverse]; intro; simp only [eq_iff_true_of_subsingleton]
  right_inv := by
    dsimp [Function.LeftInverse,Function.RightInverse]; intro
    simp only [eq_iff_true_of_subsingleton]

Equivalence of limit conditions for isomorphic empty cones

Informal description

Given two empty cones $c_1$ and $c_2$ in a category $\mathcal{C}$ with an isomorphism $h \colon c_1.pt \cong c_2.pt$ between their apexes, there is an equivalence between the types asserting that $c_1$ is a limit and that $c_2$ is a limit. This equivalence is constructed by transporting the limit structure along the isomorphism $h$ and its inverse $h^{-1}$.

CategoryTheory.Limits.isColimitChangeEmptyCocone definition

{c₁ : Cocone F₁} (hl : IsColimit c₁) (c₂ : Cocone F₂) (hi : c₁.pt ≅ c₂.pt) : IsColimit c₂

Full source

/-- Being initial is independent of the empty diagram, its universe, and the cocone over it,
    as long as the cocone points are isomorphic. -/
def isColimitChangeEmptyCocone {c₁ : Cocone F₁} (hl : IsColimit c₁) (c₂ : Cocone F₂)
    (hi : c₁.pt ≅ c₂.pt) : IsColimit c₂ where
  desc c := hi.inv ≫ hl.desc ⟨c.pt, by aesop_cat, by simp⟩
  uniq c f _ := by
    dsimp
    rw [← hl.uniq _ (hi.hom ≫ f) _]
    · simp only [Iso.inv_hom_id_assoc]
    · simp

Colimit preservation under apex isomorphism

Informal description

Given a cocone `c₁` over a diagram `F₁` that is a colimit, and another cocone `c₂` over a diagram `F₂` with an isomorphism between their apexes `c₁.pt ≅ c₂.pt`, then `c₂` is also a colimit. The colimit structure on `c₂` is constructed by precomposing the colimit structure of `c₁` with the isomorphism.

CategoryTheory.Limits.isColimitEmptyCoconeEquiv definition

(c₁ : Cocone F₁) (c₂ : Cocone F₂) (h : c₁.pt ≅ c₂.pt) : IsColimit c₁ ≃ IsColimit c₂

Full source

/-- Replacing an empty cocone in `IsColimit` by another with the same cocone point
    is an equivalence. -/
def isColimitEmptyCoconeEquiv (c₁ : Cocone F₁) (c₂ : Cocone F₂) (h : c₁.pt ≅ c₂.pt) :
    IsColimitIsColimit c₁ ≃ IsColimit c₂ where
  toFun hl := isColimitChangeEmptyCocone C hl c₂ h
  invFun hl := isColimitChangeEmptyCocone C hl c₁ h.symm
  left_inv := by dsimp [Function.LeftInverse]; intro; simp only [eq_iff_true_of_subsingleton]
  right_inv := by
    dsimp [Function.LeftInverse,Function.RightInverse]; intro
    simp only [eq_iff_true_of_subsingleton]

Equivalence of colimit conditions for isomorphic empty cocones

Informal description

Given two empty cocones $c_1$ and $c_2$ in a category $\mathcal{C}$ with an isomorphism $h \colon c_1.pt \cong c_2.pt$ between their apexes, there is an equivalence between the types asserting that $c_1$ is a colimit and that $c_2$ is a colimit. This equivalence is constructed by transporting the colimit structure along the isomorphism $h$ and its inverse $h^{-1}$.

CategoryTheory.Limits.terminalOpOfInitial definition

{X : C} (t : IsInitial X) : IsTerminal (Opposite.op X)

Full source

/-- An initial object is terminal in the opposite category. -/
def terminalOpOfInitial {X : C} (t : IsInitial X) : IsTerminal (Opposite.op X) where
  lift s := (t.to s.pt.unop).op
  uniq _ _ _ := Quiver.Hom.unop_inj (t.hom_ext _ _)

Terminal object in opposite category from initial object

Informal description

Given an initial object $X$ in a category $\mathcal{C}$ (as witnessed by $t : \text{IsInitial } X$), its opposite $X^{\mathrm{op}}$ in the opposite category $\mathcal{C}^{\mathrm{op}}$ is terminal. The unique morphism to $X^{\mathrm{op}}$ from any object $Y$ in $\mathcal{C}^{\mathrm{op}}$ is obtained by taking the opposite of the unique morphism from $X$ to $Y^{\mathrm{unop}}$ in $\mathcal{C}$.

CategoryTheory.Limits.terminalUnopOfInitial definition

{X : Cᵒᵖ} (t : IsInitial X) : IsTerminal X.unop

Full source

/-- An initial object in the opposite category is terminal in the original category. -/
def terminalUnopOfInitial {X : Cᵒᵖ} (t : IsInitial X) : IsTerminal X.unop where
  lift s := (t.to (Opposite.op s.pt)).unop
  uniq _ _ _ := Quiver.Hom.op_inj (t.hom_ext _ _)

Terminal object in $\mathcal{C}$ from initial object in $\mathcal{C}^{\mathrm{op}}$

Informal description

Given an object $X$ in the opposite category $\mathcal{C}^{\mathrm{op}}$ that is initial (as witnessed by $t : \text{IsInitial } X$), its corresponding object $X^{\mathrm{unop}}$ in the original category $\mathcal{C}$ is terminal. The unique morphism to $X^{\mathrm{unop}}$ from any object $Y$ in $\mathcal{C}$ is obtained by unopposite of the unique morphism from $X$ to $Y^{\mathrm{op}}$ in $\mathcal{C}^{\mathrm{op}}$.

CategoryTheory.Limits.initialOpOfTerminal definition

{X : C} (t : IsTerminal X) : IsInitial (Opposite.op X)

Full source

/-- A terminal object is initial in the opposite category. -/
def initialOpOfTerminal {X : C} (t : IsTerminal X) : IsInitial (Opposite.op X) where
  desc s := (t.from s.pt.unop).op
  uniq _ _ _ := Quiver.Hom.unop_inj (t.hom_ext _ _)

Initial object in opposite category from terminal object

Informal description

Given a terminal object $X$ in a category $\mathcal{C}$ (as witnessed by $t : \text{IsTerminal } X$), its opposite $X^{\mathrm{op}}$ in the opposite category $\mathcal{C}^{\mathrm{op}}$ is initial. The unique morphism from $X^{\mathrm{op}}$ to any object $Y$ in $\mathcal{C}^{\mathrm{op}}$ is obtained by taking the opposite of the unique morphism from $Y^{\mathrm{unop}}$ to $X$ in $\mathcal{C}$.

CategoryTheory.Limits.initialUnopOfTerminal definition

{X : Cᵒᵖ} (t : IsTerminal X) : IsInitial X.unop

Full source

/-- A terminal object in the opposite category is initial in the original category. -/
def initialUnopOfTerminal {X : Cᵒᵖ} (t : IsTerminal X) : IsInitial X.unop where
  desc s := (t.from (Opposite.op s.pt)).unop
  uniq _ _ _ := Quiver.Hom.op_inj (t.hom_ext _ _)

Initial object in $\mathcal{C}$ from terminal object in $\mathcal{C}^{\mathrm{op}}$

Informal description

Given a terminal object $X$ in the opposite category $\mathcal{C}^{\mathrm{op}}$, its corresponding object $X^{\mathrm{unop}}$ in the original category $\mathcal{C}$ is initial. The unique morphism from $X^{\mathrm{unop}}$ to any object $Y$ in $\mathcal{C}$ is obtained by unopposite of the unique morphism from $Y^{\mathrm{op}}$ to $X$ in $\mathcal{C}^{\mathrm{op}}$.

CategoryTheory.Limits.InitialMonoClass structure

(C : Type u₁) [Category.{v₁} C]

Full source

/-- 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.
-/
class InitialMonoClass (C : Type u₁) [Category.{v₁} C] : Prop where
  /-- The map from the (any as stated) initial object to any other object is a
    monomorphism -/
  isInitial_mono_from : ∀ {I} (X : C) (hI : IsInitial I), Mono (hI.to X)

Category with Monomorphic Initial Morphisms

Informal description

A category $ C $ is said to be an `InitialMonoClass` if for any initial object $ I $ in $ C $, the canonical morphism from $ I $ to any other object $ X $ is a monomorphism. This property is particularly useful when working with arbitrary morphisms out of an initial object. In categories with a terminal object, this condition is equivalent to requiring that the unique morphism from the initial object to the terminal object is a monomorphism, which corresponds to the second of Freyd's axioms for an AT category.

CategoryTheory.Limits.IsInitial.mono_from theorem

[InitialMonoClass C] {I} {X : C} (hI : IsInitial I) (f : I ⟶ X) : Mono f

Full source

theorem IsInitial.mono_from [InitialMonoClass C] {I} {X : C} (hI : IsInitial I) (f : I ⟶ X) :
    Mono f := by
  rw [hI.hom_ext f (hI.to X)]
  apply InitialMonoClass.isInitial_mono_from

Monomorphisms from Initial Objects in `InitialMonoClass` Categories

Informal description

In a category $\mathcal{C}$ that satisfies the `InitialMonoClass` property, for any initial object $I$ and any object $X$ in $\mathcal{C}$, every morphism $f: I \to X$ is a monomorphism.

CategoryTheory.Limits.InitialMonoClass.of_isInitial theorem

{I : C} (hI : IsInitial I) (h : ∀ X, Mono (hI.to X)) : InitialMonoClass C

Full source

/-- 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 InitialMonoClass.of_isInitial {I : C} (hI : IsInitial I) (h : ∀ X, Mono (hI.to X)) :
    InitialMonoClass C where
  isInitial_mono_from {I'} X hI' := by
    rw [hI'.hom_ext (hI'.to X) ((hI'.uniqueUpToIso hI).hom ≫ hI.to X)]
    apply mono_comp

InitialMonoClass Criterion via Monomorphic Initial Morphisms

Informal description

Let $\mathcal{C}$ be a category and $I$ an initial object in $\mathcal{C}$. If for every object $X$ in $\mathcal{C}$, the unique morphism $I \to X$ is a monomorphism, then $\mathcal{C}$ is an `InitialMonoClass`.

CategoryTheory.Limits.InitialMonoClass.of_isTerminal theorem

{I T : C} (hI : IsInitial I) (hT : IsTerminal T) (_ : Mono (hI.to T)) : InitialMonoClass C

Full source

/-- 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. -/
theorem InitialMonoClass.of_isTerminal {I T : C} (hI : IsInitial I) (hT : IsTerminal T)
    (_ : Mono (hI.to T)) : InitialMonoClass C :=
  InitialMonoClass.of_isInitial hI fun X => mono_of_mono_fac (hI.hom_ext (_ ≫ hT.from X) (hI.to T))

InitialMonoClass Criterion via Terminal Object Morphism

Informal description

Let $\mathcal{C}$ be a category with an initial object $I$ and a terminal object $T$. If the unique morphism $I \to T$ is a monomorphism, then $\mathcal{C}$ is an `InitialMonoClass` (i.e., all morphisms from initial objects are monomorphisms).

CategoryTheory.Limits.coneOfDiagramInitial definition

{X : J} (tX : IsInitial X) (F : J ⥤ C) : Cone F

Full source

/-- 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. -/
@[simps]
def coneOfDiagramInitial {X : J} (tX : IsInitial X) (F : J ⥤ C) : Cone F where
  pt := F.obj X
  π :=
    { app := fun j => F.map (tX.to j)
      naturality := fun j j' k => by
        dsimp
        rw [← F.map_comp, Category.id_comp, tX.hom_ext (tX.to j ≫ k) (tX.to j')] }

Cone construction from initial object and functor

Informal description

Given an initial object $X$ in a small category $J$ (as witnessed by $t_X : \text{IsInitial } X$) and a functor $F : J \to C$, the construction $\text{coneOfDiagramInitial } t_X F$ produces a cone over $F$ with apex $F(X)$. The projection maps of this cone are given by $F$ applied to the unique morphisms from $X$ to each object in $J$.

CategoryTheory.Limits.limitOfDiagramInitial definition

{X : J} (tX : IsInitial X) (F : J ⥤ C) : IsLimit (coneOfDiagramInitial tX F)

Full source

/-- From a functor `F : J ⥤ C`, given an initial object of `J`, show the cone
`coneOfDiagramInitial` is a limit. -/
def limitOfDiagramInitial {X : J} (tX : IsInitial X) (F : J ⥤ C) :
    IsLimit (coneOfDiagramInitial tX F) where
  lift s := s.π.app X
  uniq s m w := by
    conv_lhs => dsimp
    simp_rw [← w X, coneOfDiagramInitial_π_app, tX.hom_ext (tX.to X) (𝟙 _)]
    simp

Limit cone property for functors from categories with initial objects

Informal description

Given an initial object $X$ in a small category $J$ (as witnessed by $t_X : \text{IsInitial } X$) and a functor $F : J \to C$, the cone $\text{coneOfDiagramInitial } t_X F$ is a limit cone. The unique morphism from any other cone $s$ to this limit cone is given by the projection $\pi_X$ of $s$ at $X$.

CategoryTheory.Limits.coneOfDiagramTerminal definition

{X : J} (hX : IsTerminal X) (F : J ⥤ C) [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : Cone F

Full source

/-- 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. -/
@[simps]
def coneOfDiagramTerminal {X : J} (hX : IsTerminal X) (F : J ⥤ C)
    [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : Cone F where
  pt := F.obj X
  π :=
    { app := fun _ => inv (F.map (hX.from _))
      naturality := by
        intro i j f
        dsimp
        simp only [IsIso.eq_inv_comp, IsIso.comp_inv_eq, Category.id_comp, ← F.map_comp,
          hX.hom_ext (hX.from i) (f ≫ hX.from j)] }

Cone construction from a terminal object and isomorphism-preserving functor

Informal description

Given a terminal object $X$ in a small category $J$ and a functor $F : J \to C$ such that for every morphism $f : i \to j$ in $J$, the morphism $F(f)$ is an isomorphism, the construction `coneOfDiagramTerminal hX F` produces a cone over $F$ with apex $F(X)$. The projection maps of this cone are given by the inverses of the morphisms $F(\text{from}_X(i)) : F(i) \to F(X)$, where $\text{from}_X(i)$ is the unique morphism from $i$ to $X$.

CategoryTheory.Limits.limitOfDiagramTerminal definition

 {X : J} (hX : IsTerminal X) (F : J ⥤ C) [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] :
  IsLimit (coneOfDiagramTerminal hX F)

Full source

/-- 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 limitOfDiagramTerminal {X : J} (hX : IsTerminal X) (F : J ⥤ C)
    [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : IsLimit (coneOfDiagramTerminal hX F) where
  lift S := S.π.app _

Limit cone from a terminal object and isomorphism-preserving functor

Informal description

Given a terminal object $X$ in a small category $J$ and a functor $F : J \to C$ such that for every morphism $f : i \to j$ in $J$, the morphism $F(f)$ is an isomorphism, the cone `coneOfDiagramTerminal hX F` is a limit cone. The lifting morphism for any other cone $S$ over $F$ is given by the projection map $S.\pi.\text{app}(X)$.

CategoryTheory.Limits.coconeOfDiagramTerminal definition

{X : J} (tX : IsTerminal X) (F : J ⥤ C) : Cocone F

Full source

/-- 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. -/
@[simps]
def coconeOfDiagramTerminal {X : J} (tX : IsTerminal X) (F : J ⥤ C) : Cocone F where
  pt := F.obj X
  ι :=
    { app := fun j => F.map (tX.from j)
      naturality := fun j j' k => by
        dsimp
        rw [← F.map_comp, Category.comp_id, tX.hom_ext (k ≫ tX.from j') (tX.from j)] }

Cocone construction from a terminal object

Informal description

Given a terminal object $X$ in a small category $J$ and a functor $F : J \to C$, the construction `coconeOfDiagramTerminal tX F` produces a cocone under $F$ with apex $F(X)$. The injection maps of this cocone are given by $F(f_j)$ for each unique morphism $f_j : j \to X$ from any object $j$ in $J$ to the terminal object $X$.

CategoryTheory.Limits.colimitOfDiagramTerminal definition

{X : J} (tX : IsTerminal X) (F : J ⥤ C) : IsColimit (coconeOfDiagramTerminal tX F)

Full source

/-- From a functor `F : J ⥤ C`, given a terminal object of `J`, show the cocone
`coconeOfDiagramTerminal` is a colimit. -/
def colimitOfDiagramTerminal {X : J} (tX : IsTerminal X) (F : J ⥤ C) :
    IsColimit (coconeOfDiagramTerminal tX F) where
  desc s := s.ι.app X
  uniq s m w := by
    conv_rhs => dsimp -- Porting note: why do I need this much firepower?
    rw [← w X, coconeOfDiagramTerminal_ι_app, tX.hom_ext (tX.from X) (𝟙 _)]
    simp

Colimit cocone from a terminal object

Informal description

Given a terminal object $X$ in a small category $J$ and a functor $F : J \to C$, the cocone `coconeOfDiagramTerminal tX F` is a colimit cocone for $F$. The colimit is given by the unique morphism from any other cocone to the apex $F(X)$ of this cocone, and the uniqueness follows from the terminality of $X$.

CategoryTheory.Limits.IsColimit.isIso_ι_app_of_isTerminal theorem

{F : J ⥤ C} {c : Cocone F} (hc : IsColimit c) (X : J) (hX : IsTerminal X) : IsIso (c.ι.app X)

Full source

lemma IsColimit.isIso_ι_app_of_isTerminal {F : J ⥤ C} {c : Cocone F} (hc : IsColimit c)
    (X : J) (hX : IsTerminal X) :
    IsIso (c.ι.app X) := by
  change IsIso (coconePointUniqueUpToIso (colimitOfDiagramTerminal hX F) hc).hom
  infer_instance

Colimit Cocone Component at Terminal Object is Isomorphism

Informal description

Let $\mathcal{C}$ be a category, $J$ a small category, and $F : J \to \mathcal{C}$ a functor. Given a colimit cocone $c$ for $F$ (witnessed by $hc : \text{IsColimit } c$) and a terminal object $X$ in $J$ (witnessed by $hX : \text{IsTerminal } X$), the component $c.\iota.\text{app } X$ of the cocone's natural transformation at $X$ is an isomorphism.

CategoryTheory.Limits.coconeOfDiagramInitial definition

{X : J} (hX : IsInitial X) (F : J ⥤ C) [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : Cocone F

Full source

/-- 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. -/
@[simps]
def coconeOfDiagramInitial {X : J} (hX : IsInitial X) (F : J ⥤ C)
    [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : Cocone F where
  pt := F.obj X
  ι :=
    { app := fun _ => inv (F.map (hX.to _))
      naturality := by
        intro i j f
        dsimp
        simp only [IsIso.eq_inv_comp, IsIso.comp_inv_eq, Category.comp_id, ← F.map_comp,
          hX.hom_ext (hX.to i ≫ f) (hX.to j)] }

Cocone from a functor with initial object and isomorphisms

Informal description

Given a functor $ F : J \to C $ and an initial object $ X $ in the category $ J $ (as witnessed by $ hX : \text{IsInitial } X $), and assuming that for any objects $ i, j $ in $ J $ and any morphism $ f : i \to j $, the morphism $ F(f) $ is an isomorphism, this constructs a cocone for $ F $ with apex $ F(X) $. The cocone's morphisms are given by the inverses of the morphisms $ F(hX.to \, i) $, where $ hX.to \, i $ is the unique morphism from $ X $ to $ i $.

CategoryTheory.Limits.colimitOfDiagramInitial definition

 {X : J} (hX : IsInitial X) (F : J ⥤ C) [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] :
  IsColimit (coconeOfDiagramInitial hX F)

Full source

/-- 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. -/
def colimitOfDiagramInitial {X : J} (hX : IsInitial X) (F : J ⥤ C)
    [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : IsColimit (coconeOfDiagramInitial hX F) where
  desc S := S.ι.app _

Colimit cocone from a functor with initial object and isomorphisms

Informal description

Given a functor $ F : J \to C $ and an initial object $ X $ in the category $ J $ (as witnessed by $ hX : \text{IsInitial } X $), and assuming that for any objects $ i, j $ in $ J $ and any morphism $ f : i \to j $, the morphism $ F(f) $ is an isomorphism, then the cocone constructed by `coconeOfDiagramInitial` is a colimit cocone for $ F $. The colimit cocone's universal property is given by the unique morphism from the apex of any other cocone to $ F(X) $.

CategoryTheory.Limits.IsLimit.isIso_π_app_of_isInitial theorem

{F : J ⥤ C} {c : Cone F} (hc : IsLimit c) (X : J) (hX : IsInitial X) : IsIso (c.π.app X)

Full source

lemma IsLimit.isIso_π_app_of_isInitial {F : J ⥤ C} {c : Cone F} (hc : IsLimit c)
    (X : J) (hX : IsInitial X) :
    IsIso (c.π.app X) := by
  change IsIso (conePointUniqueUpToIso hc (limitOfDiagramInitial hX F)).hom
  infer_instance

Limit Cone Projection at Initial Object is Isomorphism

Informal description

Let $F : J \to C$ be a functor, $c$ a cone over $F$, and $X$ an initial object in $J$. If $c$ is a limit cone, then the projection morphism $c.\pi_X : c.\text{pt} \to F(X)$ is an isomorphism.

CategoryTheory.Limits.isIso_of_isTerminal theorem

{X Y : C} (hX : IsTerminal X) (hY : IsTerminal Y) (f : X ⟶ Y) : IsIso f

Full source

/-- Any morphism between terminal objects is an isomorphism. -/
lemma isIso_of_isTerminal {X Y : C} (hX : IsTerminal X) (hY : IsTerminal Y) (f : X ⟶ Y) :
    IsIso f := by
  refine ⟨⟨IsTerminal.from hX Y, ?_⟩⟩
  simp only [IsTerminal.comp_from, IsTerminal.from_self, true_and]
  apply IsTerminal.hom_ext hY

Morphisms between terminal objects are isomorphisms

Informal description

Let $X$ and $Y$ be terminal objects in a category $\mathcal{C}$. Then any morphism $f : X \to Y$ is an isomorphism.

CategoryTheory.Limits.isIso_of_isInitial theorem

{X Y : C} (hX : IsInitial X) (hY : IsInitial Y) (f : X ⟶ Y) : IsIso f

Full source

/-- Any morphism between initial objects is an isomorphism. -/
lemma isIso_of_isInitial {X Y : C} (hX : IsInitial X) (hY : IsInitial Y) (f : X ⟶ Y) :
    IsIso f := by
  refine ⟨⟨IsInitial.to hY X, ?_⟩⟩
  simp only [IsInitial.to_comp, IsInitial.to_self, and_true]
  apply IsInitial.hom_ext hX

Morphisms Between Initial Objects are Isomorphisms

Informal description

For any two initial objects $X$ and $Y$ in a category $\mathcal{C}$, any morphism $f : X \to Y$ is an isomorphism.

References