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, i.e. 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) [Category.{v, u} C] : Prop

We say C has strict initial objects if every initial object is strict, i.e. 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) : ∀ (a : IsInitial I), IsIso f

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

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

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

noncomputable def CategoryTheory.Limits.IsInitial.ofStrict {C : Type u} [Category.{v, u} C] [HasStrictInitialObjects C] {X Y : C} (f : X ⟶ Y) (hY : IsInitial Y) : 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} [Category.{v, u} C] [HasStrictInitialObjects C] : InitialMonoClass C

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

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

Equations

• CategoryTheory.Limits.mulIsInitial X hI = CategoryTheory.asIso CategoryTheory.Limits.prod.snd

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.Limits.isInitialMul X hI = CategoryTheory.asIso CategoryTheory.Limits.prod.fst

@[simp]

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

@[simp]

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

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

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

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

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

noncomputable def CategoryTheory.Limits.mulInitial {C : Type u} [Category.{v, u} C] [HasStrictInitialObjects C] [HasInitial C] (X : C) [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_hom {C : Type u} [Category.{v, u} C] [HasStrictInitialObjects C] [HasInitial C] (X : C) [HasBinaryProduct X (⊥_ C)] : (mulInitial X).hom = prod.snd

@[simp]

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

noncomputable def CategoryTheory.Limits.initialMul {C : Type u} [Category.{v, u} C] [HasStrictInitialObjects C] [HasInitial C] (X : C) [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_hom {C : Type u} [Category.{v, u} C] [HasStrictInitialObjects C] [HasInitial C] (X : C) [HasBinaryProduct (⊥_ C) X] : (initialMul X).hom = prod.fst

@[simp]

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

theorem CategoryTheory.Limits.hasStrictInitialObjects_of_initial_is_strict {C : Type u} [Category.{v, u} C] [HasInitial C] (h : ∀ (A : C) (f : A ⟶ ⊥_ C), IsIso f) : 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) [Category.{v, u} C] : Prop

We say C has strict terminal objects if every terminal object is strict, i.e. 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) : ∀ (a : IsTerminal I), IsIso f

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

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

noncomputable def CategoryTheory.Limits.IsTerminal.ofStrict {C : Type u} [Category.{v, u} C] [HasStrictTerminalObjects C] {X Y : C} (f : X ⟶ Y) (hY : IsTerminal X) : 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} [Category.{v, u} C] [HasStrictTerminalObjects C] {I : C} (hI : IsTerminal I) {A : C} : Subsingleton (I ⟶ A)

theorem CategoryTheory.Limits.limit_π_isIso_of_is_strict_terminal {C : Type u} [Category.{v, u} C] [HasStrictTerminalObjects C] {J : Type v} [SmallCategory J] (F : Functor J C) [HasLimit F] (i : J) (H : (j : J) → j ≠ i → IsTerminal (F.obj j)) [Subsingleton (i ⟶ i)] : IsIso (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} [Category.{v, u} C] [HasStrictTerminalObjects C] [HasTerminal C] {A : C} (f : ⊤_ C ⟶ A) : IsIso f

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

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

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

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

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