# mathlibdocumentation

# 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

• [Riehl, Category theory in context, Definition 5.2.9][riehl2017]
@[nolint]
def category_theory.kleisli {C : Type u} (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]
def category_theory.kleisli.inhabited {C : Type u} (T : C C) [inhabited C] :

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

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

Equations
@[simp]
theorem category_theory.kleisli.adjunction.to_kleisli_obj {C : Type u} (T : C C) (X : C) :

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

def category_theory.kleisli.adjunction.to_kleisli {C : Type u} (T : C C)  :

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

Equations
def category_theory.kleisli.adjunction.from_kleisli {C : Type u} (T : C C)  :

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

Equations
@[simp]
theorem category_theory.kleisli.adjunction.from_kleisli_map {C : Type u} (T : C C) (X Y : category_theory.kleisli T) (f : X Y) :
= T.map f (μ_ T).app Y

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

Equations

The composition of the adjunction gives the original functor.

Equations