mathlib documentation

category_theory.monad.kleisli

# Kleisli category on a monad

This file defines the Kleisli category on a monad (T, η_ T, μ_ T). It also defines the Kleisli adjunction which gives rise to the monad (T, η_ T, μ_ T).

References

@[nolint]
def category_theory.kleisli {C : Type u} [category_theory.category C] (T : C C) :
Type u

The objects for the Kleisli category of the functor (usually monad) T : C ⥤ C, which are the same thing as objects of the base category C.

Equations
@[instance]

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

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