Documentation

Mathlib.CategoryTheory.Monad.EquivMon

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

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

Definitions/Theorems #

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

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

Equations
  • M.toMon = { X := M.toFunctor, one := M, mul := M, one_mul := , mul_one := , mul_assoc := }
Instances For

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

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

      Equations
      Instances For

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

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          Oh, monads are just monoids in the category of endofunctors (equivalence of categories).

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For