Initial and terminal objects in a category.

References

• Stacks: Initial and final objects

@[reducible, inline]

abbrev CategoryTheory.Limits.HasTerminal (C : Type u₁) [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₁) [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

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

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

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

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.terminal (C : Type u₁) [Category.{v₁, u₁} C] [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]

noncomputable abbrev CategoryTheory.Limits.initial (C : Type u₁) [Category.{v₁, u₁} C] [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₁} [Category.{v₁, u₁} C] (X : C) [∀ (Y : C), Nonempty (Y ⟶ X)] [∀ (Y : C), Subsingleton (Y ⟶ X)] : 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₁} [Category.{v₁, u₁} C] {X : C} (h : IsTerminal X) : HasTerminal C

theorem CategoryTheory.Limits.hasInitial_of_unique {C : Type u₁} [Category.{v₁, u₁} C] (X : C) [∀ (Y : C), Nonempty (X ⟶ Y)] [∀ (Y : C), Subsingleton (X ⟶ Y)] : 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₁} [Category.{v₁, u₁} C] {X : C} (h : IsInitial X) : HasInitial C

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.terminal.from {C : Type u₁} [Category.{v₁, u₁} C] [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]

noncomputable abbrev CategoryTheory.Limits.initial.to {C : Type u₁} [Category.{v₁, u₁} C] [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)

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

A terminal object is terminal.

Equations

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

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

An initial object is initial.

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

noncomputable instance CategoryTheory.Limits.uniqueFromInitial {C : Type u₁} [Category.{v₁, u₁} C] [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 {C : Type u₁} [Category.{v₁, u₁} C] [HasTerminal C] {P : C} (f g : P ⟶ ⊤_ C) : f = g

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

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

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.terminal.comp_from_assoc {C : Type u₁} [Category.{v₁, u₁} C] [HasTerminal C] {P Q : C} (f : P ⟶ Q) {Z : C} (h : ⊤_ C ⟶ Z) : CategoryStruct.comp f (CategoryStruct.comp («from» Q) h) = CategoryStruct.comp («from» P) h

@[simp]

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

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

noncomputable def CategoryTheory.Limits.initialIsoIsInitial {C : Type u₁} [Category.{v₁, u₁} C] [HasInitial C] {P : C} (t : 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

@[simp]

theorem CategoryTheory.Limits.initialIsoIsInitial_hom {C : Type u₁} [Category.{v₁, u₁} C] [HasInitial C] {P : C} (t : IsInitial P) : (initialIsoIsInitial t).hom = initialIsInitial.to P

@[simp]

theorem CategoryTheory.Limits.initialIsoIsInitial_inv {C : Type u₁} [Category.{v₁, u₁} C] [HasInitial C] {P : C} (t : IsInitial P) : (initialIsoIsInitial t).inv = t.to (⊥_ C)

noncomputable def CategoryTheory.Limits.terminalIsoIsTerminal {C : Type u₁} [Category.{v₁, u₁} C] [HasTerminal C] {P : C} (t : 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

@[simp]

theorem CategoryTheory.Limits.terminalIsoIsTerminal_hom {C : Type u₁} [Category.{v₁, u₁} C] [HasTerminal C] {P : C} (t : IsTerminal P) : (terminalIsoIsTerminal t).hom = t.from (⊤_ C)

@[simp]

theorem CategoryTheory.Limits.terminalIsoIsTerminal_inv {C : Type u₁} [Category.{v₁, u₁} C] [HasTerminal C] {P : C} (t : IsTerminal P) : (terminalIsoIsTerminal t).inv = terminalIsTerminal.from P

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

Any morphism from a terminal object is split mono.

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

Any morphism to an initial object is split epi.

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

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

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

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

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

noncomputable def CategoryTheory.Limits.limitConstTerminal {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_2} [Category.{v_2, u_2} C] [HasTerminal C] : limit ((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_hom {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_2} [Category.{v_2, u_2} C] [HasTerminal C] : limitConstTerminal.hom = terminal.from (limit ((Functor.const J).obj (⊤_ C)))

@[simp]

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

@[simp]

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

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

noncomputable def CategoryTheory.Limits.colimitConstInitial {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_2} [Category.{v_2, u_2} C] [HasInitial C] : colimit ((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_inv {J : Type u_1} [Category.{v_1, u_1} J] {C : Type u_2} [Category.{v_2, u_2} C] [HasInitial C] : colimitConstInitial.inv = initial.to (colimit ((Functor.const J).obj (⊥_ C)))

@[simp]

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

@[simp]

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

@[instance 100]

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

theorem CategoryTheory.Limits.InitialMonoClass.of_initial {C : Type u₁} [Category.{v₁, u₁} C] [HasInitial C] (h : ∀ (X : C), Mono (initial.to X)) : 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_terminal {C : Type u₁} [Category.{v₁, u₁} C] [HasInitial C] [HasTerminal C] (h : Mono (initial.to (⊤_ C))) : 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.

noncomputable def CategoryTheory.Limits.terminalComparison {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) [HasTerminal C] [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))

noncomputable def CategoryTheory.Limits.initialComparison {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) [HasInitial C] [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))

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.limitOfInitial {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] (F : Functor J C) [HasInitial J] : 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)

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.limitOfTerminal {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] (F : Functor J C) [HasTerminal J] [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : 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.

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.colimitOfTerminal {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] (F : Functor J C) [HasTerminal J] : 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.

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.colimitOfInitial {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] (F : Functor J C) [HasInitial J] [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] : 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₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {j : J} (I : IsInitial j) (F : Functor J C) [HasLimit F] : IsIso (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₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] [HasInitial J] (F : Functor J C) : IsIso (limit.π F (⊥_ J))

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

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

theorem CategoryTheory.Limits.isIso_ι_of_isTerminal {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {j : J} (I : IsTerminal j) (F : Functor J C) [HasColimit F] : IsIso (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₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] [HasTerminal J] (F : Functor J C) : IsIso (colimit.ι F (⊤_ J))

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

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