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 #
- 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.
Instances of this typeclass
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.