# 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]
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}
[category_theory.category C]
(T : C ⥤ C)
[inhabited C] :
Equations
- category_theory.kleisli.inhabited T = {default := default C _inst_2}
@[instance]
def
category_theory.kleisli.kleisli.category
{C : Type u}
[category_theory.category C]
(T : C ⥤ C)
[category_theory.monad T] :
The Kleisli category on a monad T.
cf Definition 5.2.9 in [Riehl][riehl2017].
Equations
- category_theory.kleisli.kleisli.category T = {to_category_struct := {to_has_hom := {hom := λ (X Y : C), X ⟶ T.obj Y}, id := λ (X : category_theory.kleisli T), (η_ T).app X, comp := λ (X Y Z : category_theory.kleisli T) (f : X ⟶ Y) (g : Y ⟶ Z), f ≫ T.map g ≫ (μ_ T).app Z}, id_comp' := _, comp_id' := _, assoc' := _}
@[simp]
theorem
category_theory.kleisli.adjunction.to_kleisli_obj
{C : Type u}
[category_theory.category C]
(T : C ⥤ C)
[category_theory.monad T]
(X : C) :
@[simp]
theorem
category_theory.kleisli.adjunction.to_kleisli_map
{C : Type u}
[category_theory.category C]
(T : C ⥤ C)
[category_theory.monad T]
(X Y : C)
(f : X ⟶ Y) :
def
category_theory.kleisli.adjunction.to_kleisli
{C : Type u}
[category_theory.category C]
(T : C ⥤ C)
[category_theory.monad T] :
The left adjoint of the adjunction which induces the monad (T, η_ T, μ_ T).
def
category_theory.kleisli.adjunction.from_kleisli
{C : Type u}
[category_theory.category C]
(T : C ⥤ C)
[category_theory.monad T] :
The right adjoint of the adjunction which induces the monad (T, η_ T, μ_ T).
Equations
- category_theory.kleisli.adjunction.from_kleisli T = {obj := λ (X : category_theory.kleisli T), T.obj X, map := λ (X Y : category_theory.kleisli T) (f : X ⟶ Y), T.map f ≫ (μ_ T).app Y, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.kleisli.adjunction.from_kleisli_obj
{C : Type u}
[category_theory.category C]
(T : C ⥤ C)
[category_theory.monad T]
(X : category_theory.kleisli T) :
@[simp]
theorem
category_theory.kleisli.adjunction.from_kleisli_map
{C : Type u}
[category_theory.category C]
(T : C ⥤ C)
[category_theory.monad T]
(X Y : category_theory.kleisli T)
(f : X ⟶ Y) :
def
category_theory.kleisli.adjunction.adj
{C : Type u}
[category_theory.category C]
(T : C ⥤ C)
[category_theory.monad T] :
The Kleisli adjunction which gives rise to the monad (T, η_ T, μ_ T).
cf Lemma 5.2.11 of [Riehl][riehl2017].
Equations
- category_theory.kleisli.adjunction.adj T = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : C) (Y : category_theory.kleisli T), equiv.refl (X ⟶ T.obj Y), hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}
def
category_theory.kleisli.adjunction.to_kleisli_comp_from_kleisli_iso_self
{C : Type u}
[category_theory.category C]
(T : C ⥤ C)
[category_theory.monad T] :
The composition of the adjunction gives the original functor.