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).
source
def CategoryTheory.Monad.toMon {C : Type u} [Category.{v, u} C] (M : Monad C) :
Mon_ (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 := ⋯ }
source
@[simp]
theorem CategoryTheory.Monad.toMon_mul {C : Type u} [Category.{v, u} C] (M : Monad C) :
M.toMon.mul = M.μ
source
@[simp]
theorem CategoryTheory.Monad.toMon_one {C : Type u} [Category.{v, u} C] (M : Monad C) :
M.toMon.one = M.η
source
@[simp]
theorem CategoryTheory.Monad.toMon_X {C : Type u} [Category.{v, u} C] (M : Monad C) :
M.toMon.X = M.toFunctor
source
def CategoryTheory.Monad.monadToMon (C : Type u) [Category.{v, u} C] :
Functor (Monad C) (Mon_ (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.
source
@[simp]
theorem CategoryTheory.Monad.monadToMon_map_hom (C : Type u) [Category.{v, u} C] {X✝ Y✝ : Monad C} (f : X✝ ⟶ Y✝) :
((monadToMon C).map f).hom = f.toNatTrans
source
@[simp]
theorem CategoryTheory.Monad.monadToMon_obj (C : Type u) [Category.{v, u} C] (M : Monad C) :
(monadToMon C).obj M = M.toMon
source
def CategoryTheory.Monad.ofMon {C : Type u} [Category.{v, u} C] (M : Mon_ (Functor C C)) :
Monad C

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

Equations
source
@[simp]
theorem CategoryTheory.Monad.ofMon_η {C : Type u} [Category.{v, u} C] (M : Mon_ (Functor C C)) :
(ofMon M).η = M.one
source
@[simp]
theorem CategoryTheory.Monad.ofMon_μ {C : Type u} [Category.{v, u} C] (M : Mon_ (Functor C C)) :
(ofMon M).μ = M.mul
source
@[simp]
theorem CategoryTheory.Monad.ofMon_obj {C : Type u} [Category.{v, u} C] (M : Mon_ (Functor C C)) (X : C) :
(ofMon M).obj X = M.X.obj X
source
def CategoryTheory.Monad.monToMonad (C : Type u) [Category.{v, u} C] :
Functor (Mon_ (Functor C C)) (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.
source
@[simp]
theorem CategoryTheory.Monad.monToMonad_obj (C : Type u) [Category.{v, u} C] (M : Mon_ (Functor C C)) :
(monToMonad C).obj M = ofMon M
source
@[simp]
theorem CategoryTheory.Monad.monToMonad_map_toNatTrans (C : Type u) [Category.{v, u} C] {X Y : Mon_ (Functor C C)} (f : X ⟶ Y) :
((monToMonad C).map f).toNatTrans = f.hom
source
def CategoryTheory.Monad.monadMonEquiv (C : Type u) [Category.{v, u} C] :
Monad C ≌ Mon_ (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.
source
@[simp]
theorem CategoryTheory.Monad.monadMonEquiv_unitIso_hom_app_toNatTrans_app (C : Type u) [Category.{v, u} C] (x✝ : Monad C) (x✝¹ : C) :
((monadMonEquiv C).unitIso.hom.app x✝).app x✝¹ = CategoryStruct.id (((Functor.id (Monad C)).obj x✝).obj x✝¹)
source
@[simp]
theorem CategoryTheory.Monad.monadMonEquiv_unitIso_inv_app_toNatTrans_app (C : Type u) [Category.{v, u} C] (x✝ : Monad C) (x✝¹ : C) :
((monadMonEquiv C).unitIso.inv.app x✝).app x✝¹ = CategoryStruct.id ((((monadToMon C).comp (monToMonad C)).obj x✝).obj x✝¹)
source
@[simp]
theorem CategoryTheory.Monad.monadMonEquiv_counitIso_inv_app_hom (C : Type u) [Category.{v, u} C] (x✝ : Mon_ (Functor C C)) :
((monadMonEquiv C).counitIso.inv.app x✝).hom = CategoryStruct.id ((Functor.id (Mon_ (Functor C C))).obj x✝).X
source
@[simp]
theorem CategoryTheory.Monad.monadMonEquiv_counitIso_hom_app_hom (C : Type u) [Category.{v, u} C] (x✝ : Mon_ (Functor C C)) :
((monadMonEquiv C).counitIso.hom.app x✝).hom = CategoryStruct.id (((monToMonad C).comp (monadToMon C)).obj x✝).X
source
@[simp]
theorem CategoryTheory.Monad.monadMonEquiv_inverse (C : Type u) [Category.{v, u} C] :
(monadMonEquiv C).inverse = monToMonad C
source
@[simp]
theorem CategoryTheory.Monad.monadMonEquiv_functor (C : Type u) [Category.{v, u} C] :
(monadMonEquiv C).functor = monadToMon C