Initial and terminal objects in a category.

References

• Stacks: Initial and final objects

@[simp]

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

@[simp]

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

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

Construct a cone for the empty diagram given an object.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

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

Construct a cocone for the empty diagram given an object.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

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

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

Equations

• CategoryTheory.Limits.IsTerminal X = CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.asEmptyCone X)

@[reducible, inline]

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

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

Equations

• CategoryTheory.Limits.IsInitial X = CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.asEmptyCocone X)

def CategoryTheory.Limits.isTerminalEquivUnique {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{1}) C) (Y : C) : CategoryTheory.Limits.IsLimit { pt := Y, π := { app := fun (X : CategoryTheory.Discrete PEmpty.{1}) => id (CategoryTheory.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.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• CategoryTheory.Limits.IsTerminal.ofUnique Y = { lift := fun (s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)) => default, fac := ⋯, uniq := ⋯ }

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

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

Equations

• CategoryTheory.Limits.IsTerminal.ofUniqueHom h uniq = CategoryTheory.Limits.IsTerminal.ofUnique Y

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

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

Equations

• CategoryTheory.Limits.isTerminalTop = CategoryTheory.Limits.IsTerminal.ofUnique ⊤

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

Transport a term of type IsTerminal across an isomorphism.

Equations

• hY.ofIso i = CategoryTheory.Limits.IsLimit.ofIsoLimit hY { hom := { hom := i.hom, w := ⋯ }, inv := { hom := i.inv, w := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

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

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.isInitialEquivUnique {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{1}) C) (X : C) : CategoryTheory.Limits.IsColimit { pt := X, ι := { app := fun (X_1 : CategoryTheory.Discrete PEmpty.{1}) => id (CategoryTheory.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.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• CategoryTheory.Limits.IsInitial.ofUnique X = { desc := fun (s : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.empty C)) => default, fac := ⋯, uniq := ⋯ }

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

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

Equations

• CategoryTheory.Limits.IsInitial.ofUniqueHom h uniq = CategoryTheory.Limits.IsInitial.ofUnique X

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

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

Equations

• CategoryTheory.Limits.isInitialBot = CategoryTheory.Limits.IsInitial.ofUnique ⊥

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

Transport a term of type is_initial across an isomorphism.

Equations

• hX.ofIso i = CategoryTheory.Limits.IsColimit.ofIsoColimit hX { hom := { hom := i.hom, w := ⋯ }, inv := { hom := i.inv, w := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Give the morphism to a terminal object from any other.

Equations

• t.from Y = t.lift (CategoryTheory.Limits.asEmptyCone Y)

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

Any two morphisms to a terminal object are equal.

@[simp]

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

@[simp]

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

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

Give the morphism from an initial object to any other.

Equations

• t.to Y = t.desc (CategoryTheory.Limits.asEmptyCocone Y)

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

Any two morphisms from an initial object are equal.

@[simp]

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

@[simp]

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

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

Any morphism from a terminal object is split mono.

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

Any morphism to an initial object is split epi.

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

Any morphism from a terminal object is mono.

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

Any morphism to an initial object is epi.

@[simp]

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

@[simp]

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

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

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

Equations

• hT.uniqueUpToIso hT' = { hom := hT'.from T, inv := hT.from T', hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[simp]

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

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

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

Equations

• hI.uniqueUpToIso hI' = { hom := hI.to I', inv := hI'.to I, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[reducible, inline]

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

A category has a terminal object if it has a limit over the empty diagram. Use hasTerminal_of_unique to construct instances.

Equations

• CategoryTheory.Limits.HasTerminal C = CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) C

@[reducible, inline]

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

A category has an initial object if it has a colimit over the empty diagram. Use hasInitial_of_unique to construct instances.

Equations

• CategoryTheory.Limits.HasInitial C = CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) C

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.hasTerminalChangeDiagram (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {F₁ : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w + 1} ) C} {F₂ : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w' + 1} ) C} (h : CategoryTheory.Limits.HasLimit F₁) : CategoryTheory.Limits.HasLimit F₂

theorem CategoryTheory.Limits.hasTerminalChangeUniverse (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [h : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete PEmpty.{w + 1} ) C] : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete PEmpty.{w' + 1} ) C

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.hasInitialChangeDiagram (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {F₁ : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w + 1} ) C} {F₂ : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w' + 1} ) C} (h : CategoryTheory.Limits.HasColimit F₁) : CategoryTheory.Limits.HasColimit F₂

theorem CategoryTheory.Limits.hasInitialChangeUniverse (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [h : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete PEmpty.{w + 1} ) C] : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete PEmpty.{w' + 1} ) C

@[reducible, inline]

abbrev CategoryTheory.Limits.terminal (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] : C

An arbitrary choice of terminal object, if one exists. You can use the notation ⊤_ C. This object is characterized by having a unique morphism from any object.

Equations

• (⊤_ C) = CategoryTheory.Limits.limit (CategoryTheory.Functor.empty C)

@[reducible, inline]

abbrev CategoryTheory.Limits.initial (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] : C

An arbitrary choice of initial object, if one exists. You can use the notation ⊥_ C. This object is characterized by having a unique morphism to any object.

Equations

• (⊥_ C) = CategoryTheory.Limits.colimit (CategoryTheory.Functor.empty C)

def CategoryTheory.Limits.«term⊤__» : Lean.ParserDescr

Notation for the terminal object in C

Equations

• CategoryTheory.Limits.«term⊤__» = Lean.ParserDescr.node `CategoryTheory.Limits.term⊤__ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊤_ ") (Lean.ParserDescr.cat `term 20))

def CategoryTheory.Limits.«term⊥__» : Lean.ParserDescr

Notation for the initial object in C

Equations

• CategoryTheory.Limits.«term⊥__» = Lean.ParserDescr.node `CategoryTheory.Limits.term⊥__ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊥_ ") (Lean.ParserDescr.cat `term 20))

theorem CategoryTheory.Limits.hasTerminal_of_unique {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) [h : (Y : C) → Unique (Y ⟶ X)] : CategoryTheory.Limits.HasTerminal C

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 CategoryTheory.Limits.IsTerminal.hasTerminal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (h : CategoryTheory.Limits.IsTerminal X) : CategoryTheory.Limits.HasTerminal C

theorem CategoryTheory.Limits.hasInitial_of_unique {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) [h : (Y : C) → Unique (X ⟶ Y)] : CategoryTheory.Limits.HasInitial C

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 CategoryTheory.Limits.IsInitial.hasInitial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (h : CategoryTheory.Limits.IsInitial X) : CategoryTheory.Limits.HasInitial C

@[reducible, inline]

abbrev CategoryTheory.Limits.terminal.from {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] (P : C) : P ⟶ ⊤_ C

The map from an object to the terminal object.

Equations

• CategoryTheory.Limits.terminal.from P = CategoryTheory.Limits.limit.lift (CategoryTheory.Functor.empty C) (CategoryTheory.Limits.asEmptyCone P)

@[reducible, inline]

abbrev CategoryTheory.Limits.initial.to {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] (P : C) : ⊥_ C ⟶ P

The map to an object from the initial object.

Equations

• CategoryTheory.Limits.initial.to P = CategoryTheory.Limits.colimit.desc (CategoryTheory.Functor.empty C) (CategoryTheory.Limits.asEmptyCocone P)

def CategoryTheory.Limits.terminalIsTerminal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Limits.IsTerminal (⊤_ C)

A terminal object is terminal.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.initialIsInitial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] : CategoryTheory.Limits.IsInitial (⊥_ C)

An initial object is initial.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Limits.uniqueToTerminal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] (P : C) : Unique (P ⟶ ⊤_ C)

Equations

• CategoryTheory.Limits.uniqueToTerminal P = (CategoryTheory.Limits.isTerminalEquivUnique (CategoryTheory.Functor.empty C) (⊤_ C)) CategoryTheory.Limits.terminalIsTerminal P

instance CategoryTheory.Limits.uniqueFromInitial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] (P : C) : Unique (⊥_ C ⟶ P)

Equations

• CategoryTheory.Limits.uniqueFromInitial P = (CategoryTheory.Limits.isInitialEquivUnique (CategoryTheory.Functor.empty C) (⊥_ C)) CategoryTheory.Limits.initialIsInitial P

theorem CategoryTheory.Limits.terminal.hom_ext_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] {P : C} {f : P ⟶ ⊤_ C} {g : P ⟶ ⊤_ C} : f = g ↔ True

theorem CategoryTheory.Limits.terminal.hom_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] {P : C} (f : P ⟶ ⊤_ C) (g : P ⟶ ⊤_ C) : f = g

theorem CategoryTheory.Limits.initial.hom_ext_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] {P : C} {f : ⊥_ C ⟶ P} {g : ⊥_ C ⟶ P} : f = g ↔ True

theorem CategoryTheory.Limits.initial.hom_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] {P : C} (f : ⊥_ C ⟶ P) (g : ⊥_ C ⟶ P) : f = g

@[simp]

theorem CategoryTheory.Limits.terminal.comp_from {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] {P : C} {Q : C} (f : P ⟶ Q) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.terminal.from Q) = CategoryTheory.Limits.terminal.from P

@[simp]

theorem CategoryTheory.Limits.initial.to_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] {P : C} {Q : C} (f : P ⟶ Q) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.initial.to P) f = CategoryTheory.Limits.initial.to Q

def CategoryTheory.Limits.initialIsoIsInitial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] {P : C} (t : CategoryTheory.Limits.IsInitial P) : ⊥_ C ≅ P

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

Equations

• CategoryTheory.Limits.initialIsoIsInitial t = CategoryTheory.Limits.initialIsInitial.uniqueUpToIso t

def CategoryTheory.Limits.terminalIsoIsTerminal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] {P : C} (t : CategoryTheory.Limits.IsTerminal P) : ⊤_ C ≅ P

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

Equations

• CategoryTheory.Limits.terminalIsoIsTerminal t = CategoryTheory.Limits.terminalIsTerminal.uniqueUpToIso t

instance CategoryTheory.Limits.terminal.isSplitMono_from {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Y : C} [CategoryTheory.Limits.HasTerminal C] (f : ⊤_ C ⟶ Y) : CategoryTheory.IsSplitMono f

Any morphism from a terminal object is split mono.

Equations

• ⋯ = ⋯

instance CategoryTheory.Limits.initial.isSplitEpi_to {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Y : C} [CategoryTheory.Limits.HasInitial C] (f : Y ⟶ ⊥_ C) : CategoryTheory.IsSplitEpi f

Any morphism to an initial object is split epi.

Equations

• ⋯ = ⋯

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

An initial object is terminal in the opposite category.

Equations

• CategoryTheory.Limits.terminalOpOfInitial t = { lift := fun (s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty Cᵒᵖ)) => (t.to (Opposite.unop s.pt)).op, fac := ⋯, uniq := ⋯ }

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

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

Equations

• CategoryTheory.Limits.terminalUnopOfInitial t = { lift := fun (s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)) => (t.to (Opposite.op s.pt)).unop, fac := ⋯, uniq := ⋯ }

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

A terminal object is initial in the opposite category.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• CategoryTheory.Limits.initialUnopOfTerminal t = { desc := fun (s : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.empty C)) => (t.from (Opposite.op s.pt)).unop, fac := ⋯, uniq := ⋯ }

instance CategoryTheory.Limits.hasInitial_op_of_hasTerminal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Limits.HasInitial Cᵒᵖ

Equations

• ⋯ = ⋯

instance CategoryTheory.Limits.hasTerminal_op_of_hasInitial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] : CategoryTheory.Limits.HasTerminal Cᵒᵖ

Equations

• ⋯ = ⋯

theorem CategoryTheory.Limits.hasTerminal_of_hasInitial_op {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial Cᵒᵖ] : CategoryTheory.Limits.HasTerminal C

theorem CategoryTheory.Limits.hasInitial_of_hasTerminal_op {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal Cᵒᵖ] : CategoryTheory.Limits.HasInitial C

instance CategoryTheory.Limits.instHasLimitObjFunctorConstTerminal {J : Type u_1} [CategoryTheory.Category.{u_3, u_1} J] {C : Type u_2} [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Limits.HasLimit ((CategoryTheory.Functor.const J).obj (⊤_ C))

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.Limits.limitConstTerminal_hom {J : Type u_1} [CategoryTheory.Category.{u_3, u_1} J] {C : Type u_2} [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Limits.limitConstTerminal.hom = CategoryTheory.Limits.terminal.from (CategoryTheory.Limits.limit ((CategoryTheory.Functor.const J).obj (⊤_ C)))

def CategoryTheory.Limits.limitConstTerminal {J : Type u_1} [CategoryTheory.Category.{u_3, u_1} J] {C : Type u_2} [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Limits.limit ((CategoryTheory.Functor.const J).obj (⊤_ C)) ≅ ⊤_ C

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.limitConstTerminal_inv_π_assoc {J : Type u_1} [CategoryTheory.Category.{u_3, u_1} J] {C : Type u_2} [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasTerminal C] {j : J} {Z : C} (h : ((CategoryTheory.Functor.const J).obj (⊤_ C)).obj j ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.limitConstTerminal.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.const J).obj (⊤_ C)) j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.terminal.from (⊤_ C)) h

@[simp]

theorem CategoryTheory.Limits.limitConstTerminal_inv_π {J : Type u_1} [CategoryTheory.Category.{u_3, u_1} J] {C : Type u_2} [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasTerminal C] {j : J} : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.limitConstTerminal.inv (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.const J).obj (⊤_ C)) j) = CategoryTheory.Limits.terminal.from (⊤_ C)

instance CategoryTheory.Limits.instHasColimitObjFunctorConstInitial {J : Type u_1} [CategoryTheory.Category.{u_3, u_1} J] {C : Type u_2} [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasInitial C] : CategoryTheory.Limits.HasColimit ((CategoryTheory.Functor.const J).obj (⊥_ C))

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.Limits.colimitConstInitial_inv {J : Type u_1} [CategoryTheory.Category.{u_3, u_1} J] {C : Type u_2} [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasInitial C] : CategoryTheory.Limits.colimitConstInitial.inv = CategoryTheory.Limits.initial.to (CategoryTheory.Limits.colimit ((CategoryTheory.Functor.const J).obj (⊥_ C)))

def CategoryTheory.Limits.colimitConstInitial {J : Type u_1} [CategoryTheory.Category.{u_3, u_1} J] {C : Type u_2} [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasInitial C] : CategoryTheory.Limits.colimit ((CategoryTheory.Functor.const J).obj (⊥_ C)) ≅ ⊥_ C

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.ι_colimitConstInitial_hom_assoc {J : Type u_1} [CategoryTheory.Category.{u_3, u_1} J] {C : Type u_2} [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasInitial C] {j : J} {Z : C} (h : ⊥_ C ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.const J).obj (⊥_ C)) j) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.colimitConstInitial.hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.initial.to (⊥_ C)) h

@[simp]

theorem CategoryTheory.Limits.ι_colimitConstInitial_hom {J : Type u_1} [CategoryTheory.Category.{u_3, u_1} J] {C : Type u_2} [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasInitial C] {j : J} : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.const J).obj (⊥_ C)) j) CategoryTheory.Limits.colimitConstInitial.hom = CategoryTheory.Limits.initial.to (⊥_ C)

class CategoryTheory.Limits.InitialMonoClass (C : Type u₁) [CategoryTheory.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 : CategoryTheory.Limits.IsInitial I), CategoryTheory.Mono (hI.to X)

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

theorem CategoryTheory.Limits.InitialMonoClass.isInitial_mono_from {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} [self : CategoryTheory.Limits.InitialMonoClass C] {I : C} (X : C) (hI : CategoryTheory.Limits.IsInitial I), CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.InitialMonoClass C] {I : C} {X : C} (hI : CategoryTheory.Limits.IsInitial I) (f : I ⟶ X) : CategoryTheory.Mono f

@[instance 100]

instance CategoryTheory.Limits.initial.mono_from {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.InitialMonoClass C] (X : C) (f : ⊥_ C ⟶ X) : CategoryTheory.Mono f

Equations

• ⋯ = ⋯

theorem CategoryTheory.Limits.InitialMonoClass.of_isInitial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I : C} (hI : CategoryTheory.Limits.IsInitial I) (h : ∀ (X : C), CategoryTheory.Mono (hI.to X)) : CategoryTheory.Limits.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_initial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] (h : ∀ (X : C), CategoryTheory.Mono (CategoryTheory.Limits.initial.to X)) : CategoryTheory.Limits.InitialMonoClass C

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

theorem CategoryTheory.Limits.InitialMonoClass.of_isTerminal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I : C} {T : C} (hI : CategoryTheory.Limits.IsInitial I) (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.Mono (hI.to T) → CategoryTheory.Limits.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.

theorem CategoryTheory.Limits.InitialMonoClass.of_terminal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasTerminal C] (h : CategoryTheory.Mono (CategoryTheory.Limits.initial.to (⊤_ C))) : CategoryTheory.Limits.InitialMonoClass C

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.

def CategoryTheory.Limits.terminalComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasTerminal D] : G.obj (⊤_ C) ⟶ ⊤_ D

The comparison morphism from the image of a terminal object to the terminal object in the target category. This is an isomorphism iff G preserves terminal objects, see CategoryTheory.Limits.PreservesTerminal.ofIsoComparison.

Equations

• CategoryTheory.Limits.terminalComparison G = CategoryTheory.Limits.terminal.from (G.obj (⊤_ C))

def CategoryTheory.Limits.initialComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasInitial D] : ⊥_ D ⟶ G.obj (⊥_ C)

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

Equations

• CategoryTheory.Limits.initialComparison G = CategoryTheory.Limits.initial.to (G.obj (⊥_ C))

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.coneOfDiagramInitial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {X : J} (tX : CategoryTheory.Limits.IsInitial X) (F : CategoryTheory.Functor J C) : CategoryTheory.Limits.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.

Equations

• CategoryTheory.Limits.coneOfDiagramInitial tX F = { pt := F.obj X, π := { app := fun (j : J) => F.map (tX.to j), naturality := ⋯ } }

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

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

Equations

• CategoryTheory.Limits.limitOfDiagramInitial tX F = { lift := fun (s : CategoryTheory.Limits.Cone F) => s.π.app X, fac := ⋯, uniq := ⋯ }

instance CategoryTheory.Limits.hasLimit_of_domain_hasInitial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.HasInitial J] {F : CategoryTheory.Functor J C} : CategoryTheory.Limits.HasLimit F

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev CategoryTheory.Limits.limitOfInitial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasInitial J] : CategoryTheory.Limits.limit F ≅ F.obj (⊥_ J)

For a functor F : J ⥤ C, if J has an initial object then the image of it is isomorphic to the limit of F.

Equations

• CategoryTheory.Limits.limitOfInitial F = (CategoryTheory.Limits.limit.isLimit F).conePointUniqueUpToIso (CategoryTheory.Limits.limitOfDiagramInitial CategoryTheory.Limits.initialIsInitial F)

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.coneOfDiagramTerminal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {X : J} (hX : CategoryTheory.Limits.IsTerminal X) (F : CategoryTheory.Functor J C) [∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)] : CategoryTheory.Limits.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.

Equations

• CategoryTheory.Limits.coneOfDiagramTerminal hX F = { pt := F.obj X, π := { app := fun (i : J) => CategoryTheory.inv (F.map (hX.from i)), naturality := ⋯ } }

def CategoryTheory.Limits.limitOfDiagramTerminal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {X : J} (hX : CategoryTheory.Limits.IsTerminal X) (F : CategoryTheory.Functor J C) [∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.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.

Equations

• CategoryTheory.Limits.limitOfDiagramTerminal hX F = { lift := fun (S : CategoryTheory.Limits.Cone F) => S.π.app X, fac := ⋯, uniq := ⋯ }

instance CategoryTheory.Limits.hasLimit_of_domain_hasTerminal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.HasTerminal J] {F : CategoryTheory.Functor J C} [∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)] : CategoryTheory.Limits.HasLimit F

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev CategoryTheory.Limits.limitOfTerminal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasTerminal J] [∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)] : CategoryTheory.Limits.limit F ≅ F.obj (⊤_ J)

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.coconeOfDiagramTerminal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {X : J} (tX : CategoryTheory.Limits.IsTerminal X) (F : CategoryTheory.Functor J C) : CategoryTheory.Limits.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.

Equations

• CategoryTheory.Limits.coconeOfDiagramTerminal tX F = { pt := F.obj X, ι := { app := fun (j : J) => F.map (tX.from j), naturality := ⋯ } }

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

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

Equations

• CategoryTheory.Limits.colimitOfDiagramTerminal tX F = { desc := fun (s : CategoryTheory.Limits.Cocone F) => s.ι.app X, fac := ⋯, uniq := ⋯ }

instance CategoryTheory.Limits.hasColimit_of_domain_hasTerminal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.HasTerminal J] {F : CategoryTheory.Functor J C} : CategoryTheory.Limits.HasColimit F

Equations

• ⋯ = ⋯

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

@[reducible, inline]

abbrev CategoryTheory.Limits.colimitOfTerminal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasTerminal J] : CategoryTheory.Limits.colimit F ≅ F.obj (⊤_ J)

For a functor F : J ⥤ C, if J has a terminal object then the image of it is isomorphic to the colimit of F.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.coconeOfDiagramInitial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {X : J} (hX : CategoryTheory.Limits.IsInitial X) (F : CategoryTheory.Functor J C) [∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)] : CategoryTheory.Limits.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.

Equations

• CategoryTheory.Limits.coconeOfDiagramInitial hX F = { pt := F.obj X, ι := { app := fun (i : J) => CategoryTheory.inv (F.map (hX.to i)), naturality := ⋯ } }

def CategoryTheory.Limits.colimitOfDiagramInitial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {X : J} (hX : CategoryTheory.Limits.IsInitial X) (F : CategoryTheory.Functor J C) [∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.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.

Equations

• CategoryTheory.Limits.colimitOfDiagramInitial hX F = { desc := fun (S : CategoryTheory.Limits.Cocone F) => S.ι.app X, fac := ⋯, uniq := ⋯ }

instance CategoryTheory.Limits.hasColimit_of_domain_hasInitial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.HasInitial J] {F : CategoryTheory.Functor J C} [∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)] : CategoryTheory.Limits.HasColimit F

Equations

• ⋯ = ⋯

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

@[reducible, inline]

abbrev CategoryTheory.Limits.colimitOfInitial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasInitial J] [∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)] : CategoryTheory.Limits.colimit F ≅ F.obj (⊥_ J)

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

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.isIso_π_of_isInitial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {j : J} (I : CategoryTheory.Limits.IsInitial j) (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasLimit F] : CategoryTheory.IsIso (CategoryTheory.Limits.limit.π F j)

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

instance CategoryTheory.Limits.isIso_π_initial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.HasInitial J] (F : CategoryTheory.Functor J C) : CategoryTheory.IsIso (CategoryTheory.Limits.limit.π F (⊥_ J))

Equations

• ⋯ = ⋯

theorem CategoryTheory.Limits.isIso_π_of_isTerminal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {j : J} (I : CategoryTheory.Limits.IsTerminal j) (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasLimit F] [∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)] : CategoryTheory.IsIso (CategoryTheory.Limits.limit.π F j)

instance CategoryTheory.Limits.isIso_π_terminal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.HasTerminal J] (F : CategoryTheory.Functor J C) [∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)] : CategoryTheory.IsIso (CategoryTheory.Limits.limit.π F (⊤_ J))

Equations

• ⋯ = ⋯

theorem CategoryTheory.Limits.isIso_ι_of_isTerminal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {j : J} (I : CategoryTheory.Limits.IsTerminal j) (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasColimit F] : CategoryTheory.IsIso (CategoryTheory.Limits.colimit.ι F j)

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

instance CategoryTheory.Limits.isIso_ι_terminal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.HasTerminal J] (F : CategoryTheory.Functor J C) : CategoryTheory.IsIso (CategoryTheory.Limits.colimit.ι F (⊤_ J))

Equations

• ⋯ = ⋯

theorem CategoryTheory.Limits.isIso_ι_of_isInitial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {j : J} (I : CategoryTheory.Limits.IsInitial j) (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasColimit F] [∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)] : CategoryTheory.IsIso (CategoryTheory.Limits.colimit.ι F j)

instance CategoryTheory.Limits.isIso_ι_initial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.HasInitial J] (F : CategoryTheory.Functor J C) [∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)] : CategoryTheory.IsIso (CategoryTheory.Limits.colimit.ι F (⊥_ J))

Equations

• ⋯ = ⋯

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

Any morphism between terminal objects is an isomorphism.

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

Any morphism between initial objects is an isomorphism.