The equivalence between Monad C
and Mon_ (C ⥤ C)
. #
A monad "is just" a monoid in the category of endofunctors.
Definitions/Theorems #
toMon
associates a monoid object inC ⥤ C
to any monad onC
.monadToMon
is the functorial version oftoMon
.ofMon
associates a monad onC
to any monoid object inC ⥤ C
.monadMonEquiv
is the equivalence betweenMonad C
andMon_ (C ⥤ C)
.
@[simp]
@[simp]
@[simp]
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
@[simp]
theorem
CategoryTheory.Monad.monadToMon_map_hom
(C : Type u)
[Category.{v, u} C]
{X✝ Y✝ : Monad C}
(f : X✝ ⟶ Y✝)
:
@[simp]
To every monoid object in C ⥤ C
we associate a Monad C
.
Equations
- CategoryTheory.Monad.ofMon M = { toFunctor := M.X, η := M.one, μ := M.mul, assoc := ⋯, left_unit := ⋯, right_unit := ⋯ }
Instances For
@[simp]
@[simp]
@[simp]
theorem
CategoryTheory.Monad.ofMon_obj
{C : Type u}
[Category.{v, u} C]
(M : Mon_ (Functor C C))
(X : C)
:
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
@[simp]
theorem
CategoryTheory.Monad.monToMonad_obj
(C : Type u)
[Category.{v, u} C]
(M : Mon_ (Functor C C))
:
@[simp]
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.