The equivalence between Monad C and Mon_ (C ⥤ C).
A monad "is just" a monoid in the category of endofunctors.
Definitions/Theorems
to_Monassociates a monoid object inC ⥤ Cto any monad onC.Monad_to_Monis the functorial version ofto_Mon.of_Monassociates a monad onCto any monoid object inC ⥤ C.Monad_Mon_equivis the equivalence betweenMonad CandMon_ (C ⥤ C).
@[simp]
theorem
category_theory.Monad.to_Mon_one
{C : Type u}
[category_theory.category C]
(a : category_theory.Monad C) :
def
category_theory.Monad.to_Mon
{C : Type u}
[category_theory.category C] :
category_theory.Monad C → Mon_ (C ⥤ C)
To every Monad C we associated a monoid object in C ⥤ C.
Equations
- category_theory.Monad.to_Mon = λ (M : category_theory.Monad C), {X := M.func, one := η_ M.func category_theory.Monad.category_theory.monad, mul := μ_ M.func category_theory.Monad.category_theory.monad, one_mul' := _, mul_one' := _, mul_assoc' := _}
@[simp]
theorem
category_theory.Monad.to_Mon_X
{C : Type u}
[category_theory.category C]
(a : category_theory.Monad C) :
@[simp]
theorem
category_theory.Monad.to_Mon_mul
{C : Type u}
[category_theory.category C]
(a : category_theory.Monad C) :
@[simp]
theorem
category_theory.Monad.Monad_to_Mon_map_hom
(C : Type u)
[category_theory.category C]
(_x _x_1 : category_theory.Monad C)
(f : _x ⟶ _x_1) :
((category_theory.Monad.Monad_to_Mon C).map f).hom = f.to_nat_trans
def
category_theory.Monad.Monad_to_Mon
(C : Type u)
[category_theory.category C] :
category_theory.Monad C ⥤ Mon_ (C ⥤ C)
Passing from Monad C to Mon_ (C ⥤ C) is functorial.
Equations
- category_theory.Monad.Monad_to_Mon C = {obj := category_theory.Monad.to_Mon _inst_1, map := λ (_x _x_1 : category_theory.Monad C) (f : _x ⟶ _x_1), {hom := f.to_nat_trans, one_hom' := _, mul_hom' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.Monad.Monad_to_Mon_obj
(C : Type u)
[category_theory.category C]
(a : category_theory.Monad C) :
(category_theory.Monad.Monad_to_Mon C).obj a = a.to_Mon
@[simp]
theorem
category_theory.Monad.of_Mon_func
{C : Type u}
[category_theory.category C]
(a : Mon_ (C ⥤ C)) :
(category_theory.Monad.of_Mon a).func = a.X
def
category_theory.Monad.of_Mon
{C : Type u}
[category_theory.category C] :
Mon_ (C ⥤ C) → category_theory.Monad C
To every monoid object in C ⥤ C we associate a Monad C.
@[simp]
theorem
category_theory.Monad.of_Mon_str_μ
{C : Type u}
[category_theory.category C]
(a : Mon_ (C ⥤ C)) :
@[simp]
theorem
category_theory.Monad.of_Mon_str_η
{C : Type u}
[category_theory.category C]
(a : Mon_ (C ⥤ C)) :
@[simp]
theorem
category_theory.Monad.Mon_to_Monad_map_to_nat_trans_app
(C : Type u)
[category_theory.category C]
(_x _x_1 : Mon_ (C ⥤ C))
(f : _x ⟶ _x_1)
(X : C) :
((category_theory.Monad.Mon_to_Monad C).map f).to_nat_trans.app X = f.hom.app X
def
category_theory.Monad.Mon_to_Monad
(C : Type u)
[category_theory.category C] :
Mon_ (C ⥤ C) ⥤ category_theory.Monad C
Passing from Mon_ (C ⥤ C) to Monad C is functorial.
Equations
- category_theory.Monad.Mon_to_Monad C = {obj := category_theory.Monad.of_Mon _inst_1, map := λ (_x _x_1 : Mon_ (C ⥤ C)) (f : _x ⟶ _x_1), {to_nat_trans := {app := f.hom.app, naturality' := _}, app_η' := _, app_μ' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.Monad.Mon_to_Monad_obj
(C : Type u)
[category_theory.category C]
(a : Mon_ (C ⥤ C)) :
@[simp]
theorem
category_theory.Monad.of_to_mon_end_iso_hom_app_hom
{C : Type u}
[category_theory.category C]
(_x : Mon_ (C ⥤ C)) :
Isomorphism of functors used in Monad_Mon_equiv
Equations
- category_theory.Monad.of_to_mon_end_iso = {hom := {app := λ (_x : Mon_ (C ⥤ C)), {hom := 𝟙 ((category_theory.Monad.Mon_to_Monad C ⋙ category_theory.Monad.Monad_to_Mon C).obj _x).X, one_hom' := _, mul_hom' := _}, naturality' := _}, inv := {app := λ (_x : Mon_ (C ⥤ C)), {hom := 𝟙 ((𝟭 (Mon_ (C ⥤ C))).obj _x).X, one_hom' := _, mul_hom' := _}, naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.Monad.to_of_mon_end_iso_hom_app_to_nat_trans_app
{C : Type u}
[category_theory.category C]
(_x : category_theory.Monad C)
(_x_1 : C) :
(category_theory.Monad.to_of_mon_end_iso.hom.app _x).to_nat_trans.app _x_1 = 𝟙 (((category_theory.Monad.Monad_to_Mon C ⋙ category_theory.Monad.Mon_to_Monad C).obj _x).func.obj _x_1)
@[simp]
theorem
category_theory.Monad.to_of_mon_end_iso_inv_app_to_nat_trans_app
{C : Type u}
[category_theory.category C]
(_x : category_theory.Monad C)
(_x_1 : C) :
(category_theory.Monad.to_of_mon_end_iso.inv.app _x).to_nat_trans.app _x_1 = 𝟙 (((𝟭 (category_theory.Monad C)).obj _x).func.obj _x_1)
Isomorphism of functors used in Monad_Mon_equiv
Equations
- category_theory.Monad.to_of_mon_end_iso = {hom := {app := λ (_x : category_theory.Monad C), {to_nat_trans := {app := λ (_x_1 : C), 𝟙 (((category_theory.Monad.Monad_to_Mon C ⋙ category_theory.Monad.Mon_to_Monad C).obj _x).func.obj _x_1), naturality' := _}, app_η' := _, app_μ' := _}, naturality' := _}, inv := {app := λ (_x : category_theory.Monad C), {to_nat_trans := {app := λ (_x_1 : C), 𝟙 (((𝟭 (category_theory.Monad C)).obj _x).func.obj _x_1), naturality' := _}, app_η' := _, app_μ' := _}, naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}
def
category_theory.Monad.Monad_Mon_equiv
(C : Type u)
[category_theory.category C] :
category_theory.Monad C ≌ Mon_ (C ⥤ C)
Oh, monads are just monoids in the category of endofunctors (equivalence of categories).
Equations
- category_theory.Monad.Monad_Mon_equiv C = {functor := category_theory.Monad.Monad_to_Mon C _inst_1, inverse := category_theory.Monad.Mon_to_Monad C _inst_1, unit_iso := category_theory.Monad.to_of_mon_end_iso.symm, counit_iso := category_theory.Monad.of_to_mon_end_iso _inst_1, functor_unit_iso_comp' := _}
@[simp]
@[simp]
@[simp]
@[simp]