Strict initial objects

This file sets up the basic theory of strict initial objects: initial objects where every morphism to it is an isomorphism. This generalises a property of the empty set in the category of sets: namely that the only function to the empty set is from itself.

We say C has strict initial objects if every initial object is strict, ie given any morphism f : A ⟶ I where I is initial, then f is an isomorphism. Strictly speaking, this says that any initial object must be strict, rather than that strict initial objects exist, which turns out to be a more useful notion to formalise.

If the binary product of X with a strict initial object exists, it is also initial.

To show a category C with an initial object has strict initial objects, the most convenient way is to show any morphism to the (chosen) initial object is an isomorphism and use hasStrictInitialObjects_of_initial_is_strict.

The dual notion (strict terminal objects) occurs much less frequently in practice so is ignored.

TODO

• Construct examples of this: Type*, TopCat, Groupoid, simplicial types, posets.
• Construct the bottom element of the subobject lattice given strict initials.
• Show cartesian closed categories have strict initials

References

• https://ncatlab.org/nlab/show/strict+initial+object

class CategoryTheory.Limits.HasStrictInitialObjects (C : Type u) [CategoryTheory.Category.{v, u} C] : Prop

We say C has strict initial objects if every initial object is strict, ie given any morphism f : A ⟶ I where I is initial, then f is an isomorphism.

Strictly speaking, this says that any initial object must be strict, rather than that strict initial objects exist.

• out : ∀ {I A : C} (f : A ⟶ I), CategoryTheory.Limits.IsInitial I → CategoryTheory.IsIso f

theorem CategoryTheory.Limits.HasStrictInitialObjects.out {C : Type u} [CategoryTheory.Category.{v, u} C] [self : CategoryTheory.Limits.HasStrictInitialObjects C] {I : C} {A : C} (f : A ⟶ I) : CategoryTheory.Limits.IsInitial I → CategoryTheory.IsIso f

theorem CategoryTheory.Limits.IsInitial.isIso_to {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] {I : C} (hI : CategoryTheory.Limits.IsInitial I) {A : C} (f : A ⟶ I) : CategoryTheory.IsIso f

theorem CategoryTheory.Limits.IsInitial.strict_hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] {I : C} (hI : CategoryTheory.Limits.IsInitial I) {A : C} (f : A ⟶ I) (g : A ⟶ I) : f = g

theorem CategoryTheory.Limits.IsInitial.subsingleton_to {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] {I : C} (hI : CategoryTheory.Limits.IsInitial I) {A : C} : Subsingleton (A ⟶ I)

noncomputable def CategoryTheory.Limits.IsInitial.ofStrict {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] {X : C} {Y : C} (f : X ⟶ Y) (hY : CategoryTheory.Limits.IsInitial Y) : CategoryTheory.Limits.IsInitial X

If X ⟶ Y with Y being a strict initial object, then X is also an initial object.

Equations

• CategoryTheory.Limits.IsInitial.ofStrict f hY = hY.ofIso (CategoryTheory.asIso f).symm

@[instance 100]

instance CategoryTheory.Limits.initial_mono_of_strict_initial_objects {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] : CategoryTheory.Limits.InitialMonoClass C

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.Limits.mulIsInitial_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] {I : C} (X : C) [CategoryTheory.Limits.HasBinaryProduct X I] (hI : CategoryTheory.Limits.IsInitial I) : (CategoryTheory.Limits.mulIsInitial X hI).hom = CategoryTheory.Limits.prod.snd

noncomputable def CategoryTheory.Limits.mulIsInitial {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] {I : C} (X : C) [CategoryTheory.Limits.HasBinaryProduct X I] (hI : CategoryTheory.Limits.IsInitial I) : X ⨯ I ≅ I

If I is initial, then X ⨯ I is isomorphic to it.

Equations

• CategoryTheory.Limits.mulIsInitial X hI = let_fun this := ⋯; CategoryTheory.asIso CategoryTheory.Limits.prod.snd

@[simp]

theorem CategoryTheory.Limits.mulIsInitial_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] {I : C} (X : C) [CategoryTheory.Limits.HasBinaryProduct X I] (hI : CategoryTheory.Limits.IsInitial I) : (CategoryTheory.Limits.mulIsInitial X hI).inv = hI.to (X ⨯ I)

@[simp]

theorem CategoryTheory.Limits.isInitialMul_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] {I : C} (X : C) [CategoryTheory.Limits.HasBinaryProduct I X] (hI : CategoryTheory.Limits.IsInitial I) : (CategoryTheory.Limits.isInitialMul X hI).hom = CategoryTheory.Limits.prod.fst

noncomputable def CategoryTheory.Limits.isInitialMul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] {I : C} (X : C) [CategoryTheory.Limits.HasBinaryProduct I X] (hI : CategoryTheory.Limits.IsInitial I) : I ⨯ X ≅ I

If I is initial, then I ⨯ X is isomorphic to it.

Equations

• CategoryTheory.Limits.isInitialMul X hI = let_fun this := ⋯; CategoryTheory.asIso CategoryTheory.Limits.prod.fst

@[simp]

theorem CategoryTheory.Limits.isInitialMul_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] {I : C} (X : C) [CategoryTheory.Limits.HasBinaryProduct I X] (hI : CategoryTheory.Limits.IsInitial I) : (CategoryTheory.Limits.isInitialMul X hI).inv = hI.to (I ⨯ X)

instance CategoryTheory.Limits.initial_isIso_to {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] [CategoryTheory.Limits.HasInitial C] {A : C} (f : A ⟶ ⊥_ C) : CategoryTheory.IsIso f

Equations

• ⋯ = ⋯

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

theorem CategoryTheory.Limits.initial.subsingleton_to {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] [CategoryTheory.Limits.HasInitial C] {A : C} : Subsingleton (A ⟶ ⊥_ C)

@[simp]

theorem CategoryTheory.Limits.mulInitial_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] [CategoryTheory.Limits.HasInitial C] (X : C) [CategoryTheory.Limits.HasBinaryProduct X (⊥_ C)] : (CategoryTheory.Limits.mulInitial X).hom = CategoryTheory.Limits.prod.snd

noncomputable def CategoryTheory.Limits.mulInitial {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] [CategoryTheory.Limits.HasInitial C] (X : C) [CategoryTheory.Limits.HasBinaryProduct X (⊥_ C)] : X ⨯ ⊥_ C ≅ ⊥_ C

The product of X with an initial object in a category with strict initial objects is itself initial. This is the generalisation of the fact that X × Empty ≃ Empty for types (or n * 0 = 0).

Equations

• CategoryTheory.Limits.mulInitial X = CategoryTheory.Limits.mulIsInitial X CategoryTheory.Limits.initialIsInitial

@[simp]

theorem CategoryTheory.Limits.mulInitial_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] [CategoryTheory.Limits.HasInitial C] (X : C) [CategoryTheory.Limits.HasBinaryProduct X (⊥_ C)] : (CategoryTheory.Limits.mulInitial X).inv = CategoryTheory.Limits.initial.to (X ⨯ ⊥_ C)

@[simp]

theorem CategoryTheory.Limits.initialMul_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] [CategoryTheory.Limits.HasInitial C] (X : C) [CategoryTheory.Limits.HasBinaryProduct (⊥_ C) X] : (CategoryTheory.Limits.initialMul X).hom = CategoryTheory.Limits.prod.fst

noncomputable def CategoryTheory.Limits.initialMul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] [CategoryTheory.Limits.HasInitial C] (X : C) [CategoryTheory.Limits.HasBinaryProduct (⊥_ C) X] : (⊥_ C) ⨯ X ≅ ⊥_ C

The product of X with an initial object in a category with strict initial objects is itself initial. This is the generalisation of the fact that Empty × X ≃ Empty for types (or 0 * n = 0).

Equations

• CategoryTheory.Limits.initialMul X = CategoryTheory.Limits.isInitialMul X CategoryTheory.Limits.initialIsInitial

@[simp]

theorem CategoryTheory.Limits.initialMul_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] [CategoryTheory.Limits.HasInitial C] (X : C) [CategoryTheory.Limits.HasBinaryProduct (⊥_ C) X] : (CategoryTheory.Limits.initialMul X).inv = CategoryTheory.Limits.initial.to ((⊥_ C) ⨯ X)

theorem CategoryTheory.Limits.hasStrictInitialObjects_of_initial_is_strict {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] (h : ∀ (A : C) (f : A ⟶ ⊥_ C), CategoryTheory.IsIso f) : CategoryTheory.Limits.HasStrictInitialObjects C

If C has an initial object such that every morphism to it is an isomorphism, then C has strict initial objects.

class CategoryTheory.Limits.HasStrictTerminalObjects (C : Type u) [CategoryTheory.Category.{v, u} C] : Prop

We say C has strict terminal objects if every terminal object is strict, ie given any morphism f : I ⟶ A where I is terminal, then f is an isomorphism.

Strictly speaking, this says that any terminal object must be strict, rather than that strict terminal objects exist.

• out : ∀ {I A : C} (f : I ⟶ A), CategoryTheory.Limits.IsTerminal I → CategoryTheory.IsIso f

theorem CategoryTheory.Limits.HasStrictTerminalObjects.out {C : Type u} [CategoryTheory.Category.{v, u} C] [self : CategoryTheory.Limits.HasStrictTerminalObjects C] {I : C} {A : C} (f : I ⟶ A) : CategoryTheory.Limits.IsTerminal I → CategoryTheory.IsIso f

theorem CategoryTheory.Limits.IsTerminal.isIso_from {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictTerminalObjects C] {I : C} (hI : CategoryTheory.Limits.IsTerminal I) {A : C} (f : I ⟶ A) : CategoryTheory.IsIso f

theorem CategoryTheory.Limits.IsTerminal.strict_hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictTerminalObjects C] {I : C} (hI : CategoryTheory.Limits.IsTerminal I) {A : C} (f : I ⟶ A) (g : I ⟶ A) : f = g

noncomputable def CategoryTheory.Limits.IsTerminal.ofStrict {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictTerminalObjects C] {X : C} {Y : C} (f : X ⟶ Y) (hY : CategoryTheory.Limits.IsTerminal X) : CategoryTheory.Limits.IsTerminal Y

If X ⟶ Y with Y being a strict terminal object, then X is also an terminal object.

Equations

• CategoryTheory.Limits.IsTerminal.ofStrict f hY = hY.ofIso (CategoryTheory.asIso f)

theorem CategoryTheory.Limits.IsTerminal.subsingleton_to {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictTerminalObjects C] {I : C} (hI : CategoryTheory.Limits.IsTerminal I) {A : C} : Subsingleton (I ⟶ A)

theorem CategoryTheory.Limits.limit_π_isIso_of_is_strict_terminal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictTerminalObjects C] {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasLimit F] (i : J) (H : (j : J) → j ≠ i → CategoryTheory.Limits.IsTerminal (F.obj j)) [Subsingleton (i ⟶ i)] : CategoryTheory.IsIso (CategoryTheory.Limits.limit.π F i)

If all but one object in a diagram is strict terminal, then the limit is isomorphic to the said object via limit.π.

instance CategoryTheory.Limits.terminal_isIso_from {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictTerminalObjects C] [CategoryTheory.Limits.HasTerminal C] {A : C} (f : ⊤_ C ⟶ A) : CategoryTheory.IsIso f

Equations

• ⋯ = ⋯

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

theorem CategoryTheory.Limits.terminal.subsingleton_to {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictTerminalObjects C] [CategoryTheory.Limits.HasTerminal C] {A : C} : Subsingleton (⊤_ C ⟶ A)

theorem CategoryTheory.Limits.hasStrictTerminalObjects_of_terminal_is_strict {C : Type u} [CategoryTheory.Category.{v, u} C] (I : C) (h : ∀ (A : C) (f : I ⟶ A), CategoryTheory.IsIso f) : CategoryTheory.Limits.HasStrictTerminalObjects C

If C has an object such that every morphism from it is an isomorphism, then C has strict terminal objects.