Initial and terminal objects in a category. #

IsLimit { pt := Y, π := { app := fun (X : Discrete PEmpty.{1}) => id (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.

source

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

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 := ⋯ }

source

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

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

source

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

IsTerminal ⊤

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

Equations

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

source

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

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 := ⋯ }

source

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

IsTerminal X ≃ 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.

source

def CategoryTheory.Limits.isInitialEquivUnique {C : Type u₁} [Category.{v₁, u₁} C] (F : Functor (Discrete PEmpty.{1}) C) (X : C) :

IsColimit { pt := X, ι := { app := fun (X_1 : Discrete PEmpty.{1}) => id (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.

source

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

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 := ⋯ }

source

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

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

source

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

IsInitial ⊥

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

Equations

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

source

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

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 := ⋯ }

source

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

IsInitial X ≃ 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.

source

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

source

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

f = g

Any two morphisms to a terminal object are equal.

source

@[simp]

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

CategoryStruct.comp f (t.from Y) = t.from X

source

@[simp]

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

t.from X = CategoryStruct.id X

source

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

source

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

f = g

Any two morphisms from an initial object are equal.

source

@[simp]

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

CategoryStruct.comp (t.to Y) f = t.to Z

source

@[simp]

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

t.to X = CategoryStruct.id X

source

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

IsSplitMono f

Any morphism from a terminal object is split mono.

source

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

IsSplitEpi f

Any morphism to an initial object is split epi.

source

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

Mono f

Any morphism from a terminal object is mono.

source

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

Epi f

Any morphism to an initial object is epi.

source

def CategoryTheory.Limits.IsTerminal.uniqueUpToIso {C : Type u₁} [Category.{v₁, u₁} C] {T T' : C} (hT : IsTerminal T) (hT' : 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 := ⋯ }

source

@[simp]

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

(hT.uniqueUpToIso hT').hom = hT'.from T

source

@[simp]

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

(hT.uniqueUpToIso hT').inv = hT.from T'

source

def CategoryTheory.Limits.IsInitial.uniqueUpToIso {C : Type u₁} [Category.{v₁, u₁} C] {I I' : C} (hI : IsInitial I) (hI' : 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 := ⋯ }

source

@[simp]

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

(hI.uniqueUpToIso hI').inv = hI'.to I

source

@[simp]

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

(hI.uniqueUpToIso hI').hom = hI.to I'

source

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

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.

source

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

IsLimit c₁ ≃ 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.

source

noncomputable def CategoryTheory.Limits.isLimitEquivIsTerminalOfIsEmpty (C : Type u₁) [Category.{v₁, u₁} C] {J : Type u_1} [Category.{u_2, u_1} J] [IsEmpty J] {F : Functor J C} (c : Cone F) :

IsLimit c ≃ IsTerminal c.pt

If F is an empty diagram, then a cone over F is limiting iff the cone point is terminal.

Equations

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

source

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

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.

source

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

IsColimit c₁ ≃ 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.

source

noncomputable def CategoryTheory.Limits.isColimitEquivIsInitialOfIsEmpty (C : Type u₁) [Category.{v₁, u₁} C] {J : Type u_1} [Category.{u_2, u_1} J] [IsEmpty J] {F : Functor J C} (c : Cocone F) :

IsColimit c ≃ IsInitial c.pt

If F is an empty diagram, then a cocone over F is colimiting iff the cocone point is initial.

Equations

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

source

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

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 := ⋯ }

source

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

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 := ⋯ }

source

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

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.

source

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

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 := ⋯ }

source

class CategoryTheory.Limits.InitialMonoClass (C : Type u₁) [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 : IsInitial I) : Mono (hI.to X)
The map from the (any as stated) initial object to any other object is a monomorphism

Instances

source

theorem CategoryTheory.Limits.IsInitial.mono_from {C : Type u₁} [Category.{v₁, u₁} C] [InitialMonoClass C] {I X : C} (hI : IsInitial I) (f : I ⟶ X) :

Mono f

source

theorem CategoryTheory.Limits.InitialMonoClass.of_isInitial {C : Type u₁} [Category.{v₁, u₁} C] {I : C} (hI : IsInitial I) (h : ∀ (X : C), Mono (hI.to X)) :

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.

source

theorem CategoryTheory.Limits.InitialMonoClass.of_isTerminal {C : Type u₁} [Category.{v₁, u₁} C] {I T : C} (hI : IsInitial I) (hT : IsTerminal T) :

Mono (hI.to T) → 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.

source

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

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 := ⋯ } }

source

@[simp]

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

(coneOfDiagramInitial tX F).pt = F.obj X

source

@[simp]

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

(coneOfDiagramInitial tX F).π.app j = F.map (tX.to j)

source

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

IsLimit (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 := ⋯ }

source

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

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 (x : J) => CategoryTheory.inv (F.map (hX.from x)), naturality := ⋯ } }

source

@[simp]

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

(coneOfDiagramTerminal hX F).pt = F.obj X

source

@[simp]

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

(coneOfDiagramTerminal hX F).π.app x✝ = inv (F.map (hX.from x✝))

source

def CategoryTheory.Limits.limitOfDiagramTerminal {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {X : J} (hX : IsTerminal X) (F : Functor J C) [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] :

IsLimit (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 := ⋯ }

source

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

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 := ⋯ } }

source

@[simp]

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

(coconeOfDiagramTerminal tX F).ι.app j = F.map (tX.from j)

source

@[simp]

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

(coconeOfDiagramTerminal tX F).pt = F.obj X

source

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

IsColimit (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 := ⋯ }

source

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

IsIso (c.ι.app X)

source

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

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 (x : J) => CategoryTheory.inv (F.map (hX.to x)), naturality := ⋯ } }

source

@[simp]

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

(coconeOfDiagramInitial hX F).pt = F.obj X

source

@[simp]

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

(coconeOfDiagramInitial hX F).ι.app x✝ = inv (F.map (hX.to x✝))

source

def CategoryTheory.Limits.colimitOfDiagramInitial {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u} [Category.{v, u} J] {X : J} (hX : IsInitial X) (F : Functor J C) [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] :

IsColimit (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 := ⋯ }

source

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

IsIso (c.π.app X)

source

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

IsIso f

Any morphism between terminal objects is an isomorphism.

source

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

IsIso f

Any morphism between initial objects is an isomorphism.

Documentation

Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Initial and terminal objects in a category. #

References #