Kleisli

📁 Source: Mathlib/CategoryTheory/Monad/Kleisli.lean

Statistics

Metric	Count
Definitions Cokleisli, adj, fromCokleisli, toCokleisli, toCokleisliCompFromCokleisliIsoSelf, of, category, instInhabited, of, Kleisli, adj, fromKleisli, toKleisli, toKleisliCompFromKleisliIsoSelf, of, category, instInhabited, of	18
Theorems fromCokleisli_map, fromCokleisli_obj, toCokleisli_map_of, toCokleisli_obj_of, ext, ext_iff, category_comp_of, category_id_of, hom_ext, hom_ext_iff, mk_of, of_mk, fromKleisli_map, fromKleisli_obj, toKleisli_map_of, toKleisli_obj_of, ext, ext_iff, category_comp_of, category_id_of, hom_ext, hom_ext_iff, mk_of, of_mk	24
Total	42

CategoryTheory

Definitions

Name	Category	Theorems
Cokleisli 📖	CompData	6 math math: Cokleisli.category_id_of, Cokleisli.Adjunction.toCokleisli_map_of, Cokleisli.Adjunction.toCokleisli_obj_of, Cokleisli.Adjunction.fromCokleisli_map, Cokleisli.category_comp_of, Cokleisli.Adjunction.fromCokleisli_obj
Kleisli 📖	CompData	12 math math: eq_counitIso, eq_functor_obj_of, Kleisli.category_comp_of, Kleisli.Adjunction.toKleisli_map_of, eq_inverse_obj, Kleisli.Adjunction.toKleisli_obj_of, Kleisli.category_id_of, eq_functor_map_of, Kleisli.Adjunction.fromKleisli_map, eq_unitIso, Kleisli.Adjunction.fromKleisli_obj, eq_inverse_map

CategoryTheory.Cokleisli

Definitions

Name	Category	Theorems
category 📖	CompOp	6 math math: category_id_of, Adjunction.toCokleisli_map_of, Adjunction.toCokleisli_obj_of, Adjunction.fromCokleisli_map, category_comp_of, Adjunction.fromCokleisli_obj
instInhabited 📖	CompOp	—
of 📖	CompOp	8 math math: of_mk, category_id_of, mk_of, Adjunction.toCokleisli_map_of, Adjunction.toCokleisli_obj_of, Adjunction.fromCokleisli_map, category_comp_of, Adjunction.fromCokleisli_obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
category_comp_of 📖	mathematical	—	Hom.of CategoryTheory.CategoryStruct.comp CategoryTheory.Cokleisli CategoryTheory.Category.toCategoryStruct category CategoryTheory.Functor.obj CategoryTheory.Comonad.toFunctor of CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Comonad.δ CategoryTheory.Functor.map	—	—
category_id_of 📖	mathematical	—	Hom.of CategoryTheory.CategoryStruct.id CategoryTheory.Cokleisli CategoryTheory.Category.toCategoryStruct category CategoryTheory.NatTrans.app CategoryTheory.Comonad.toFunctor CategoryTheory.Functor.id CategoryTheory.Comonad.ε of	—	—
hom_ext 📖	—	Hom.of	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.of	—	hom_ext
mk_of 📖	mathematical	—	of	—	—
of_mk 📖	mathematical	—	of	—	—

CategoryTheory.Cokleisli.Adjunction

Definitions

Name	Category	Theorems
adj 📖	CompOp	—
fromCokleisli 📖	CompOp	2 math math: fromCokleisli_map, fromCokleisli_obj
toCokleisli 📖	CompOp	2 math math: toCokleisli_map_of, toCokleisli_obj_of
toCokleisliCompFromCokleisliIsoSelf 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fromCokleisli_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Cokleisli CategoryTheory.Cokleisli.category fromCokleisli CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comonad.toFunctor CategoryTheory.Cokleisli.of CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Comonad.δ CategoryTheory.Cokleisli.Hom.of	—	—
fromCokleisli_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Cokleisli CategoryTheory.Cokleisli.category fromCokleisli CategoryTheory.Comonad.toFunctor CategoryTheory.Cokleisli.of	—	—
toCokleisli_map_of 📖	mathematical	—	CategoryTheory.Cokleisli.Hom.of CategoryTheory.Functor.map CategoryTheory.Cokleisli CategoryTheory.Cokleisli.category toCokleisli CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Comonad.toFunctor CategoryTheory.Cokleisli.of CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Comonad.ε	—	—
toCokleisli_obj_of 📖	mathematical	—	CategoryTheory.Cokleisli.of CategoryTheory.Functor.obj CategoryTheory.Cokleisli CategoryTheory.Cokleisli.category toCokleisli	—	—

CategoryTheory.Cokleisli.Hom

Definitions

Name	Category	Theorems
of 📖	CompOp	6 math math: CategoryTheory.Cokleisli.hom_ext_iff, CategoryTheory.Cokleisli.category_id_of, CategoryTheory.Cokleisli.Adjunction.toCokleisli_map_of, CategoryTheory.Cokleisli.Adjunction.fromCokleisli_map, CategoryTheory.Cokleisli.category_comp_of, ext_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	of	—	—	—
ext_iff 📖	mathematical	—	of	—	ext

CategoryTheory.Kleisli

Definitions

Name	Category	Theorems
category 📖	CompOp	12 math math: CategoryTheory.eq_counitIso, CategoryTheory.eq_functor_obj_of, category_comp_of, Adjunction.toKleisli_map_of, CategoryTheory.eq_inverse_obj, Adjunction.toKleisli_obj_of, category_id_of, CategoryTheory.eq_functor_map_of, Adjunction.fromKleisli_map, CategoryTheory.eq_unitIso, Adjunction.fromKleisli_obj, CategoryTheory.eq_inverse_map
instInhabited 📖	CompOp	—
of 📖	CompOp	12 math math: CategoryTheory.eq_counitIso, CategoryTheory.eq_functor_obj_of, category_comp_of, Adjunction.toKleisli_map_of, CategoryTheory.eq_inverse_obj, Adjunction.toKleisli_obj_of, category_id_of, mk_of, Adjunction.fromKleisli_map, CategoryTheory.eq_unitIso, Adjunction.fromKleisli_obj, of_mk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
category_comp_of 📖	mathematical	—	Hom.of CategoryTheory.CategoryStruct.comp CategoryTheory.Kleisli CategoryTheory.Category.toCategoryStruct category of CategoryTheory.Functor.obj CategoryTheory.Monad.toFunctor CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Monad.μ	—	—
category_id_of 📖	mathematical	—	Hom.of CategoryTheory.CategoryStruct.id CategoryTheory.Kleisli CategoryTheory.Category.toCategoryStruct category CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Monad.toFunctor CategoryTheory.Monad.η of	—	—
hom_ext 📖	—	Hom.of	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.of	—	hom_ext
mk_of 📖	mathematical	—	of	—	—
of_mk 📖	mathematical	—	of	—	—

CategoryTheory.Kleisli.Adjunction

Definitions

Name	Category	Theorems
adj 📖	CompOp	—
fromKleisli 📖	CompOp	2 math math: fromKleisli_map, fromKleisli_obj
toKleisli 📖	CompOp	2 math math: toKleisli_map_of, toKleisli_obj_of
toKleisliCompFromKleisliIsoSelf 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fromKleisli_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Kleisli CategoryTheory.Kleisli.category fromKleisli CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Monad.toFunctor CategoryTheory.Kleisli.of CategoryTheory.Kleisli.Hom.of CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Monad.μ	—	—
fromKleisli_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Kleisli CategoryTheory.Kleisli.category fromKleisli CategoryTheory.Monad.toFunctor CategoryTheory.Kleisli.of	—	—
toKleisli_map_of 📖	mathematical	—	CategoryTheory.Kleisli.Hom.of CategoryTheory.Functor.map CategoryTheory.Kleisli CategoryTheory.Kleisli.category toKleisli CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Kleisli.of CategoryTheory.Functor.obj CategoryTheory.Monad.toFunctor CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Monad.η	—	—
toKleisli_obj_of 📖	mathematical	—	CategoryTheory.Kleisli.of CategoryTheory.Functor.obj CategoryTheory.Kleisli CategoryTheory.Kleisli.category toKleisli	—	—

CategoryTheory.Kleisli.Hom

Definitions

Name	Category	Theorems
of 📖	CompOp	10 math math: CategoryTheory.eq_counitIso, CategoryTheory.Kleisli.category_comp_of, CategoryTheory.Kleisli.Adjunction.toKleisli_map_of, CategoryTheory.Kleisli.category_id_of, CategoryTheory.eq_functor_map_of, CategoryTheory.Kleisli.Adjunction.fromKleisli_map, ext_iff, CategoryTheory.eq_unitIso, CategoryTheory.Kleisli.hom_ext_iff, CategoryTheory.eq_inverse_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	of	—	—	—
ext_iff 📖	mathematical	—	of	—	ext

---

← Back to Index