mathlib3 documentation

category_theory.limits.constructions.weakly_initial

Constructions related to weakly initial objects #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file gives constructions related to weakly initial objects, namely:

These are primarily useful to show the General Adjoint Functor Theorem.

If C has (small) products and a small weakly initial set of objects, then it has a weakly initial object.

If C has (small) wide equalizers and a weakly initial object, then it has an initial object.

The initial object is constructed as the wide equalizer of all endomorphisms on the given weakly initial object.