mathlib documentation

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 #

References #

@[class]

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.

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 × emptyempty for types (or n * 0 = 0).

Equations

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

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