mathlib documentation

category_theory.monad.kleisli

Kleisli category on a (co)monad #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

source
@[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 monad T : monad C, which are the same thing as objects of the base category C.

Equations
Instances for category_theory.kleisli
source
@[protected, instance]
def category_theory.kleisli.inhabited {C : Type u} [category_theory.category C] [inhabited C] (T : category_theory.monad C) :
inhabited (category_theory.kleisli T)
Equations
source
@[protected, instance]
def category_theory.kleisli.kleisli.category {C : Type u} [category_theory.category C] (T : category_theory.monad C) :
category_theory.category (category_theory.kleisli T)

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

Equations
source
@[simp]
theorem category_theory.kleisli.adjunction.to_kleisli_obj {C : Type u} [category_theory.category C] (T : category_theory.monad C) (X : C) :
(category_theory.kleisli.adjunction.to_kleisli T).obj X = X
source
@[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) :
(category_theory.kleisli.adjunction.to_kleisli T).map f = f ≫ T.η.app Y
source
def category_theory.kleisli.adjunction.to_kleisli {C : Type u} [category_theory.category C] (T : category_theory.monad C) :
C ⥤ category_theory.kleisli T

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

Equations
source
def category_theory.kleisli.adjunction.from_kleisli {C : Type u} [category_theory.category C] (T : category_theory.monad C) :
category_theory.kleisli T ⥤ C

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

Equations
source
@[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) :
(category_theory.kleisli.adjunction.from_kleisli T).obj X = T.to_functor.obj X
source
@[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
source
def category_theory.kleisli.adjunction.adj {C : Type u} [category_theory.category C] (T : category_theory.monad C) :
category_theory.kleisli.adjunction.to_kleisli T ⊣ category_theory.kleisli.adjunction.from_kleisli T

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

Equations
source
def category_theory.kleisli.adjunction.to_kleisli_comp_from_kleisli_iso_self {C : Type u} [category_theory.category C] (T : category_theory.monad C) :
category_theory.kleisli.adjunction.to_kleisli T ⋙ category_theory.kleisli.adjunction.from_kleisli T ≅ ↑T

The composition of the adjunction gives the original functor.

Equations
source
@[nolint]
def category_theory.cokleisli {C : Type u} [category_theory.category C] (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
source
@[protected, instance]
def category_theory.cokleisli.inhabited {C : Type u} [category_theory.category C] [inhabited C] (U : category_theory.comonad C) :
inhabited (category_theory.cokleisli U)
Equations
source
@[protected, instance]
def category_theory.cokleisli.cokleisli.category {C : Type u} [category_theory.category C] (U : category_theory.comonad C) :
category_theory.category (category_theory.cokleisli U)

The co-Kleisli category on a comonad U.

Equations
source
def category_theory.cokleisli.adjunction.to_cokleisli {C : Type u} [category_theory.category C] (U : category_theory.comonad C) :
C ⥤ category_theory.cokleisli U

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

Equations
source
@[simp]
theorem category_theory.cokleisli.adjunction.to_cokleisli_map {C : Type u} [category_theory.category C] (U : category_theory.comonad C) (X Y : C) (f : X ⟶ Y) :
(category_theory.cokleisli.adjunction.to_cokleisli U).map f = U.ε.app X ≫ f
source
@[simp]
theorem category_theory.cokleisli.adjunction.to_cokleisli_obj {C : Type u} [category_theory.category C] (U : category_theory.comonad C) (X : C) :
(category_theory.cokleisli.adjunction.to_cokleisli U).obj X = X
source
@[simp]
theorem category_theory.cokleisli.adjunction.from_cokleisli_obj {C : Type u} [category_theory.category C] (U : category_theory.comonad C) (X : category_theory.cokleisli U) :
(category_theory.cokleisli.adjunction.from_cokleisli U).obj X = U.to_functor.obj X
source
def category_theory.cokleisli.adjunction.from_cokleisli {C : Type u} [category_theory.category C] (U : category_theory.comonad C) :
category_theory.cokleisli U ⥤ C

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

Equations
source
@[simp]
theorem category_theory.cokleisli.adjunction.from_cokleisli_map {C : Type u} [category_theory.category C] (U : category_theory.comonad C) (X Y : category_theory.cokleisli U) (f : X ⟶ Y) :
(category_theory.cokleisli.adjunction.from_cokleisli U).map f = U.δ.app X ≫ U.to_functor.map f
source
def category_theory.cokleisli.adjunction.adj {C : Type u} [category_theory.category C] (U : category_theory.comonad C) :
category_theory.cokleisli.adjunction.from_cokleisli U ⊣ category_theory.cokleisli.adjunction.to_cokleisli U

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

Equations
source
def category_theory.cokleisli.adjunction.to_cokleisli_comp_from_cokleisli_iso_self {C : Type u} [category_theory.category C] (U : category_theory.comonad C) :
category_theory.cokleisli.adjunction.to_cokleisli U ⋙ category_theory.cokleisli.adjunction.from_cokleisli U ≅ ↑U

The composition of the adjunction gives the original functor.

Equations