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

structure 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.

• of : C

  The underlying object of the base category.

@[simp]

theorem CategoryTheory.Kleisli.mk_of {C : Type u} [Category.{v, u} C] {T : Monad C} (c : Kleisli T) : { of := c.of } = c

theorem CategoryTheory.Kleisli.of_mk {C : Type u} [Category.{v, u} C] {T : Monad C} (c : C) : { of := c }.of = c

structure CategoryTheory.Kleisli.Hom {C : Type u} [Category.{v, u} C] {T : Monad C} (c c' : Kleisli T) : Type v

For (T : Monad C), morphisms c ⟶ c' in the Kleisli category of T are morphisms c ⟶ T.obj c' in C.

• of : c.of ⟶ T.obj c'.of

  The morphism in C underlying the morphism in the Kleisli category.

@[implicit_reducible]

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 := { of := default } }

theorem CategoryTheory.Kleisli.Hom.ext {C : Type u} {inst✝ : Category.{v, u} C} {T : Monad C} {c c' : Kleisli T} {x y : c.Hom c'} (of : x.of = y.of) : x = y

theorem CategoryTheory.Kleisli.Hom.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {T : Monad C} {c c' : Kleisli T} {x y : c.Hom c'} : x = y ↔ x.of = y.of

@[implicit_reducible]

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

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

@[simp]

theorem CategoryTheory.Kleisli.category_id_of {C : Type u} [Category.{v, u} C] (T : Monad C) (X : Kleisli T) : (CategoryStruct.id X).of = T.η.app X.of

@[simp]

theorem CategoryTheory.Kleisli.category_comp_of {C : Type u} [Category.{v, u} C] (T : Monad C) {x✝ x✝¹ Z : Kleisli T} (f : x✝.Hom x✝¹) (g : x✝¹.Hom Z) : (CategoryStruct.comp f g).of = CategoryStruct.comp f.of (CategoryStruct.comp (T.map g.of) (T.μ.app Z.of))

theorem CategoryTheory.Kleisli.hom_ext {C : Type u} [Category.{v, u} C] {T : Monad C} {x y : Kleisli T} {f g : x ⟶ y} (h : f.of = g.of) : f = g

theorem CategoryTheory.Kleisli.hom_ext_iff {C : Type u} [Category.{v, u} C] {T : Monad C} {x y : Kleisli T} {f g : x ⟶ y} : f = g ↔ f.of = g.of

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

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

@[simp]

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

@[simp]

theorem CategoryTheory.Kleisli.Adjunction.toKleisli_map_of {C : Type u} [Category.{v, u} C] (T : Monad C) {X Y : C} (f : X ⟶ Y) : ((toKleisli T).map f).of = 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.of

@[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.of) (T.μ.app Y.of)

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.

structure 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.

• of : C

  The underlying object of the base category.

@[simp]

theorem CategoryTheory.Cokleisli.mk_of {C : Type u} [Category.{v, u} C] (U : Comonad C) (c : Cokleisli U) : { of := c.of } = c

theorem CategoryTheory.Cokleisli.of_mk {C : Type u} [Category.{v, u} C] (U : Comonad C) (c : C) : { of := c }.of = c

structure CategoryTheory.Cokleisli.Hom {C : Type u} [Category.{v, u} C] {U : Comonad C} (c c' : Cokleisli U) : Type v

For (U : Comonad C), morphisms c ⟶ c' in the Cokleisli category of U are morphisms U.obj c ⟶ c' in C.

• of : U.obj c.of ⟶ c'.of

  The morphism in C underlying the morphism in the Kleisli category.

@[implicit_reducible]

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 := { of := default } }

@[implicit_reducible]

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

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

@[simp]

theorem CategoryTheory.Cokleisli.category_comp_of {C : Type u} [Category.{v, u} C] (U : Comonad C) {X✝ Y✝ Z✝ : Cokleisli U} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) : (CategoryStruct.comp f g).of = CategoryStruct.comp (U.δ.app X✝.of) (CategoryStruct.comp (U.map f.of) g.of)

@[simp]

theorem CategoryTheory.Cokleisli.category_id_of {C : Type u} [Category.{v, u} C] (U : Comonad C) (X : Cokleisli U) : (CategoryStruct.id X).of = U.ε.app X.of

theorem CategoryTheory.Cokleisli.Hom.ext {C : Type u} {inst✝ : Category.{v, u} C} {U : Comonad C} {c c' : Cokleisli U} {x y : c.Hom c'} (of : x.of = y.of) : x = y

theorem CategoryTheory.Cokleisli.Hom.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {U : Comonad C} {c c' : Cokleisli U} {x y : c.Hom c'} : x = y ↔ x.of = y.of

theorem CategoryTheory.Cokleisli.hom_ext {C : Type u} [Category.{v, u} C] (U : Comonad C) {x y : Cokleisli U} {f g : x ⟶ y} (h : f.of = g.of) : f = g

theorem CategoryTheory.Cokleisli.hom_ext_iff {C : Type u} [Category.{v, u} C] {U : Comonad C} {x y : Cokleisli U} {f g : x ⟶ y} : f = g ↔ f.of = g.of

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

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

@[simp]

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

@[simp]

theorem CategoryTheory.Cokleisli.Adjunction.toCokleisli_map_of {C : Type u} [Category.{v, u} C] (U : Comonad C) {X x✝ : C} (f : X ⟶ x✝) : ((toCokleisli U).map f).of = 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_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.of) (U.map f.of)

@[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.of

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 comonad (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.