mathlib3 documentation

category_theory.adjunction.comma

Properties of comma categories relating to adjunctions #

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

This file shows that for a functor G : D ⥤ C the data of an initial object in each structured_arrow category on G is equivalent to a left adjoint to G, as well as the dual.

Specifically, adjunction_of_structured_arrow_initials gives the left adjoint assuming the appropriate initial objects exist, and mk_initial_of_left_adjoint constructs the initial objects provided a left adjoint.

The duals are also shown.

Implementation: If each structured arrow category on G has an initial object, an equivalence which is helpful for constructing a left adjoint to G.

Equations

If each structured arrow category on G has an initial object, construct a left adjoint to G. It is shown that it is a left adjoint in adjunction_of_structured_arrow_initials.

Equations

Implementation: If each costructured arrow category on G has a terminal object, an equivalence which is helpful for constructing a right adjoint to G.

Equations

If each costructured arrow category on G has a terminal object, construct a right adjoint to G. It is shown that it is a right adjoint in adjunction_of_structured_arrow_initials.

Equations