Theorems · Inductive type · category theory
CategoryTheory.Monad
(C : Type u₁) → [CategoryTheory.Category.{v₁, u₁} C] → Type (max u₁ v₁)The data of a monad on C consists of an endofunctor T together with natural transformations
η : 𝟭 C ⟶ T and μ : T ⋙ T ⟶ T satisfying three equations:
- T μ_X ≫ μ_X = μ_(TX) ≫ μ_X (associativity)
- η_(TX) ≫ μ_X = 1_X (left unit)
- Tη_X ≫ μ_X = 1_X (right unit)
- Defined in
- Mathlib.CategoryTheory.Monad.Basic
- Cited by
- 153 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement · cited by 32,673
Cited by252
Results whose statement or proof uses this declaration.
- CategoryTheory.Monad.toFunctorstatement and proof · cited by 127
- CategoryTheory.Monad.Algebrastatement · cited by 110
- CategoryTheory.Monad.Algebra.Astatement and proof · cited by 81
- CategoryTheory.Monad.Algebra.Hom.fstatement and proof · cited by 48
- CategoryTheory.Monad.Algebra.astatement and proof · cited by 45
- CategoryTheory.Monad.μstatement and proof · cited by 40
- CategoryTheory.Monad.ηstatement and proof · cited by 34
- CategoryTheory.Monad.forgetstatement and proof · cited by 29
- CategoryTheory.Kleislistatement · cited by 23
- CategoryTheory.Adjunction.toMonadstatement · cited by 22
- CategoryTheory.Kleisli.ofstatement and proof · cited by 21
- CategoryTheory.MonadHom.toNatTransstatement and proof · cited by 21
Showing the 200 most cited of 252.