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

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.

Equations

• M.toMon = { X := M.toFunctor, one := M.η, mul := M.μ, one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }

@[simp]

theorem CategoryTheory.Monad.toMon_mul {C : Type u} [CategoryTheory.Category.{v, u} C] (M : CategoryTheory.Monad C) : M.toMon.mul = M.μ

@[simp]

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

@[simp]

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

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.

Equations

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

@[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 = M.toMon

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.

Equations

• CategoryTheory.Monad.ofMon M = { toFunctor := M.X, η := M.one, μ := M.mul, assoc := ⋯, left_unit := ⋯, right_unit := ⋯ }

@[simp]

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

@[simp]

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

@[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).obj X = M.X.obj 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.

Equations

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

@[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 (C : Type u) [CategoryTheory.Category.{v, u} C] {X : Mon_ (CategoryTheory.Functor C C)} {Y : Mon_ (CategoryTheory.Functor C C)} (f : X ⟶ Y) : ((CategoryTheory.Monad.monToMonad C).map f).toNatTrans = f.hom

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

Equations

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

@[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.Monad.monadToMon C).comp (CategoryTheory.Monad.monToMonad C)).obj x).obj x_1)

@[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

@[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.Monad.monToMonad C).comp (CategoryTheory.Monad.monadToMon C)).obj x).X

@[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_functor (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.Monad.monadMonEquiv C).functor = CategoryTheory.Monad.monadToMon C