mathlib documentation

category_theory.monad.equiv_mon

The equivalence between Monad C and Mon_ (C ⥤ C).

A monad "is just" a monoid in the category of endofunctors.

Definitions/Theorems

  1. to_Mon associates a monoid object in C ⥤ C to any monad on C.
  2. Monad_to_Mon is the functorial version of to_Mon.
  3. of_Mon associates a monad on C to any monoid object in C ⥤ C.
  4. Monad_Mon_equiv is the equivalence between Monad C and Mon_ (C ⥤ C).
source
def category_theory.Monad.to_Mon {C : Type u} [category_theory.category C] (a : category_theory.Monad C) :
Mon_ (C ⥤ C)

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

Equations
source
@[simp]
theorem category_theory.Monad.to_Mon_mul {C : Type u} [category_theory.category C] (a : category_theory.Monad C) :
a.to_Mon.mul = μ_ a.func

source
@[simp]
theorem category_theory.Monad.to_Mon_one {C : Type u} [category_theory.category C] (a : category_theory.Monad C) :
a.to_Mon.one = η_ a.func

source
@[simp]
theorem category_theory.Monad.to_Mon_X {C : Type u} [category_theory.category C] (a : category_theory.Monad C) :
a.to_Mon.X = a.func

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

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

source
@[simp]
theorem category_theory.Monad.of_Mon_str_η {C : Type u} [category_theory.category C] (a : Mon_ (C ⥤ C)) :
η_ a.X = a.one

source
@[simp]
theorem category_theory.Monad.of_Mon_str_μ {C : Type u} [category_theory.category C] (a : Mon_ (C ⥤ C)) :
μ_ a.X = a.mul

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

source
def category_theory.Monad.of_Mon {C : Type u} [category_theory.category C] (a : Mon_ (C ⥤ C)) :
category_theory.Monad C

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

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

source
@[simp]
theorem category_theory.Monad.Mon_to_Monad_obj (C : Type u) [category_theory.category C] (a : Mon_ (C ⥤ C)) :
(category_theory.Monad.Mon_to_Monad C).obj a = category_theory.Monad.of_Mon a

source
def category_theory.Monad.of_to_mon_end_iso {C : Type u} [category_theory.category C] :
category_theory.Monad.Mon_to_Monad C ⋙ category_theory.Monad.Monad_to_Mon C ≅ 𝟭 (Mon_ (C ⥤ C))

Isomorphism of functors used in Monad_Mon_equiv

Equations
source
@[simp]
theorem category_theory.Monad.of_to_mon_end_iso_inv_app_hom {C : Type u} [category_theory.category C] (_x : Mon_ (C ⥤ C)) :
(category_theory.Monad.of_to_mon_end_iso.inv.app _x).hom = 𝟙 ((𝟭 (Mon_ (C ⥤ C))).obj _x).X

source
@[simp]
theorem category_theory.Monad.of_to_mon_end_iso_hom_app_hom {C : Type u} [category_theory.category C] (_x : Mon_ (C ⥤ C)) :
(category_theory.Monad.of_to_mon_end_iso.hom.app _x).hom = 𝟙 ((category_theory.Monad.Mon_to_Monad C ⋙ category_theory.Monad.Monad_to_Mon C).obj _x).X

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

source
def category_theory.Monad.to_of_mon_end_iso {C : Type u} [category_theory.category C] :
category_theory.Monad.Monad_to_Mon C ⋙ category_theory.Monad.Mon_to_Monad C ≅ 𝟭 (category_theory.Monad C)

Isomorphism of functors used in Monad_Mon_equiv

Equations
source
@[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)

source
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
source
@[simp]
theorem category_theory.Monad.Monad_Mon_equiv_counit_iso (C : Type u) [category_theory.category C] :
(category_theory.Monad.Monad_Mon_equiv C).counit_iso = category_theory.Monad.of_to_mon_end_iso

source
@[simp]
theorem category_theory.Monad.Monad_Mon_equiv_functor (C : Type u) [category_theory.category C] :
(category_theory.Monad.Monad_Mon_equiv C).functor = category_theory.Monad.Monad_to_Mon C

source
@[simp]
theorem category_theory.Monad.Monad_Mon_equiv_unit_iso (C : Type u) [category_theory.category C] :
(category_theory.Monad.Monad_Mon_equiv C).unit_iso = category_theory.Monad.to_of_mon_end_iso.symm

source
@[simp]
theorem category_theory.Monad.Monad_Mon_equiv_inverse (C : Type u) [category_theory.category C] :
(category_theory.Monad.Monad_Mon_equiv C).inverse = category_theory.Monad.Mon_to_Monad C