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

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

Equations

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

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

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

Equations

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

def CategoryTheory.Kleisli.Adjunction.toKleisli {C : Type u} [Category.{v, u} C] (T : Monad C) : Functor C (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} [Category.{v, u} C] (T : Monad C) (X : C) : (toKleisli T).obj X = X

@[simp]

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

def CategoryTheory.Kleisli.Adjunction.fromKleisli {C : Type u} [Category.{v, u} C] (T : Monad C) : Functor (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} [Category.{v, u} C] (T : Monad C) (X : Kleisli T) : (fromKleisli T).obj X = T.obj X

@[simp]

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

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

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

Equations

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

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

Equations

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

instance CategoryTheory.Cokleisli.category {C : Type u} [Category.{v, u} C] (U : Comonad C) : Category.{v, u} (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} [Category.{v, u} C] (U : Comonad C) : Functor C (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} [Category.{v, u} C] (U : Comonad C) (X : C) : (toCokleisli U).obj X = X

@[simp]

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

def CategoryTheory.Cokleisli.Adjunction.fromCokleisli {C : Type u} [Category.{v, u} C] (U : Comonad C) : Functor (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} [Category.{v, u} C] (U : Comonad C) (X : Cokleisli U) : (fromCokleisli U).obj X = U.obj X

@[simp]

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

def CategoryTheory.Cokleisli.Adjunction.adj {C : Type u} [Category.{v, u} C] (U : Comonad C) : fromCokleisli U ⊣ 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} [Category.{v, u} C] (U : Comonad C) : (toCokleisli U).comp (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.