mathlib3 documentation

category_theory.monad.kleisli

Kleisli category on a (co)monad #

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

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 #

@[nolint]

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 category_theory.kleisli
@[protected, instance]

The Kleisli category on a monad T. cf Definition 5.2.9 in Riehl.

Equations

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

Equations

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

Equations
@[nolint]

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

Equations
Instances for category_theory.cokleisli
@[protected, instance]

The co-Kleisli category on a comonad U.

Equations

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

Equations

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

Equations