mathlib documentation

category_theory.monad.basic

@[class]
structure category_theory.monad {C : Type u₁} [category_theory.category C] :
C CType (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)
Instances
@[class]
structure category_theory.comonad {C : Type u₁} [category_theory.category C] :
C CType (max u₁ v₁)

The data of a comonad on C consists of an endofunctor G together with natural transformations ε : G ⟶ 𝟭 C and δ : G ⟶ G ⋙ G satisfying three equations:

  • δ_X ≫ G δ_X = δ_X ≫ δ_(GX) (coassociativity)
  • δ_X ≫ ε_(GX) = 1_X (left counit)
  • δ_X ≫ G ε_X = 1_X (right counit)
Instances
structure category_theory.monad_hom {C : Type u₁} [category_theory.category C] (M N : C C) [category_theory.monad M] [category_theory.monad N] :
Type (max u₁ v₁)

A morphisms of monads is a natural transformation compatible with η and μ.

structure category_theory.comonad_hom {C : Type u₁} [category_theory.category C] (M N : C C) [category_theory.comonad M] [category_theory.comonad N] :
Type (max u₁ v₁)

A morphisms of comonads is a natural transformation compatible with η and μ.

The identity natural transformations is a morphism of monads.

Equations

The composition of two morphisms of monads.

Equations
@[simp]

Note: category_theory.monad.bundled provides a category instance for bundled monads.

The identity natural transformations is a morphism of comonads.

Equations

The composition of two morphisms of comonads.

Equations
@[simp]

Note: category_theory.monad.bundled provides a category instance for bundled comonads.