Initial and terminal objects in a category.

References

• Stacks: Initial and final objects

@[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

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

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

theorem CategoryTheory.Limits.initial.hom_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] {P : C} (f 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 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 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

• ⋯ = ⋯

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

• ⋯ = ⋯

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_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)))

@[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)

@[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

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

• ⋯ = ⋯

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_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)))

@[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)

@[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

@[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_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_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))

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)

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.

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

• ⋯ = ⋯

@[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.

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

• ⋯ = ⋯

@[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

• ⋯ = ⋯