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

def CategoryTheory.Kleisli {C : Type u} (_T : ) :

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
instance CategoryTheory.Kleisli.instInhabited {C : Type u} [] (T : ) :
Equations
• = { default := default }
instance CategoryTheory.Kleisli.category {C : Type u} (T : ) :

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

Equations
@[simp]
theorem CategoryTheory.Kleisli.Adjunction.toKleisli_map {C : Type u} (T : ) {X : C} {Y : C} (f : X Y) :
@[simp]
theorem CategoryTheory.Kleisli.Adjunction.toKleisli_obj {C : Type u} (T : ) (X : C) :
= X

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Kleisli.Adjunction.fromKleisli_map {C : Type u} (T : ) :
∀ {x Y : } (f : x Y), = CategoryTheory.CategoryStruct.comp (T.map f) (T.app Y)
@[simp]
theorem CategoryTheory.Kleisli.Adjunction.fromKleisli_obj {C : Type u} (T : ) (X : ) :
= T.obj X

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

Equations
• One or more equations did not get rendered due to their size.
Instances For

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

Equations
• One or more equations did not get rendered due to their size.
Instances For

The composition of the adjunction gives the original functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Cokleisli {C : Type u} (_U : ) :

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

Equations
Instances For
instance CategoryTheory.Cokleisli.instInhabited {C : Type u} [] (U : ) :
Equations
• = { default := default }
instance CategoryTheory.Cokleisli.category {C : Type u} (U : ) :

The co-Kleisli category on a comonad U.

Equations
@[simp]
theorem CategoryTheory.Cokleisli.Adjunction.toCokleisli_map {C : Type u} (U : ) {X : C} :
∀ {x : C} (f : X x), = CategoryTheory.CategoryStruct.comp (U.app X) f
@[simp]

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Cokleisli.Adjunction.fromCokleisli_obj {C : Type u} (U : ) (X : ) :
= U.obj X
@[simp]
theorem CategoryTheory.Cokleisli.Adjunction.fromCokleisli_map {C : Type u} (U : ) {X : } :
∀ {x : } (f : X x), = CategoryTheory.CategoryStruct.comp (U.app X) (U.map f)

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

Equations
• One or more equations did not get rendered due to their size.
Instances For

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

Equations
• One or more equations did not get rendered due to their size.
Instances For

The composition of the adjunction gives the original functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For