doc-next-gen

Mathlib.CategoryTheory.Limits.Shapes.Terminal

CategoryTheory.Limits.HasTerminal abbrev
Full source 
/-- A category has a terminal object if it has a limit over the empty diagram.
Use `hasTerminal_of_unique` to construct instances.
-/
abbrev HasTerminal :=
  HasLimitsOfShape (Discrete.{0} PEmpty) C
Existence of Terminal Object in a Category
Informal description
A category $\mathcal{C}$ has a terminal object if there exists an object $1 \in \mathcal{C}$ such that for every object $X \in \mathcal{C}$, there is a unique morphism $X \to 1$.
CategoryTheory.Limits.HasInitial abbrev
Full source 
/-- A category has an initial object if it has a colimit over the empty diagram.
Use `hasInitial_of_unique` to construct instances.
-/
abbrev HasInitial :=
  HasColimitsOfShape (Discrete.{0} PEmpty) C
Existence of Initial Object in a Category
Informal description
A category $\mathcal{C}$ has an initial object if it has a colimit over the empty diagram.
CategoryTheory.Limits.hasTerminalChangeDiagram theorem
(h : HasLimit F₁) : HasLimit F₂
Full source 
theorem hasTerminalChangeDiagram (h : HasLimit F₁) : HasLimit F₂ :=
  ⟨⟨⟨⟨limit F₁, by aesop_cat, by simp⟩,
    isLimitChangeEmptyCone C (limit.isLimit F₁) _ (eqToIso rfl)⟩⟩⟩
Preservation of Limits under Diagram Change
Informal description
Given a functor $F_1$ in a category $\mathcal{C}$ that has a limit, and a functor $F_2$ obtained by changing the diagram of $F_1$, then $F_2$ also has a limit.
CategoryTheory.Limits.hasTerminalChangeUniverse theorem
[h : HasLimitsOfShape (Discrete.{w} PEmpty) C] : HasLimitsOfShape (Discrete.{w'} PEmpty) C
Full source 
theorem hasTerminalChangeUniverse [h : HasLimitsOfShape (Discrete.{w} PEmpty) C] :
    HasLimitsOfShape (Discrete.{w'} PEmpty) C where
  has_limit _ := hasTerminalChangeDiagram C (h.1 (Functor.empty C))
Terminal Objects Exist in All Universe Levels if They Exist in One
Informal description
If a category $\mathcal{C}$ has limits of shape `Discrete.{w} PEmpty` (i.e., terminal objects in universe level $w$), then it also has limits of shape `Discrete.{w'} PEmpty` (terminal objects in universe level $w'$).
CategoryTheory.Limits.hasInitialChangeDiagram theorem
(h : HasColimit F₁) : HasColimit F₂
Full source 
theorem hasInitialChangeDiagram (h : HasColimit F₁) : HasColimit F₂ :=
  ⟨⟨⟨⟨colimit F₁, by aesop_cat, by simp⟩,
    isColimitChangeEmptyCocone C (colimit.isColimit F₁) _ (eqToIso rfl)⟩⟩⟩
Preservation of Colimits under Diagram Change
Informal description
If a functor $F_1$ has a colimit in a category $C$, then any functor $F_2$ obtained by changing the diagram of $F_1$ also has a colimit in $C$.
CategoryTheory.Limits.hasInitialChangeUniverse theorem
[h : HasColimitsOfShape (Discrete.{w} PEmpty) C] : HasColimitsOfShape (Discrete.{w'} PEmpty) C
Full source 
theorem hasInitialChangeUniverse [h : HasColimitsOfShape (Discrete.{w} PEmpty) C] :
    HasColimitsOfShape (Discrete.{w'} PEmpty) C where
  has_colimit _ := hasInitialChangeDiagram C (h.1 (Functor.empty C))
Universe Independence of Initial Object Existence
Informal description
If a category $C$ has colimits of shape `Discrete.{w} PEmpty` (i.e., colimits over the empty diagram in universe level $w$), then it also has colimits of shape `Discrete.{w'} PEmpty` (i.e., colimits over the empty diagram in any other universe level $w'$).
CategoryTheory.Limits.terminal abbrev
[HasTerminal C] : C
Full source 
/-- 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.
-/
abbrev terminal [HasTerminal C] : C :=
  limit (Functor.empty.{0} C)
Terminal Object in a Category ($\top_{\mathcal{C}}$)
Informal description
The terminal object in a category $\mathcal{C}$, if it exists, is denoted by $\top_{\mathcal{C}}$. It is characterized by the property that for every object $X \in \mathcal{C}$, there exists a unique morphism $X \to \top_{\mathcal{C}}$.
CategoryTheory.Limits.initial abbrev
[HasInitial C] : C
Full source 
/-- 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.
-/
abbrev initial [HasInitial C] : C :=
  colimit (Functor.empty.{0} C)
Initial Object in a Category ($\bot_{\mathcal{C}}$)
Informal description
Given a category $\mathcal{C}$ that has an initial object (i.e., $\mathcal{C}$ satisfies `HasInitial`), the term `initial` (denotable as $\bot_{\mathcal{C}}$) represents an arbitrarily chosen initial object in $\mathcal{C}$. This object is characterized by the property that for every object $X$ in $\mathcal{C}$, there exists a unique morphism from $\bot_{\mathcal{C}}$ to $X$.
CategoryTheory.Limits.hasTerminal_of_unique theorem
(X : C) [∀ Y, Nonempty (Y ⟶ X)] [∀ Y, Subsingleton (Y ⟶ X)] : HasTerminal C
Full source 
/-- 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 hasTerminal_of_unique (X : C) [∀ Y, Nonempty (Y ⟶ X)] [∀ Y, Subsingleton (Y ⟶ X)] :
    HasTerminal C where
  has_limit F := .mk ⟨_, (isTerminalEquivUnique F X).invFun fun _ ↦
    ⟨Classical.inhabited_of_nonempty', (Subsingleton.elim · _)⟩⟩
Existence of Terminal Object via Unique Morphisms
Informal description
Let $\mathcal{C}$ be a category and $X$ an object in $\mathcal{C}$. If for every object $Y$ in $\mathcal{C}$ there exists a morphism $Y \to X$ (i.e., $\text{Hom}(Y, X)$ is nonempty) and all such morphisms are unique (i.e., $\text{Hom}(Y, X)$ is a subsingleton), then $\mathcal{C}$ has a terminal object.
CategoryTheory.Limits.IsTerminal.hasTerminal theorem
{X : C} (h : IsTerminal X) : HasTerminal C
Full source 
theorem IsTerminal.hasTerminal {X : C} (h : IsTerminal X) : HasTerminal C :=
  { has_limit := fun F => HasLimit.mk ⟨⟨X, by aesop_cat, by simp⟩,
    isLimitChangeEmptyCone _ h _ (Iso.refl _)⟩ }
Terminal Object Implies Existence of Terminal Object in Category
Informal description
Given an object $X$ in a category $\mathcal{C}$, if $X$ is terminal (i.e., for every object $Y \in \mathcal{C}$ there exists a unique morphism $Y \to X$), then the category $\mathcal{C}$ has a terminal object.
CategoryTheory.Limits.hasInitial_of_unique theorem
(X : C) [∀ Y, Nonempty (X ⟶ Y)] [∀ Y, Subsingleton (X ⟶ Y)] : HasInitial C
Full source 
/-- 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. -/
theorem hasInitial_of_unique (X : C) [∀ Y, Nonempty (X ⟶ Y)] [∀ Y, Subsingleton (X ⟶ Y)] :
    HasInitial C where
  has_colimit F := .mk ⟨_, (isInitialEquivUnique F X).invFun fun _ ↦
    ⟨Classical.inhabited_of_nonempty', (Subsingleton.elim · _)⟩⟩
Existence of Initial Object via Unique Morphisms
Informal description
Let $\mathcal{C}$ be a category and $X$ an object in $\mathcal{C}$. If for every object $Y$ in $\mathcal{C}$ there exists a morphism from $X$ to $Y$ (i.e., $\operatorname{Hom}(X, Y)$ is nonempty) and all such morphisms are unique (i.e., $\operatorname{Hom}(X, Y)$ is a subsingleton), then $\mathcal{C}$ has an initial object.
CategoryTheory.Limits.IsInitial.hasInitial theorem
{X : C} (h : IsInitial X) : HasInitial C
Full source 
theorem IsInitial.hasInitial {X : C} (h : IsInitial X) : HasInitial C where
  has_colimit F :=
    HasColimit.mk ⟨⟨X, by aesop_cat, by simp⟩, isColimitChangeEmptyCocone _ h _ (Iso.refl _)⟩
Initial Object Implies Existence of Initial Object in Category
Informal description
If an object $X$ in a category $\mathcal{C}$ is initial (i.e., for every object $Y$ in $\mathcal{C}$, there exists a unique morphism from $X$ to $Y$), then the category $\mathcal{C}$ has an initial object.
CategoryTheory.Limits.terminal.from abbrev
[HasTerminal C] (P : C) : P ⟶ ⊤_ C
Full source 
/-- The map from an object to the terminal object. -/
abbrev terminal.from [HasTerminal C] (P : C) : P ⟶ ⊤_ C :=
  limit.lift (Functor.empty C) (asEmptyCone P)
Universal Morphism to Terminal Object
Informal description
For any object $P$ in a category $\mathcal{C}$ that has a terminal object $\top_{\mathcal{C}}$, there exists a unique morphism from $P$ to $\top_{\mathcal{C}}$, denoted by $P \to \top_{\mathcal{C}}$.
CategoryTheory.Limits.initial.to abbrev
[HasInitial C] (P : C) : ⊥_ C ⟶ P
Full source 
/-- The map to an object from the initial object. -/
abbrev initial.to [HasInitial C] (P : C) : ⊥_ C⊥_ C ⟶ P :=
  colimit.desc (Functor.empty C) (asEmptyCocone P)
Universal Morphism from Initial Object
Informal description
Given a category $\mathcal{C}$ with an initial object $\bot_{\mathcal{C}}$, for any object $P$ in $\mathcal{C}$, there exists a unique morphism from $\bot_{\mathcal{C}}$ to $P$.
CategoryTheory.Limits.terminalIsTerminal definition
[HasTerminal C] : IsTerminal (⊤_ C)
Full source 
/-- A terminal object is terminal. -/
def terminalIsTerminal [HasTerminal C] : IsTerminal (⊤_ C) where
  lift _ := terminal.from _
Terminal object satisfies universal property
Informal description
Given a category $\mathcal{C}$ with a terminal object $\top_{\mathcal{C}}$, the object $\top_{\mathcal{C}}$ satisfies the universal property of being terminal: for every object $X$ in $\mathcal{C}$, there exists a unique morphism from $X$ to $\top_{\mathcal{C}}$.
CategoryTheory.Limits.initialIsInitial definition
[HasInitial C] : IsInitial (⊥_ C)
Full source 
/-- An initial object is initial. -/
def initialIsInitial [HasInitial C] : IsInitial (⊥_ C) where
  desc _ := initial.to _
Initial object satisfies universal property
Informal description
Given a category $\mathcal{C}$ with an initial object $\bot_{\mathcal{C}}$, the object $\bot_{\mathcal{C}}$ satisfies the universal property of being initial: for every object $X$ in $\mathcal{C}$, there exists a unique morphism from $\bot_{\mathcal{C}}$ to $X$.
CategoryTheory.Limits.uniqueToTerminal instance
[HasTerminal C] (P : C) : Unique (P ⟶ ⊤_ C)
Full source 
instance uniqueToTerminal [HasTerminal C] (P : C) : Unique (P ⟶ ⊤_ C) :=
  isTerminalEquivUnique _ (⊤_ C) terminalIsTerminal P
Uniqueness of Morphisms to Terminal Object
Informal description
For any category $\mathcal{C}$ with a terminal object $\top_{\mathcal{C}}$ and any object $P$ in $\mathcal{C}$, there is a unique morphism from $P$ to $\top_{\mathcal{C}}$.
CategoryTheory.Limits.uniqueFromInitial instance
[HasInitial C] (P : C) : Unique (⊥_ C ⟶ P)
Full source 
instance uniqueFromInitial [HasInitial C] (P : C) : Unique (⊥_ C⊥_ C ⟶ P) :=
  isInitialEquivUnique _ (⊥_ C) initialIsInitial P
Uniqueness of Morphisms from Initial Object
Informal description
For any category $\mathcal{C}$ with an initial object $\bot_{\mathcal{C}}$ and any object $P$ in $\mathcal{C}$, there is a unique morphism from $\bot_{\mathcal{C}}$ to $P$.
CategoryTheory.Limits.terminal.hom_ext theorem
[HasTerminal C] {P : C} (f g : P ⟶ ⊤_ C) : f = g
Full source 
@[ext] theorem terminal.hom_ext [HasTerminal C] {P : C} (f g : P ⟶ ⊤_ C) : f = g := by ext ⟨⟨⟩⟩
Uniqueness of Morphisms to Terminal Object
Informal description
In a category $\mathcal{C}$ with a terminal object $\top_{\mathcal{C}}$, any two morphisms $f, g : P \to \top_{\mathcal{C}}$ from an object $P$ in $\mathcal{C}$ are equal.
CategoryTheory.Limits.initial.hom_ext theorem
[HasInitial C] {P : C} (f g : ⊥_ C ⟶ P) : f = g
Full source 
@[ext] theorem initial.hom_ext [HasInitial C] {P : C} (f g : ⊥_ C⊥_ C ⟶ P) : f = g := by ext ⟨⟨⟩⟩
Uniqueness of Morphisms from Initial Object
Informal description
In a category $\mathcal{C}$ with an initial object $\bot_{\mathcal{C}}$, any two morphisms $f, g : \bot_{\mathcal{C}} \to P$ to an object $P$ in $\mathcal{C}$ are equal.
CategoryTheory.Limits.terminal.comp_from theorem
[HasTerminal C] {P Q : C} (f : P ⟶ Q) : f ≫ terminal.from Q = terminal.from P
Full source 
@[reassoc (attr := simp)]
theorem terminal.comp_from [HasTerminal C] {P Q : C} (f : P ⟶ Q) :
    f ≫ terminal.from Q = terminal.from P := by
  simp [eq_iff_true_of_subsingleton]
Composition with Terminal Morphism Preserves Universality
Informal description
In a category $\mathcal{C}$ with a terminal object $\top_{\mathcal{C}}$, for any morphism $f : P \to Q$ between objects $P$ and $Q$ in $\mathcal{C}$, the composition of $f$ with the unique morphism from $Q$ to $\top_{\mathcal{C}}$ is equal to the unique morphism from $P$ to $\top_{\mathcal{C}}$. That is, $f \circ (Q \to \top_{\mathcal{C}}) = (P \to \top_{\mathcal{C}})$.
CategoryTheory.Limits.initial.to_comp theorem
[HasInitial C] {P Q : C} (f : P ⟶ Q) : initial.to P ≫ f = initial.to Q
Full source 
@[simp, reassoc]
theorem initial.to_comp [HasInitial C] {P Q : C} (f : P ⟶ Q) : initial.toinitial.to P ≫ f = initial.to Q := by
  simp [eq_iff_true_of_subsingleton]
Composition with Morphism from Initial Object Preserves Uniqueness
Informal description
In a category $\mathcal{C}$ with an initial object $\bot_{\mathcal{C}}$, for any morphism $f : P \to Q$ between objects $P$ and $Q$ in $\mathcal{C}$, the composition of the unique morphism $\bot_{\mathcal{C}} \to P$ with $f$ is equal to the unique morphism $\bot_{\mathcal{C}} \to Q$. That is, the following diagram commutes: \[ \bot_{\mathcal{C}} \xrightarrow{\text{initial.to } P} P \xrightarrow{f} Q = \bot_{\mathcal{C}} \xrightarrow{\text{initial.to } Q} Q \]
CategoryTheory.Limits.initialIsoIsInitial definition
[HasInitial C] {P : C} (t : IsInitial P) : ⊥_ C ≅ P
Full source 
/-- The (unique) isomorphism between the chosen initial object and any other initial object. -/
@[simps!]
def initialIsoIsInitial [HasInitial C] {P : C} (t : IsInitial P) : ⊥_ C⊥_ C ≅ P :=
  initialIsInitial.uniqueUpToIso t
Isomorphism between initial objects
Informal description
Given a category $\mathcal{C}$ with an initial object $\bot_{\mathcal{C}}$ and an object $P$ that satisfies the universal property of being initial, there exists a unique isomorphism between $\bot_{\mathcal{C}}$ and $P$.
CategoryTheory.Limits.terminalIsoIsTerminal definition
[HasTerminal C] {P : C} (t : IsTerminal P) : ⊤_ C ≅ P
Full source 
/-- The (unique) isomorphism between the chosen terminal object and any other terminal object. -/
@[simps!]
def terminalIsoIsTerminal [HasTerminal C] {P : C} (t : IsTerminal P) : ⊤_ C⊤_ C ≅ P :=
  terminalIsTerminal.uniqueUpToIso t
Isomorphism between terminal objects
Informal description
Given a category $\mathcal{C}$ with a terminal object $\top_{\mathcal{C}}$ and an object $P$ in $\mathcal{C}$ that satisfies the universal property of being terminal, there exists a unique isomorphism between $\top_{\mathcal{C}}$ and $P$.
CategoryTheory.Limits.terminal.isSplitMono_from instance
{Y : C} [HasTerminal C] (f : ⊤_ C ⟶ Y) : IsSplitMono f
Full source 
/-- Any morphism from a terminal object is split mono. -/
instance terminal.isSplitMono_from {Y : C} [HasTerminal C] (f : ⊤_ C⊤_ C ⟶ Y) : IsSplitMono f :=
  IsTerminal.isSplitMono_from terminalIsTerminal _
Morphisms from Terminal Objects are Split Monomorphisms
Informal description
For any category $\mathcal{C}$ with a terminal object $\top_{\mathcal{C}}$ and any morphism $f : \top_{\mathcal{C}} \to Y$ where $Y$ is an object in $\mathcal{C}$, the morphism $f$ is a split monomorphism.
CategoryTheory.Limits.initial.isSplitEpi_to instance
{Y : C} [HasInitial C] (f : Y ⟶ ⊥_ C) : IsSplitEpi f
Full source 
/-- Any morphism to an initial object is split epi. -/
instance initial.isSplitEpi_to {Y : C} [HasInitial C] (f : Y ⟶ ⊥_ C) : IsSplitEpi f :=
  IsInitial.isSplitEpi_to initialIsInitial _
Morphisms to Initial Objects are Split Epimorphisms
Informal description
For any category $\mathcal{C}$ with an initial object $\bot_{\mathcal{C}}$ and any morphism $f : Y \to \bot_{\mathcal{C}}$ where $Y$ is an object in $\mathcal{C}$, the morphism $f$ is a split epimorphism.
CategoryTheory.Limits.instHasLimitObjFunctorConstTerminal instance
{J : Type*} [Category J] {C : Type*} [Category C] [HasTerminal C] : HasLimit ((CategoryTheory.Functor.const J).obj (⊤_ C))
Full source 
instance {J : Type*} [Category J] {C : Type*} [Category C] [HasTerminal C] :
    HasLimit ((CategoryTheory.Functor.const J).obj (⊤_ C)) :=
  HasLimit.mk
    { cone :=
        { pt := ⊤_ C
          π := { app := fun _ => terminal.from _ } }
      isLimit := { lift := fun _ => terminal.from _ } }
Existence of Limits for Constant Functors to Terminal Objects
Informal description
For any category $\mathcal{C}$ with a terminal object and any small category $J$, the constant functor from $J$ to the terminal object of $\mathcal{C}$ has a limit.
CategoryTheory.Limits.limitConstTerminal definition
{J : Type*} [Category J] {C : Type*} [Category C] [HasTerminal C] : limit ((CategoryTheory.Functor.const J).obj (⊤_ C)) ≅ ⊤_ C
Full source 
/-- The limit of the constant `⊤_ C` functor is `⊤_ C`. -/
@[simps hom]
def limitConstTerminal {J : Type*} [Category J] {C : Type*} [Category C] [HasTerminal C] :
    limitlimit ((CategoryTheory.Functor.const J).obj (⊤_ C)) ≅ ⊤_ C where
  hom := terminal.from _
  inv :=
    limit.lift ((CategoryTheory.Functor.const J).obj (⊤_ C))
      { pt := ⊤_ C
        π := { app := fun _ => terminal.from _ } }
Limit of constant functor to terminal object is terminal
Informal description
For any category $\mathcal{C}$ with a terminal object $\top_{\mathcal{C}}$ and any small category $J$, the limit of the constant functor from $J$ to $\top_{\mathcal{C}}$ is isomorphic to $\top_{\mathcal{C}}$. The isomorphism consists of: - A morphism from the limit to $\top_{\mathcal{C}}$ given by the universal morphism from the limit object to the terminal object - An inverse morphism constructed via the universal property of limits, using the terminal object's universal property
CategoryTheory.Limits.limitConstTerminal_inv_π theorem
{J : Type*} [Category J] {C : Type*} [Category C] [HasTerminal C] {j : J} : limitConstTerminal.inv ≫ limit.π ((CategoryTheory.Functor.const J).obj (⊤_ C)) j = terminal.from _
Full source 
@[reassoc (attr := simp)]
theorem limitConstTerminal_inv_π {J : Type*} [Category J] {C : Type*} [Category C] [HasTerminal C]
    {j : J} :
    limitConstTerminallimitConstTerminal.inv ≫ limit.π ((CategoryTheory.Functor.const J).obj (⊤_ C)) j =
      terminal.from _ := by aesop_cat
Composition of Inverse Limit Isomorphism with Projection Equals Terminal Morphism
Informal description
For any category $\mathcal{C}$ with a terminal object $\top_{\mathcal{C}}$, any small category $J$, and any object $j \in J$, the composition of the inverse morphism of the isomorphism $\text{limitConstTerminal}$ with the projection morphism $\pi_j$ from the limit of the constant functor to $\top_{\mathcal{C}}$ equals the universal morphism from the terminal object to itself, i.e., \[ \text{limitConstTerminal.inv} \circ \pi_j = \text{terminal.from} \_\ .\]
CategoryTheory.Limits.instHasColimitObjFunctorConstInitial instance
{J : Type*} [Category J] {C : Type*} [Category C] [HasInitial C] : HasColimit ((CategoryTheory.Functor.const J).obj (⊥_ C))
Full source 
instance {J : Type*} [Category J] {C : Type*} [Category C] [HasInitial C] :
    HasColimit ((CategoryTheory.Functor.const J).obj (⊥_ C)) :=
  HasColimit.mk
    { cocone :=
        { pt := ⊥_ C
          ι := { app := fun _ => initial.to _ } }
      isColimit := { desc := fun _ => initial.to _ } }
Colimit of Constant Functor to Initial Object
Informal description
For any category $\mathcal{C}$ with an initial object $\bot_{\mathcal{C}}$ and any small category $J$, the constant functor $J \to \mathcal{C}$ sending every object to $\bot_{\mathcal{C}}$ has a colimit, which is isomorphic to $\bot_{\mathcal{C}}$.
CategoryTheory.Limits.colimitConstInitial definition
{J : Type*} [Category J] {C : Type*} [Category C] [HasInitial C] : colimit ((CategoryTheory.Functor.const J).obj (⊥_ C)) ≅ ⊥_ C
Full source 
/-- The colimit of the constant `⊥_ C` functor is `⊥_ C`. -/
@[simps inv]
def colimitConstInitial {J : Type*} [Category J] {C : Type*} [Category C] [HasInitial C] :
    colimitcolimit ((CategoryTheory.Functor.const J).obj (⊥_ C)) ≅ ⊥_ C where
  hom :=
    colimit.desc ((CategoryTheory.Functor.const J).obj (⊥_ C))
      { pt := ⊥_ C
        ι := { app := fun _ => initial.to _ } }
  inv := initial.to _
Colimit of Constant Functor to Initial Object is Initial Object
Informal description
For any category $\mathcal{C}$ with an initial object $\bot_{\mathcal{C}}$ and any small category $J$, the colimit of the constant functor $J \to \mathcal{C}$ sending every object to $\bot_{\mathcal{C}}$ is isomorphic to $\bot_{\mathcal{C}}$. The isomorphism is given by the universal property of the colimit and the initial object.
CategoryTheory.Limits.ι_colimitConstInitial_hom theorem
{J : Type*} [Category J] {C : Type*} [Category C] [HasInitial C] {j : J} : colimit.ι ((CategoryTheory.Functor.const J).obj (⊥_ C)) j ≫ colimitConstInitial.hom = initial.to _
Full source 
@[reassoc (attr := simp)]
theorem ι_colimitConstInitial_hom {J : Type*} [Category J] {C : Type*} [Category C] [HasInitial C]
    {j : J} :
    colimit.ιcolimit.ι ((CategoryTheory.Functor.const J).obj (⊥_ C)) j ≫ colimitConstInitial.hom =
      initial.to _ := by aesop_cat
Compatibility of Colimit Inclusion with Initial Object Morphism
Informal description
For any category $\mathcal{C}$ with an initial object $\bot_{\mathcal{C}}$ and any small category $J$, the composition of the colimit inclusion morphism $\iota_j$ (for any object $j \in J$) with the isomorphism $\text{colimitConstInitial.hom}$ (from the colimit of the constant functor $J \to \mathcal{C}$ sending every object to $\bot_{\mathcal{C}}$ to $\bot_{\mathcal{C}}$ itself) equals the unique morphism $\bot_{\mathcal{C}} \to \text{colimitConstInitial}$.
CategoryTheory.Limits.initial.mono_from instance
[HasInitial C] [InitialMonoClass C] (X : C) (f : ⊥_ C ⟶ X) : Mono f
Full source 
instance (priority := 100) initial.mono_from [HasInitial C] [InitialMonoClass C] (X : C)
    (f : ⊥_ C⊥_ C ⟶ X) : Mono f :=
  initialIsInitial.mono_from f
Monomorphisms from Initial Objects in InitialMonoClass Categories
Informal description
In a category $\mathcal{C}$ with an initial object $\bot_{\mathcal{C}}$ and satisfying the `InitialMonoClass` property, every morphism $f$ from $\bot_{\mathcal{C}}$ to any object $X$ in $\mathcal{C}$ is a monomorphism.
CategoryTheory.Limits.InitialMonoClass.of_initial theorem
[HasInitial C] (h : ∀ X : C, Mono (initial.to X)) : InitialMonoClass C
Full source 
/-- To show a category is an `InitialMonoClass` it suffices to show every morphism out of the
initial object is a monomorphism. -/
theorem InitialMonoClass.of_initial [HasInitial C] (h : ∀ X : C, Mono (initial.to X)) :
    InitialMonoClass C :=
  InitialMonoClass.of_isInitial initialIsInitial h
InitialMonoClass Criterion via Monomorphisms from Initial Object
Informal description
Let $\mathcal{C}$ be a category with an initial object $\bot_{\mathcal{C}}$. If for every object $X$ in $\mathcal{C}$, the unique morphism $\bot_{\mathcal{C}} \to X$ is a monomorphism, then $\mathcal{C}$ is an `InitialMonoClass` category.
CategoryTheory.Limits.InitialMonoClass.of_terminal theorem
[HasInitial C] [HasTerminal C] (h : Mono (initial.to (⊤_ C))) : InitialMonoClass C
Full source 
/-- To show a category is an `InitialMonoClass` it suffices to show the unique morphism from the
initial object to a terminal object is a monomorphism. -/
theorem InitialMonoClass.of_terminal [HasInitial C] [HasTerminal C] (h : Mono (initial.to (⊤_ C))) :
    InitialMonoClass C :=
  InitialMonoClass.of_isTerminal initialIsInitial terminalIsTerminal h
InitialMonoClass Criterion via Terminal Object Morphism
Informal description
Let $\mathcal{C}$ be a category with an initial object $\bot_{\mathcal{C}}$ and a terminal object $\top_{\mathcal{C}}$. If the unique morphism $\bot_{\mathcal{C}} \to \top_{\mathcal{C}}$ is a monomorphism, then $\mathcal{C}$ is an `InitialMonoClass` category.
CategoryTheory.Limits.terminalComparison definition
[HasTerminal C] [HasTerminal D] : G.obj (⊤_ C) ⟶ ⊤_ D
Full source 
/-- 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
`CategoryTheory.Limits.PreservesTerminal.ofIsoComparison`.
-/
def terminalComparison [HasTerminal C] [HasTerminal D] : G.obj (⊤_ C) ⟶ ⊤_ D :=
  terminal.from _
Comparison morphism from image of terminal object to terminal object
Informal description
Given categories $\mathcal{C}$ and $\mathcal{D}$ each with a terminal object, and a functor $G : \mathcal{C} \to \mathcal{D}$, the morphism $G(\top_{\mathcal{C}}) \to \top_{\mathcal{D}}$ is the unique morphism from the image of the terminal object of $\mathcal{C}$ under $G$ to the terminal object of $\mathcal{D}$.
CategoryTheory.Limits.initialComparison definition
[HasInitial C] [HasInitial D] : ⊥_ D ⟶ G.obj (⊥_ C)
Full source 
/--
The comparison morphism from the initial object in the target category to the image of the initial
object.
-/
def initialComparison [HasInitial C] [HasInitial D] : ⊥_ D⊥_ D ⟶ G.obj (⊥_ C) :=
  initial.to _
Comparison morphism from initial object to image of initial object
Informal description
Given categories $\mathcal{C}$ and $\mathcal{D}$ each with an initial object, and a functor $G : \mathcal{C} \to \mathcal{D}$, the morphism $\bot_{\mathcal{D}} \to G(\bot_{\mathcal{C}})$ is the unique morphism from the initial object of $\mathcal{D}$ to the image of the initial object of $\mathcal{C}$ under $G$.
CategoryTheory.Limits.hasLimit_of_domain_hasInitial instance
[HasInitial J] {F : J ⥤ C} : HasLimit F
Full source 
instance hasLimit_of_domain_hasInitial [HasInitial J] {F : J ⥤ C} : HasLimit F :=
  HasLimit.mk { cone := _, isLimit := limitOfDiagramInitial (initialIsInitial) F }
Existence of Limits for Functors from Categories with Initial Objects
Informal description
For any category $\mathcal{C}$ and any functor $F : \mathcal{J} \to \mathcal{C}$ where $\mathcal{J}$ has an initial object, the functor $F$ has a limit.
CategoryTheory.Limits.limitOfInitial abbrev
(F : J ⥤ C) [HasInitial J] : limit F ≅ F.obj (⊥_ J)
Full source 
/-- For a functor `F : J ⥤ C`, if `J` has an initial object then the image of it is isomorphic
to the limit of `F`. -/
abbrev limitOfInitial (F : J ⥤ C) [HasInitial J] : limitlimit F ≅ F.obj (⊥_ J) :=
  IsLimit.conePointUniqueUpToIso (limit.isLimit _) (limitOfDiagramInitial initialIsInitial F)
Limit of Functor from Category with Initial Object is Image of Initial Object
Informal description
For any functor $F \colon \mathcal{J} \to \mathcal{C}$ where $\mathcal{J}$ has an initial object $\bot_{\mathcal{J}}$, the limit of $F$ is isomorphic to $F(\bot_{\mathcal{J}})$.
CategoryTheory.Limits.hasLimit_of_domain_hasTerminal instance
[HasTerminal J] {F : J ⥤ C} [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : HasLimit F
Full source 
instance hasLimit_of_domain_hasTerminal [HasTerminal J] {F : J ⥤ C}
    [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : HasLimit F :=
  HasLimit.mk { cone := _, isLimit := limitOfDiagramTerminal (terminalIsTerminal) F }
Existence of Limits for Functors from Categories with Terminal Objects and Isomorphic Images
Informal description
For any category $\mathcal{J}$ with a terminal object and any functor $F \colon \mathcal{J} \to \mathcal{C}$ where all morphisms in $\mathcal{J}$ are mapped to isomorphisms in $\mathcal{C}$, the limit of $F$ exists.
CategoryTheory.Limits.limitOfTerminal abbrev
(F : J ⥤ C) [HasTerminal J] [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : limit F ≅ F.obj (⊤_ J)
Full source 
/-- 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`. -/
abbrev limitOfTerminal (F : J ⥤ C) [HasTerminal J] [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] :
    limitlimit F ≅ F.obj (⊤_ J) :=
  IsLimit.conePointUniqueUpToIso (limit.isLimit _) (limitOfDiagramTerminal terminalIsTerminal F)
Limit of Functor from Category with Terminal Object and Isomorphic Images
Informal description
For any functor $F \colon \mathcal{J} \to \mathcal{C}$ where $\mathcal{J}$ has a terminal object and all morphisms in $\mathcal{J}$ are mapped to isomorphisms in $\mathcal{C}$, the limit of $F$ is isomorphic to the image of the terminal object under $F$, i.e., $\text{limit}\, F \cong F(\top_{\mathcal{J}})$.
CategoryTheory.Limits.hasColimit_of_domain_hasTerminal instance
[HasTerminal J] {F : J ⥤ C} : HasColimit F
Full source 
instance hasColimit_of_domain_hasTerminal [HasTerminal J] {F : J ⥤ C} : HasColimit F :=
  HasColimit.mk { cocone := _, isColimit := colimitOfDiagramTerminal (terminalIsTerminal) F }
Existence of Colimits for Functors from Categories with Terminal Objects
Informal description
For any category $J$ with a terminal object and any functor $F \colon J \to C$, the colimit of $F$ exists.
CategoryTheory.Limits.colimitOfTerminal abbrev
(F : J ⥤ C) [HasTerminal J] : colimit F ≅ F.obj (⊤_ J)
Full source 
/-- For a functor `F : J ⥤ C`, if `J` has a terminal object then the image of it is isomorphic
to the colimit of `F`. -/
abbrev colimitOfTerminal (F : J ⥤ C) [HasTerminal J] : colimitcolimit F ≅ F.obj (⊤_ J) :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit _)
    (colimitOfDiagramTerminal terminalIsTerminal F)
Colimit of Functor from Category with Terminal Object is Image of Terminal Object
Informal description
For any functor $F \colon J \to C$ from a category $J$ with a terminal object, the colimit of $F$ is isomorphic to the image of the terminal object under $F$, i.e., $\text{colimit}\, F \cong F(\top_J)$.
CategoryTheory.Limits.hasColimit_of_domain_hasInitial instance
[HasInitial J] {F : J ⥤ C} [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : HasColimit F
Full source 
instance hasColimit_of_domain_hasInitial [HasInitial J] {F : J ⥤ C}
    [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : HasColimit F :=
  HasColimit.mk { cocone := _, isColimit := colimitOfDiagramInitial (initialIsInitial) F }
Existence of Colimits for Functors from Categories with Initial Objects and Isomorphic Images
Informal description
For any category $J$ with an initial object and any functor $F \colon J \to C$ such that $F$ maps every morphism in $J$ to an isomorphism in $C$, the colimit of $F$ exists.
CategoryTheory.Limits.colimitOfInitial abbrev
(F : J ⥤ C) [HasInitial J] [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : colimit F ≅ F.obj (⊥_ J)
Full source 
/-- 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`. -/
abbrev colimitOfInitial (F : J ⥤ C) [HasInitial J] [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] :
    colimitcolimit F ≅ F.obj (⊥_ J) :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit _)
    (colimitOfDiagramInitial initialIsInitial _)
Colimit of Functor from Category with Initial Object and Isomorphic Images
Informal description
For any functor $F \colon J \to C$ where $J$ has an initial object $\bot_J$ and $F$ maps every morphism in $J$ to an isomorphism in $C$, the colimit of $F$ is isomorphic to $F(\bot_J)$, i.e., $\mathrm{colim}\, F \cong F(\bot_J)$.
CategoryTheory.Limits.isIso_π_of_isInitial theorem
{j : J} (I : IsInitial j) (F : J ⥤ C) [HasLimit F] : IsIso (limit.π F j)
Full source 
/-- If `j` is initial in the index category, then the map `limit.π F j` is an isomorphism.
-/
theorem isIso_π_of_isInitial {j : J} (I : IsInitial j) (F : J ⥤ C) [HasLimit F] :
    IsIso (limit.π F j) :=
  ⟨⟨limit.lift _ (coneOfDiagramInitial I F), ⟨by ext; simp, by simp⟩⟩⟩
Projection from Limit to Initial Object is Isomorphism
Informal description
Let $J$ be a category and $C$ another category. For any initial object $j$ in $J$ and any functor $F \colon J \to C$, if the limit of $F$ exists, then the projection map $\pi_j \colon \lim F \to F(j)$ is an isomorphism.
CategoryTheory.Limits.isIso_π_initial instance
[HasInitial J] (F : J ⥤ C) : IsIso (limit.π F (⊥_ J))
Full source 
instance isIso_π_initial [HasInitial J] (F : J ⥤ C) : IsIso (limit.π F (⊥_ J)) :=
  isIso_π_of_isInitial initialIsInitial F
Projection from Limit to Initial Object is Isomorphism
Informal description
For any category $\mathcal{J}$ with an initial object $\bot_{\mathcal{J}}$ and any functor $F \colon \mathcal{J} \to \mathcal{C}$, the projection morphism $\pi_{\bot_{\mathcal{J}}} \colon \lim F \to F(\bot_{\mathcal{J}})$ is an isomorphism.
CategoryTheory.Limits.isIso_π_of_isTerminal theorem
{j : J} (I : IsTerminal j) (F : J ⥤ C) [HasLimit F] [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : IsIso (limit.π F j)
Full source 
theorem isIso_π_of_isTerminal {j : J} (I : IsTerminal j) (F : J ⥤ C) [HasLimit F]
    [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : IsIso (limit.π F j) :=
  ⟨⟨limit.lift _ (coneOfDiagramTerminal I F), by ext; simp, by simp⟩⟩
Projection from Limit to Terminal Object is Isomorphism
Informal description
Let $J$ be a category and $C$ another category. Given an object $j$ in $J$ that is terminal, and a functor $F \colon J \to C$ such that: 1. The limit of $F$ exists in $C$, and 2. For every morphism $f \colon i \to j$ in $J$, the morphism $F(f)$ is an isomorphism in $C$, then the projection morphism $\pi_j \colon \lim F \to F(j)$ is an isomorphism in $C$.
CategoryTheory.Limits.isIso_π_terminal instance
[HasTerminal J] (F : J ⥤ C) [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : IsIso (limit.π F (⊤_ J))
Full source 
instance isIso_π_terminal [HasTerminal J] (F : J ⥤ C) [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] :
    IsIso (limit.π F (⊤_ J)) :=
  isIso_π_of_isTerminal terminalIsTerminal F
Isomorphism of Limit Projection at Terminal Object
Informal description
For any category $\mathcal{J}$ with a terminal object and any functor $F \colon \mathcal{J} \to \mathcal{C}$ where all morphisms in $\mathcal{J}$ are mapped to isomorphisms in $\mathcal{C}$, the projection morphism $\pi_{\top_{\mathcal{J}}} \colon \lim F \to F(\top_{\mathcal{J}})$ from the limit of $F$ to the image of the terminal object under $F$ is an isomorphism.
CategoryTheory.Limits.isIso_ι_of_isTerminal theorem
{j : J} (I : IsTerminal j) (F : J ⥤ C) [HasColimit F] : IsIso (colimit.ι F j)
Full source 
/-- If `j` is terminal in the index category, then the map `colimit.ι F j` is an isomorphism.
-/
theorem isIso_ι_of_isTerminal {j : J} (I : IsTerminal j) (F : J ⥤ C) [HasColimit F] :
    IsIso (colimit.ι F j) :=
  ⟨⟨colimit.desc _ (coconeOfDiagramTerminal I F), ⟨by simp, by ext; simp⟩⟩⟩
Colimit Morphism at Terminal Object is Isomorphism
Informal description
Let $J$ be a category and $C$ another category. For any terminal object $j$ in $J$ and any functor $F \colon J \to C$, if $C$ has colimits of shape $J$, then the morphism $\iota_j \colon F(j) \to \text{colim}\, F$ induced by the colimit construction is an isomorphism.
CategoryTheory.Limits.isIso_ι_terminal instance
[HasTerminal J] (F : J ⥤ C) : IsIso (colimit.ι F (⊤_ J))
Full source 
instance isIso_ι_terminal [HasTerminal J] (F : J ⥤ C) : IsIso (colimit.ι F (⊤_ J)) :=
  isIso_ι_of_isTerminal terminalIsTerminal F
Colimit Inclusion at Terminal Object is Isomorphism
Informal description
For any category $J$ with a terminal object and any functor $F \colon J \to C$, the colimit inclusion morphism $\iota_{\top_J} \colon F(\top_J) \to \text{colim}\, F$ is an isomorphism.
CategoryTheory.Limits.isIso_ι_of_isInitial theorem
{j : J} (I : IsInitial j) (F : J ⥤ C) [HasColimit F] [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : IsIso (colimit.ι F j)
Full source 
theorem isIso_ι_of_isInitial {j : J} (I : IsInitial j) (F : J ⥤ C) [HasColimit F]
    [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : IsIso (colimit.ι F j) :=
  ⟨⟨colimit.desc _ (coconeOfDiagramInitial I F), by
    refine ⟨?_, by ext; simp⟩
    dsimp; simp only [colimit.ι_desc, coconeOfDiagramInitial_pt, coconeOfDiagramInitial_ι_app,
      Functor.const_obj_obj, IsInitial.to_self, Functor.map_id]
    dsimp [inv]; simp only [Category.id_comp, Category.comp_id, and_self]
    apply @Classical.choose_spec _ (fun x => x = 𝟙 F.obj j) _
  ⟩⟩
Colimit inclusion at initial object is isomorphism when all morphisms are isomorphisms
Informal description
Let $J$ be a category and $C$ another category. Given an initial object $j$ in $J$ (witnessed by $I : \text{IsInitial } j$) and a functor $F : J \to C$ such that: 1. The colimit of $F$ exists in $C$, 2. For every morphism $f : i \to j$ in $J$, the morphism $F(f)$ is an isomorphism in $C$, then the colimit inclusion morphism $\text{colimit.ι } F j$ is an isomorphism in $C$.
CategoryTheory.Limits.isIso_ι_initial instance
[HasInitial J] (F : J ⥤ C) [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : IsIso (colimit.ι F (⊥_ J))
Full source 
instance isIso_ι_initial [HasInitial J] (F : J ⥤ C) [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] :
    IsIso (colimit.ι F (⊥_ J)) :=
  isIso_ι_of_isInitial initialIsInitial F
Colimit Inclusion at Initial Object is Isomorphism
Informal description
For any category $J$ with an initial object $\bot_J$ and any functor $F \colon J \to C$ such that $F$ maps every morphism in $J$ to an isomorphism in $C$, the colimit inclusion morphism $\text{colimit.ι } F (\bot_J)$ is an isomorphism in $C$.