# mathlibdocumentation

category_theory.limits.shapes.strict_initial

# 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 has_strict_initial_objects_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*, Top, Groupoid, simplicial types, posets.
• Construct the bottom element of the subobject lattice given strict initials.
• Show cartesian closed categories have strict initials

## References #

@[class]
structure category_theory.limits.has_strict_initial_objects (C : Type u)  :
Prop
• out : ∀ {I A : C} (f : A I),

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.

theorem category_theory.limits.is_initial.is_iso_to {C : Type u} {I : C} {A : C} (f : A I) :
theorem category_theory.limits.is_initial.strict_hom_ext {C : Type u} {I : C} {A : C} (f g : A I) :
f = g
theorem category_theory.limits.is_initial.subsingleton_to {C : Type u} {I : C} {A : C} :
@[protected, instance]
noncomputable def category_theory.limits.mul_is_initial {C : Type u} {I : C} (X : C)  :
X I I

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

Equations
@[simp]
theorem category_theory.limits.mul_is_initial_hom {C : Type u} {I : C} (X : C)  :
@[simp]
theorem category_theory.limits.mul_is_initial_inv {C : Type u} {I : C} (X : C)  :
= hI.to (X I)
@[simp]
theorem category_theory.limits.is_initial_mul_hom {C : Type u} {I : C} (X : C)  :
noncomputable def category_theory.limits.is_initial_mul {C : Type u} {I : C} (X : C)  :
I X I

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

Equations
@[simp]
theorem category_theory.limits.is_initial_mul_inv {C : Type u} {I : C} (X : C)  :
= hI.to (I X)
@[protected, instance]
def category_theory.limits.initial_is_iso_to {C : Type u} {A : C} (f : A ⊥_ C) :
@[ext]
theorem category_theory.limits.initial.hom_ext {C : Type u} {A : C} (f g : A ⊥_ C) :
f = g
@[simp]
noncomputable def category_theory.limits.mul_initial {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
@[simp]
noncomputable def category_theory.limits.initial_mul {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 empty × X ≃ empty for types (or 0 * n = 0).

Equations
@[simp]
@[simp]
theorem category_theory.limits.has_strict_initial_objects_of_initial_is_strict {C : Type u} (h : ∀ (A : C) (f : A ⊥_ C), ) :

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

@[class]
structure category_theory.limits.has_strict_terminal_objects (C : Type u)  :
Prop
• out : ∀ {I A : C} (f : I A),

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.

Instances
theorem category_theory.limits.is_terminal.is_iso_from {C : Type u} {I : C} {A : C} (f : I A) :
theorem category_theory.limits.is_terminal.strict_hom_ext {C : Type u} {I : C} {A : C} (f g : I A) :
f = g
theorem category_theory.limits.is_terminal.subsingleton_to {C : Type u} {I : C} {A : C} :
theorem category_theory.limits.limit_π_is_iso_of_is_strict_terminal {C : Type u} {J : Type v} (F : J C) (i : J) (H : Π (j : J), j i) [subsingleton (i i)] :

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

@[protected, instance]
def category_theory.limits.terminal_is_iso_from {C : Type u} {A : C} (f : ⊤_ C A) :
@[ext]
theorem category_theory.limits.terminal.hom_ext {C : Type u} {A : C} (f g : ⊤_ C A) :
f = g
theorem category_theory.limits.has_strict_terminal_objects_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.