# 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} (T : category_theory.monad 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
@[protected, instance]
Equations
@[protected, instance]

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

Equations
@[simp]
@[simp]
theorem category_theory.kleisli.adjunction.to_kleisli_map {C : Type u} (T : category_theory.monad C) (X Y : C) (f : X Y) :
= f T.η.app Y

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

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

Equations

The composition of the adjunction gives the original functor.

Equations