Strict initial objects #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 #
- out : ∀ {I A : C} (f : A ⟶ I), category_theory.limits.is_initial I → category_theory.is_iso f
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.
If I is initial, then X ⨯ I is isomorphic to it.
If I is initial, then I ⨯ X is isomorphic to it.
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).
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).
If C has an initial object such that every morphism to it is an isomorphism, then C
has strict initial objects.
- out : ∀ {I A : C} (f : I ⟶ A), category_theory.limits.is_terminal I → category_theory.is_iso f
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 of this typeclass
If all but one object in a diagram is strict terminal, the the limit is isomorphic to the
said object via limit.π.
If C has an object such that every morphism from it is an isomorphism, then C
has strict terminal objects.