# 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 #

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

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]
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
@[nolint]
def category_theory.cokleisli {C : Type u} (U : category_theory.comonad C) :
Type u

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]
Equations
@[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
@[simp]
theorem category_theory.cokleisli.adjunction.to_cokleisli_map {C : Type u} (U : category_theory.comonad C) (X Y : C) (f : X Y) :
= U.ε.app X f

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

Equations

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

Equations

The composition of the adjunction gives the original functor.

Equations