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}
[category_theory.category C]
(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
@[instance]
def
category_theory.kleisli.inhabited
{C : Type u}
[category_theory.category C]
[inhabited C]
(T : category_theory.monad 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 : category_theory.monad C) :
The Kleisli category on a monad T.
cf Definition 5.2.9 in Riehl.
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 : category_theory.monad C)
(X : C) :
@[simp]
theorem
category_theory.kleisli.adjunction.to_kleisli_map
{C : Type u}
[category_theory.category C]
(T : category_theory.monad C)
(X Y : C)
(f : X ⟶ Y) :
def
category_theory.kleisli.adjunction.to_kleisli
{C : Type u}
[category_theory.category C]
(T : category_theory.monad C) :
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 : category_theory.monad C) :
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.to_functor.obj X, map := λ (X Y : category_theory.kleisli T) (f : X ⟶ Y), T.to_functor.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 : category_theory.monad C)
(X : category_theory.kleisli T) :
@[simp]
theorem
category_theory.kleisli.adjunction.from_kleisli_map
{C : Type u}
[category_theory.category C]
(T : category_theory.monad C)
(X Y : category_theory.kleisli T)
(f : X ⟶ Y) :
(category_theory.kleisli.adjunction.from_kleisli T).map f = T.to_functor.map f ≫ T.μ.app Y
def
category_theory.kleisli.adjunction.adj
{C : Type u}
[category_theory.category C]
(T : category_theory.monad C) :
The Kleisli adjunction which gives rise to the monad (T, η_ T, μ_ T).
cf Lemma 5.2.11 of Riehl.
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.to_functor.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 : category_theory.monad C) :
The composition of the adjunction gives the original functor.