mathlib3 documentation

category_theory.monad.equiv_mon

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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).

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

Equations

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

Equations

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

Equations

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

Equations