Documentation

Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

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 #

References #

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

    If X ⟶ Y with Y being a strict initial object, then X is also an initial object.

    Equations
    Instances For

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

      Equations
      Instances For

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

        Equations
        Instances For

          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
          Instances For

            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.

              Instances

                If X ⟶ Y with Y being a strict terminal object, then X is also an terminal object.

                Equations
                Instances For

                  If all but one object in a diagram is strict terminal, then 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.