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_mul {C : Type u} [CategoryTheory.Category.{v, u} C] (M : CategoryTheory.Monad C) : (CategoryTheory.Monad.toMon M).mul = CategoryTheory.Monad.μ M

@[simp]

theorem CategoryTheory.Monad.toMon_X {C : Type u} [CategoryTheory.Category.{v, u} C] (M : CategoryTheory.Monad C) : (CategoryTheory.Monad.toMon M).X = M.toFunctor

@[simp]

theorem CategoryTheory.Monad.toMon_one {C : Type u} [CategoryTheory.Category.{v, u} C] (M : CategoryTheory.Monad C) : (CategoryTheory.Monad.toMon M).one = CategoryTheory.Monad.η M

def CategoryTheory.Monad.toMon {C : Type u} [CategoryTheory.Category.{v, u} C] (M : CategoryTheory.Monad C) : Mon_ (CategoryTheory.Functor C C)

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

@[simp]

theorem CategoryTheory.Monad.monadToMon_map_hom (C : Type u) [CategoryTheory.Category.{v, u} C] : ∀ {X Y : CategoryTheory.Monad C} (f : X ⟶ Y), ((CategoryTheory.Monad.monadToMon C).map f).hom = f.toNatTrans

@[simp]

theorem CategoryTheory.Monad.monadToMon_obj (C : Type u) [CategoryTheory.Category.{v, u} C] (M : CategoryTheory.Monad C) : (CategoryTheory.Monad.monadToMon C).obj M = CategoryTheory.Monad.toMon M

def CategoryTheory.Monad.monadToMon (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (CategoryTheory.Monad C) (Mon_ (CategoryTheory.Functor C C))

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

@[simp]

theorem CategoryTheory.Monad.ofMon_μ {C : Type u} [CategoryTheory.Category.{v, u} C] (M : Mon_ (CategoryTheory.Functor C C)) : CategoryTheory.Monad.μ (CategoryTheory.Monad.ofMon M) = M.mul

@[simp]

theorem CategoryTheory.Monad.ofMon_η {C : Type u} [CategoryTheory.Category.{v, u} C] (M : Mon_ (CategoryTheory.Functor C C)) : CategoryTheory.Monad.η (CategoryTheory.Monad.ofMon M) = M.one

def CategoryTheory.Monad.ofMon {C : Type u} [CategoryTheory.Category.{v, u} C] (M : Mon_ (CategoryTheory.Functor C C)) : CategoryTheory.Monad C

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

@[simp]

theorem CategoryTheory.Monad.ofMon_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (M : Mon_ (CategoryTheory.Functor C C)) (X : C) : (CategoryTheory.Monad.ofMon M).toFunctor.obj X = M.X.obj X

@[simp]

theorem CategoryTheory.Monad.monToMonad_obj (C : Type u) [CategoryTheory.Category.{v, u} C] (M : Mon_ (CategoryTheory.Functor C C)) : (CategoryTheory.Monad.monToMonad C).obj M = CategoryTheory.Monad.ofMon M

@[simp]

theorem CategoryTheory.Monad.monToMonad_map_toNatTrans_app (C : Type u) [CategoryTheory.Category.{v, u} C] {X : Mon_ (CategoryTheory.Functor C C)} {Y : Mon_ (CategoryTheory.Functor C C)} (f : X ⟶ Y) (X : C) : ((CategoryTheory.Monad.monToMonad C).map f).app X = f.hom.app X

def CategoryTheory.Monad.monToMonad (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (Mon_ (CategoryTheory.Functor C C)) (CategoryTheory.Monad C)

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

@[simp]

theorem CategoryTheory.Monad.monadMonEquiv_inverse (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.Monad.monadMonEquiv C).inverse = CategoryTheory.Monad.monToMonad C

@[simp]

theorem CategoryTheory.Monad.monadMonEquiv_unitIso_hom_app_toNatTrans_app (C : Type u) [CategoryTheory.Category.{v, u} C] : ∀ (x : CategoryTheory.Monad C) (x_1 : C), ((CategoryTheory.Monad.monadMonEquiv C).unitIso.hom.app x).app x_1 = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.id (CategoryTheory.Monad C)).obj x).obj x_1)

@[simp]

theorem CategoryTheory.Monad.monadMonEquiv_unitIso_inv_app_toNatTrans_app (C : Type u) [CategoryTheory.Category.{v, u} C] : ∀ (x : CategoryTheory.Monad C) (x_1 : C), ((CategoryTheory.Monad.monadMonEquiv C).unitIso.inv.app x).app x_1 = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.comp (CategoryTheory.Monad.monadToMon C) (CategoryTheory.Monad.monToMonad C)).obj x).obj x_1)

@[simp]

theorem CategoryTheory.Monad.monadMonEquiv_functor (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.Monad.monadMonEquiv C).functor = CategoryTheory.Monad.monadToMon C

@[simp]

theorem CategoryTheory.Monad.monadMonEquiv_counitIso_hom_app_hom (C : Type u) [CategoryTheory.Category.{v, u} C] : ∀ (x : Mon_ (CategoryTheory.Functor C C)), ((CategoryTheory.Monad.monadMonEquiv C).counitIso.hom.app x).hom = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.comp (CategoryTheory.Monad.monToMonad C) (CategoryTheory.Monad.monadToMon C)).obj x).X

@[simp]

theorem CategoryTheory.Monad.monadMonEquiv_counitIso_inv_app_hom (C : Type u) [CategoryTheory.Category.{v, u} C] : ∀ (x : Mon_ (CategoryTheory.Functor C C)), ((CategoryTheory.Monad.monadMonEquiv C).counitIso.inv.app x).hom = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id (Mon_ (CategoryTheory.Functor C C))).obj x).X

def CategoryTheory.Monad.monadMonEquiv (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Monad C ≌ Mon_ (CategoryTheory.Functor C C)

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