# 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

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),
Instances
theorem CategoryTheory.Limits.HasStrictInitialObjects.out {C : Type u} {I : C} {A : C} (f : A I) :
theorem CategoryTheory.Limits.IsInitial.isIso_to {C : Type u} {I : C} (hI : ) {A : C} (f : A I) :
theorem CategoryTheory.Limits.IsInitial.strict_hom_ext {C : Type u} {I : C} (hI : ) {A : C} (f : A I) (g : A I) :
f = g
theorem CategoryTheory.Limits.IsInitial.subsingleton_to {C : Type u} {I : C} (hI : ) {A : C} :
@[instance 100]
Equations
• =
@[simp]
theorem CategoryTheory.Limits.mulIsInitial_hom {C : Type u} {I : C} (X : C) (hI : ) :
.hom = CategoryTheory.Limits.prod.snd
noncomputable def CategoryTheory.Limits.mulIsInitial {C : Type u} {I : C} (X : C) (hI : ) :
X I I

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.mulIsInitial_inv {C : Type u} {I : C} (X : C) (hI : ) :
.inv = hI.to (X I)
@[simp]
theorem CategoryTheory.Limits.isInitialMul_hom {C : Type u} {I : C} (X : C) (hI : ) :
.hom = CategoryTheory.Limits.prod.fst
noncomputable def CategoryTheory.Limits.isInitialMul {C : Type u} {I : C} (X : C) (hI : ) :
I X I

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.isInitialMul_inv {C : Type u} {I : C} (X : C) (hI : ) :
.inv = hI.to (I X)
instance CategoryTheory.Limits.initial_isIso_to {C : Type u} {A : C} (f : A ⊥_ C) :
Equations
• =
theorem CategoryTheory.Limits.initial.strict_hom_ext {C : Type u} {A : C} (f : A ⊥_ C) (g : A ⊥_ C) :
f = g
@[simp]
theorem CategoryTheory.Limits.mulInitial_hom {C : Type u} (X : C) :
.hom = CategoryTheory.Limits.prod.snd
noncomputable def CategoryTheory.Limits.mulInitial {C : Type u} (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 X × Empty ≃ Empty for types (or n * 0 = 0).

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.mulInitial_inv {C : Type u} (X : C) :
@[simp]
theorem CategoryTheory.Limits.initialMul_hom {C : Type u} (X : C) :
.hom = CategoryTheory.Limits.prod.fst
noncomputable def CategoryTheory.Limits.initialMul {C : Type u} (X : C) :
(⊥_ 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
Instances For

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

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),
Instances
theorem CategoryTheory.Limits.HasStrictTerminalObjects.out {C : Type u} {I : C} {A : C} (f : I A) :
theorem CategoryTheory.Limits.IsTerminal.isIso_from {C : Type u} {I : C} (hI : ) {A : C} (f : I A) :
theorem CategoryTheory.Limits.IsTerminal.strict_hom_ext {C : Type u} {I : C} (hI : ) {A : C} (f : I A) (g : I A) :
f = g
theorem CategoryTheory.Limits.IsTerminal.subsingleton_to {C : Type u} {I : C} (hI : ) {A : C} :
theorem CategoryTheory.Limits.limit_π_isIso_of_is_strict_terminal {C : Type u} {J : Type v} (F : ) (i : J) (H : (j : J) → j iCategoryTheory.Limits.IsTerminal (F.obj j)) [Subsingleton (i 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} {A : C} (f : ⊤_ C A) :
Equations
• =
theorem CategoryTheory.Limits.terminal.strict_hom_ext {C : Type u} {A : C} (f : ⊤_ C A) (g : ⊤_ C A) :
f = g
theorem CategoryTheory.Limits.hasStrictTerminalObjects_of_terminal_is_strict {C : Type u} (I : C) (h : ∀ (A : C) (f : I A), ) :

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