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.instInhabited {C : Type u} [CategoryTheory.Category.{v, u} C] [Inhabited C] (T : CategoryTheory.Monad C) : Inhabited (CategoryTheory.Kleisli T)

Equations

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

instance CategoryTheory.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.category T = CategoryTheory.Category.mk ⋯ ⋯ ⋯

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

• CategoryTheory.Kleisli.Adjunction.toKleisli T = { obj := fun (X : C) => X, map := fun {X Y : C} (f : X ⟶ Y) => CategoryTheory.CategoryStruct.comp f (T.η.app Y), map_id := ⋯, map_comp := ⋯ }

@[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).obj X = X

@[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).map f = CategoryTheory.CategoryStruct.comp f (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.

@[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).obj X = T.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).map f = CategoryTheory.CategoryStruct.comp (T.map f) (T.μ.app Y)

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.Kleisli.Adjunction.toKleisli T).comp (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.instInhabited {C : Type u} [CategoryTheory.Category.{v, u} C] [Inhabited C] (U : CategoryTheory.Comonad C) : Inhabited (CategoryTheory.Cokleisli U)

Equations

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

instance CategoryTheory.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.category U = CategoryTheory.Category.mk ⋯ ⋯ ⋯

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

• CategoryTheory.Cokleisli.Adjunction.toCokleisli U = { obj := fun (X : C) => X, map := fun {X x : C} (f : X ⟶ x) => CategoryTheory.CategoryStruct.comp (U.ε.app X) f, map_id := ⋯, map_comp := ⋯ }

@[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).obj X = X

@[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).map f = CategoryTheory.CategoryStruct.comp (U.ε.app X) f

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.

@[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).obj X = U.obj X

@[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).map f = CategoryTheory.CategoryStruct.comp (U.δ.app X) (U.map f)

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.Cokleisli.Adjunction.toCokleisli U).comp (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.