mathlib3 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 #

Riehl, Category theory in context, Definition 5.2.9

@[nolint]

def category_theory.kleisli {C : Type u} [category_theory.category C] (T : category_theory.monad C) :

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

category_theory.kleisli T = C

Instances for category_theory.kleisli

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

category_theory.kleisli.inhabited T = {default := inhabited.default _inst_2}

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

category_theory.kleisli.kleisli.category T = {to_category_struct := {to_quiver := {hom := λ (X Y : C), X ⟶ ↑T.obj Y}, id := λ (X : category_theory.kleisli T), T.η.app X, comp := λ (X Y Z : category_theory.kleisli T) (f : X ⟶ Y) (g : Y ⟶ Z), f ≫ ↑T.map g ≫ T.μ.app Z}, id_comp' := _, comp_id' := _, assoc' := _}

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

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

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

category_theory.kleisli.adjunction.to_kleisli T = {obj := λ (X : C), X, map := λ (X Y : C) (f : X ⟶ Y), f ≫ T.η.app Y, map_id' := _, map_comp' := _}

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

category_theory.kleisli.adjunction.from_kleisli T = {obj := λ (X : category_theory.kleisli T), T.to_functor.obj X, map := λ (X Y : category_theory.kleisli T) (f : X ⟶ Y), T.to_functor.map f ≫ T.μ.app Y, map_id' := _, map_comp' := _}

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

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

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

category_theory.kleisli.adjunction.adj T = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : C) (Y : category_theory.kleisli T), equiv.refl (X ⟶ T.to_functor.obj Y), hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}

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

category_theory.kleisli.adjunction.to_kleisli_comp_from_kleisli_iso_self T = category_theory.nat_iso.of_components (λ (X : C), category_theory.iso.refl ((category_theory.kleisli.adjunction.to_kleisli T ⋙ category_theory.kleisli.adjunction.from_kleisli T).obj X)) _

@[nolint]

def category_theory.cokleisli {C : Type u} [category_theory.category C] (U : category_theory.comonad C) :

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

category_theory.cokleisli U = C

Instances for category_theory.cokleisli

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

category_theory.cokleisli.inhabited U = {default := inhabited.default _inst_2}

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

category_theory.cokleisli.cokleisli.category U = {to_category_struct := {to_quiver := {hom := λ (X Y : C), ↑U.obj X ⟶ Y}, id := λ (X : category_theory.cokleisli U), U.ε.app X, comp := λ (X Y Z : category_theory.cokleisli U) (f : X ⟶ Y) (g : Y ⟶ Z), U.δ.app X ≫ ↑U.map f ≫ g}, id_comp' := _, comp_id' := _, assoc' := _}

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

category_theory.cokleisli.adjunction.to_cokleisli U = {obj := λ (X : C), X, map := λ (X Y : C) (f : X ⟶ Y), U.ε.app X ≫ f, map_id' := _, map_comp' := _}

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

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

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

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

category_theory.cokleisli.adjunction.from_cokleisli U = {obj := λ (X : category_theory.cokleisli U), U.to_functor.obj X, map := λ (X Y : category_theory.cokleisli U) (f : X ⟶ Y), U.δ.app X ≫ U.to_functor.map f, map_id' := _, map_comp' := _}

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

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

category_theory.cokleisli.adjunction.adj U = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : category_theory.cokleisli U) (Y : C), equiv.refl (U.to_functor.obj X ⟶ Y), hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}

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

category_theory.cokleisli.adjunction.to_cokleisli_comp_from_cokleisli_iso_self U = category_theory.nat_iso.of_components (λ (X : C), category_theory.iso.refl ((category_theory.cokleisli.adjunction.to_cokleisli U ⋙ category_theory.cokleisli.adjunction.from_cokleisli U).obj X)) _