mathlib documentation

category_theory.monad.equiv_mon

The equivalence between Monad C and Mon_ (C ⥤ C).

A monad "is just" a monoid in the category of endofunctors.

Definitions/Theorems

  1. to_Mon associates a monoid object in C ⥤ C to any monad on C.
  2. Monad_to_Mon is the functorial version of to_Mon.
  3. of_Mon associates a monad on C to any monoid object in C ⥤ C.
  4. Monad_Mon_equiv is the equivalence between Monad C and Mon_ (C ⥤ C).
@[simp]

Passing from Monad C to Mon_ (C ⥤ C) is functorial.

Equations
@[simp]
theorem category_theory.Monad.of_Mon_str_η {C : Type u} [category_theory.category C] (ᾰ : Mon_ (C C)) :
η_ ᾰ.X = ᾰ.one

@[simp]
theorem category_theory.Monad.of_Mon_str_μ {C : Type u} [category_theory.category C] (ᾰ : Mon_ (C C)) :
μ_ ᾰ.X = ᾰ.mul

@[simp]

To every monoid object in C ⥤ C we associate a Monad C.

Equations

Passing from Mon_ (C ⥤ C) to Monad C is functorial.

Equations
@[simp]