# 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]
theorem CategoryTheory.Monad.toMon_one {C : Type u} (M : ) :
M.toMon.one = M
@[simp]
theorem CategoryTheory.Monad.toMon_mul {C : Type u} (M : ) :
M.toMon.mul = M
@[simp]
theorem CategoryTheory.Monad.toMon_X {C : Type u} (M : ) :
M.toMon.X = M.toFunctor
def CategoryTheory.Monad.toMon {C : Type u} (M : ) :

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
@[simp]
.obj M = M.toMon
@[simp]
∀ {X Y : } (f : X Y), (.map f).hom = f.toNatTrans

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.ofMon_μ {C : Type u} (M : ) :
= M.mul
@[simp]
theorem CategoryTheory.Monad.ofMon_η {C : Type u} (M : ) :
= M.one
def CategoryTheory.Monad.ofMon {C : Type u} (M : ) :

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

Equations
• = { toFunctor := M.X, η' := M.one, μ' := M.mul, assoc' := , left_unit' := , right_unit' := }
Instances For
@[simp]
theorem CategoryTheory.Monad.ofMon_obj {C : Type u} (M : ) (X : C) :
.obj X = M.X.obj X
@[simp]
theorem CategoryTheory.Monad.monToMonad_map_toNatTrans (C : Type u) {X : } {Y : } (f : X Y) :
(.map f).toNatTrans = f.hom
@[simp]

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]
∀ (x : ) (x_1 : C), (.unitIso.inv.app x).app x_1 = CategoryTheory.CategoryStruct.id ((().obj x).obj x_1)
@[simp]