Documentation Verification Report

Kleisli

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

Statistics

Metric	Count
Definitions `Cokleisli`, `adj`, `fromCokleisli`, `toCokleisli`, `toCokleisliCompFromCokleisliIsoSelf`, `category`, `instInhabited`, `Kleisli`, `adj`, `fromKleisli`, `toKleisli`, `toKleisliCompFromKleisliIsoSelf`, `category`, `instInhabited`	14
Theorems `fromCokleisli_map`, `fromCokleisli_obj`, `toCokleisli_map`, `toCokleisli_obj`, `fromKleisli_map`, `fromKleisli_obj`, `toKleisli_map`, `toKleisli_obj`	8
Total	22

CategoryTheory

Definitions

Name	Category	Theorems
`Cokleisli` 📖	CompOp	4 math math: `Cokleisli.Adjunction.toCokleisli_obj`, `Cokleisli.Adjunction.fromCokleisli_map`, `Cokleisli.Adjunction.fromCokleisli_obj`, `Cokleisli.Adjunction.toCokleisli_map`
`Kleisli` 📖	CompOp	10 math math: `eq_counitIso`, `Kleisli.Adjunction.toKleisli_map`, `eq_functor_obj`, `eq_inverse_obj`, `Kleisli.Adjunction.toKleisli_obj`, `eq_functor_map`, `Kleisli.Adjunction.fromKleisli_map`, `eq_unitIso`, `Kleisli.Adjunction.fromKleisli_obj`, `eq_inverse_map`

CategoryTheory.Cokleisli

Definitions

Name	Category	Theorems
`category` 📖	CompOp	4 math math: `Adjunction.toCokleisli_obj`, `Adjunction.fromCokleisli_map`, `Adjunction.fromCokleisli_obj`, `Adjunction.toCokleisli_map`
`instInhabited` 📖	CompOp	—

CategoryTheory.Cokleisli.Adjunction

Definitions

Name	Category	Theorems
`adj` 📖	CompOp	—
`fromCokleisli` 📖	CompOp	2 math math: `fromCokleisli_map`, `fromCokleisli_obj`
`toCokleisli` 📖	CompOp	2 math math: `toCokleisli_obj`, `toCokleisli_map`
`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.Functor.comp` `CategoryTheory.NatTrans.app` `CategoryTheory.Comonad.δ`	—	—
`fromCokleisli_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Cokleisli` `CategoryTheory.Cokleisli.category` `fromCokleisli` `CategoryTheory.Comonad.toFunctor`	—	—
`toCokleisli_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Cokleisli` `CategoryTheory.Cokleisli.category` `toCokleisli` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Comonad.toFunctor` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `CategoryTheory.Comonad.ε`	—	—
`toCokleisli_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Cokleisli` `CategoryTheory.Cokleisli.category` `toCokleisli`	—	—

CategoryTheory.Kleisli

Definitions

Name	Category	Theorems
`category` 📖	CompOp	10 math math: `CategoryTheory.eq_counitIso`, `Adjunction.toKleisli_map`, `CategoryTheory.eq_functor_obj`, `CategoryTheory.eq_inverse_obj`, `Adjunction.toKleisli_obj`, `CategoryTheory.eq_functor_map`, `Adjunction.fromKleisli_map`, `CategoryTheory.eq_unitIso`, `Adjunction.fromKleisli_obj`, `CategoryTheory.eq_inverse_map`
`instInhabited` 📖	CompOp	—

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`, `toKleisli_obj`
`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.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Monad.μ`	—	—
`fromKleisli_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Kleisli` `CategoryTheory.Kleisli.category` `fromKleisli` `CategoryTheory.Monad.toFunctor`	—	—
`toKleisli_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Kleisli` `CategoryTheory.Kleisli.category` `toKleisli` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Monad.toFunctor` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `CategoryTheory.Monad.η`	—	—
`toKleisli_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Kleisli` `CategoryTheory.Kleisli.category` `toKleisli`	—	—

---

← Back to Index