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

• [Riehl, Category theory in context, Definition 5.2.9][riehl2017]

def CategoryTheory.Kleisli {C : Type u} [CategoryTheory.Category.{v, u} C] (_T : CategoryTheory.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

• CategoryTheory.Kleisli _T = C

instance CategoryTheory.Kleisli.instInhabitedKleisli {C : Type u} [CategoryTheory.Category.{v, u} C] [Inhabited C] (T : CategoryTheory.Monad C) : Inhabited (CategoryTheory.Kleisli T)

Equations

• CategoryTheory.Kleisli.instInhabitedKleisli T = { default := default }

instance CategoryTheory.Kleisli.Kleisli.category {C : Type u} [CategoryTheory.Category.{v, u} C] (T : CategoryTheory.Monad C) : CategoryTheory.Category.{v, u} (CategoryTheory.Kleisli T)

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

Equations

• CategoryTheory.Kleisli.Kleisli.category T = CategoryTheory.Category.mk

@[simp]

theorem CategoryTheory.Kleisli.Adjunction.toKleisli_map {C : Type u} [CategoryTheory.Category.{v, u} C] (T : CategoryTheory.Monad C) {X : C} {Y : C} (f : X ⟶ Y) : (CategoryTheory.Kleisli.Adjunction.toKleisli T).toPrefunctor.map f = CategoryTheory.CategoryStruct.comp f ((CategoryTheory.Monad.η T).app Y)

@[simp]

theorem CategoryTheory.Kleisli.Adjunction.toKleisli_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (T : CategoryTheory.Monad C) (X : C) : (CategoryTheory.Kleisli.Adjunction.toKleisli T).toPrefunctor.obj X = X

def CategoryTheory.Kleisli.Adjunction.toKleisli {C : Type u} [CategoryTheory.Category.{v, u} C] (T : CategoryTheory.Monad C) : CategoryTheory.Functor C (CategoryTheory.Kleisli T)

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

Equations

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

@[simp]

theorem CategoryTheory.Kleisli.Adjunction.fromKleisli_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (T : CategoryTheory.Monad C) (X : CategoryTheory.Kleisli T) : (CategoryTheory.Kleisli.Adjunction.fromKleisli T).toPrefunctor.obj X = T.toPrefunctor.obj X

@[simp]

theorem CategoryTheory.Kleisli.Adjunction.fromKleisli_map {C : Type u} [CategoryTheory.Category.{v, u} C] (T : CategoryTheory.Monad C) : ∀ {x Y : CategoryTheory.Kleisli T} (f : x ⟶ Y), (CategoryTheory.Kleisli.Adjunction.fromKleisli T).toPrefunctor.map f = CategoryTheory.CategoryStruct.comp (T.toPrefunctor.map f) ((CategoryTheory.Monad.μ T).app Y)

def CategoryTheory.Kleisli.Adjunction.fromKleisli {C : Type u} [CategoryTheory.Category.{v, u} C] (T : CategoryTheory.Monad C) : CategoryTheory.Functor (CategoryTheory.Kleisli T) C

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.

def CategoryTheory.Kleisli.Adjunction.adj {C : Type u} [CategoryTheory.Category.{v, u} C] (T : CategoryTheory.Monad C) : CategoryTheory.Kleisli.Adjunction.toKleisli T ⊣ CategoryTheory.Kleisli.Adjunction.fromKleisli T

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

Equations

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

def CategoryTheory.Kleisli.Adjunction.toKleisliCompFromKleisliIsoSelf {C : Type u} [CategoryTheory.Category.{v, u} C] (T : CategoryTheory.Monad C) : CategoryTheory.Functor.comp (CategoryTheory.Kleisli.Adjunction.toKleisli T) (CategoryTheory.Kleisli.Adjunction.fromKleisli T) ≅ T.toFunctor

The composition of the adjunction gives the original functor.

Equations

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

def CategoryTheory.Cokleisli {C : Type u} [CategoryTheory.Category.{v, u} C] (_U : CategoryTheory.Comonad C) : Type 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

• CategoryTheory.Cokleisli _U = C

instance CategoryTheory.Cokleisli.instInhabitedCokleisli {C : Type u} [CategoryTheory.Category.{v, u} C] [Inhabited C] (U : CategoryTheory.Comonad C) : Inhabited (CategoryTheory.Cokleisli U)

Equations

• CategoryTheory.Cokleisli.instInhabitedCokleisli U = { default := default }

instance CategoryTheory.Cokleisli.Cokleisli.category {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Comonad C) : CategoryTheory.Category.{v, u} (CategoryTheory.Cokleisli U)

The co-Kleisli category on a comonad U.

Equations

• CategoryTheory.Cokleisli.Cokleisli.category U = CategoryTheory.Category.mk

@[simp]

theorem CategoryTheory.Cokleisli.Adjunction.toCokleisli_map {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Comonad C) {X : C} : ∀ {x : C} (f : X ⟶ x), (CategoryTheory.Cokleisli.Adjunction.toCokleisli U).toPrefunctor.map f = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Comonad.ε U).app X) f

@[simp]

theorem CategoryTheory.Cokleisli.Adjunction.toCokleisli_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Comonad C) (X : C) : (CategoryTheory.Cokleisli.Adjunction.toCokleisli U).toPrefunctor.obj X = X

def CategoryTheory.Cokleisli.Adjunction.toCokleisli {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Comonad C) : CategoryTheory.Functor C (CategoryTheory.Cokleisli U)

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

Equations

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

@[simp]

theorem CategoryTheory.Cokleisli.Adjunction.fromCokleisli_map {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Comonad C) {X : CategoryTheory.Cokleisli U} : ∀ {x : CategoryTheory.Cokleisli U} (f : X ⟶ x), (CategoryTheory.Cokleisli.Adjunction.fromCokleisli U).toPrefunctor.map f = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Comonad.δ U).app X) (U.toPrefunctor.map f)

@[simp]

theorem CategoryTheory.Cokleisli.Adjunction.fromCokleisli_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Comonad C) (X : CategoryTheory.Cokleisli U) : (CategoryTheory.Cokleisli.Adjunction.fromCokleisli U).toPrefunctor.obj X = U.toPrefunctor.obj X

def CategoryTheory.Cokleisli.Adjunction.fromCokleisli {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Comonad C) : CategoryTheory.Functor (CategoryTheory.Cokleisli U) C

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.

def CategoryTheory.Cokleisli.Adjunction.adj {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Comonad C) : CategoryTheory.Cokleisli.Adjunction.fromCokleisli U ⊣ CategoryTheory.Cokleisli.Adjunction.toCokleisli U

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.

def CategoryTheory.Cokleisli.Adjunction.toCokleisliCompFromCokleisliIsoSelf {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Comonad C) : CategoryTheory.Functor.comp (CategoryTheory.Cokleisli.Adjunction.toCokleisli U) (CategoryTheory.Cokleisli.Adjunction.fromCokleisli U) ≅ U.toFunctor

The composition of the adjunction gives the original functor.

Equations

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