Documentation

Mathlib.CategoryTheory.Adjunction.Evaluation

Adjunctions involving evaluation #

We show that evaluation of functors have adjoints, given the existence of (co)products.

The left adjoint of evaluation.

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

    The adjunction showing that evaluation is a right adjoint.

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

      See also the file CategoryTheory.Limits.FunctorCategoryEpiMono for a similar result under a HasPullbacks assumption.

      The right adjoint of evaluation.

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

        The adjunction showing that evaluation is a left adjoint.

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

          See also the file CategoryTheory.Limits.FunctorCategoryEpiMono for a similar result under a HasPushouts assumption.