Documentation

Mathlib.CategoryTheory.Monad.Kleisli

Kleisli category on a (co)monad #

This file defines the Kleisli category on a monad (T, η_ T, μ_ T) as well as the co-Kleisli category on a comonad (U, ε_ U, δ_ U). It also defines the Kleisli adjunction which gives rise to the monad (T, η_ T, μ_ T) as well as the co-Kleisli adjunction which gives rise to the comonad (U, ε_ U, δ_ U).

References #

The objects for the Kleisli category of the monad T : Monad C, which are the same thing as objects of the base category C.

Equations
Instances For

    The left adjoint of the adjunction which induces the monad (T, η_ T, μ_ T).

    Equations
    Instances For

      The right adjoint of the adjunction which induces the monad (T, η_ T, μ_ T).

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

        The Kleisli adjunction which gives rise to the monad (T, η_ T, μ_ T). cf Lemma 5.2.11 of Riehl.

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

          The composition of the adjunction gives the original functor.

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

            The objects for the co-Kleisli category of the comonad U : Comonad C, which are the same thing as objects of the base category C.

            Equations
            Instances For

              The right adjoint of the adjunction which induces the comonad (U, ε_ U, δ_ U).

              Equations
              Instances For

                The left adjoint of the adjunction which induces the comonad (U, ε_ U, δ_ U).

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

                  The co-Kleisli adjunction which gives rise to the monad (U, ε_ U, δ_ U).

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

                    The composition of the adjunction gives the original functor.

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