Documentation

Mathlib.CategoryTheory.Adjunction.Comma

Properties of comma categories relating to adjunctions #

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

Specifically, adjunctionOfStructuredArrowInitials gives the left adjoint assuming the appropriate initial objects exist, and mkInitialOfLeftAdjoint 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
  • One or more equations did not get rendered due to their size.
Instances For

    If each structured arrow category on G has an initial object, G is a right adjoint.

    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
    • One or more equations did not get rendered due to their size.
    Instances For

      If each costructured arrow category on G has a terminal object, G is a left adjoint.

      Given a left adjoint to G, we can construct an initial object in each structured arrow category on G.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Given a right adjoint to F, we can construct a terminal object in each costructured arrow category on F.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For