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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Definitions/Theorems #

to_Mon associates a monoid object in C ⥤ C to any monad on C.
Monad_to_Mon is the functorial version of to_Mon.
of_Mon associates a monad on C to any monoid object in C ⥤ C.
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] :

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, one := M.η, mul := M.μ, one_mul' := _, mul_one' := _, mul_assoc' := _}

source

@[simp]

theorem category_theory.Monad.to_Mon_mul {C : Type u} [category_theory.category C] (ᾰ : category_theory.monad C) :

(category_theory.Monad.to_Mon ᾰ).mul = ᾰ.μ

source

@[simp]

theorem category_theory.Monad.to_Mon_one {C : Type u} [category_theory.category C] (ᾰ : category_theory.monad C) :

(category_theory.Monad.to_Mon ᾰ).one = ᾰ.η

source

@[simp]

theorem category_theory.Monad.to_Mon_X {C : Type u} [category_theory.category C] (ᾰ : category_theory.monad C) :

(category_theory.Monad.to_Mon ᾰ).X = ↑ᾰ

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

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' := _}

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] (ᾰ : category_theory.monad C) :

(category_theory.Monad.Monad_to_Mon C).obj ᾰ = category_theory.Monad.to_Mon ᾰ

source

@[simp]

theorem category_theory.Monad.of_Mon_μ {C : Type u} [category_theory.category C] (ᾰ : Mon_ (C ⥤ C)) :

(category_theory.Monad.of_Mon ᾰ).μ = ᾰ.mul

source

@[simp]

theorem category_theory.Monad.of_Mon_coe {C : Type u} [category_theory.category C] (ᾰ : Mon_ (C ⥤ C)) :

↑(category_theory.Monad.of_Mon ᾰ) = ᾰ.X

source

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.

Equations

category_theory.Monad.of_Mon = λ (M : Mon_ (C ⥤ C)), {to_functor := M.X, η' := M.one, μ' := M.mul, assoc' := _, left_unit' := _, right_unit' := _}

source

@[simp]

theorem category_theory.Monad.of_Mon_η {C : Type u} [category_theory.category C] (ᾰ : Mon_ (C ⥤ C)) :

(category_theory.Monad.of_Mon ᾰ).η = ᾰ.one

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

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' := _}

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] (ᾰ : Mon_ (C ⥤ C)) :

(category_theory.Monad.Mon_to_Monad C).obj ᾰ = category_theory.Monad.of_Mon ᾰ

source

@[simp]

theorem category_theory.Monad.Monad_Mon_equiv.counit_iso_hom_app_hom_app {C : Type u} [category_theory.category C] (_x : Mon_ (C ⥤ C)) (X : C) :

(category_theory.Monad.Monad_Mon_equiv.counit_iso.hom.app _x).hom.app X = 𝟙 (((category_theory.Monad.Mon_to_Monad C ⋙ category_theory.Monad.Monad_to_Mon C).obj _x).X.obj X)

source

@[simp]

theorem category_theory.Monad.Monad_Mon_equiv.counit_iso_inv_app_hom_app {C : Type u} [category_theory.category C] (_x : Mon_ (C ⥤ C)) (X : C) :

(category_theory.Monad.Monad_Mon_equiv.counit_iso.inv.app _x).hom.app X = 𝟙 (((𝟭 (Mon_ (C ⥤ C))).obj _x).X.obj X)

source

def category_theory.Monad.Monad_Mon_equiv.counit_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

category_theory.Monad.Monad_Mon_equiv.counit_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' := _}

source

@[simp]

theorem category_theory.Monad.Monad_Mon_equiv.unit_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.Monad_Mon_equiv.unit_iso_hom.app _x).to_nat_trans.app _x_1 = 𝟙 (↑((𝟭 (category_theory.monad C)).obj _x).obj _x_1)

source

def category_theory.Monad.Monad_Mon_equiv.unit_iso_hom {C : Type u} [category_theory.category C] :

𝟭 (category_theory.monad C) ⟶ category_theory.Monad.Monad_to_Mon C ⋙ category_theory.Monad.Mon_to_Monad C

Auxiliary definition for Monad_Mon_equiv

Equations

category_theory.Monad.Monad_Mon_equiv.unit_iso_hom = {app := λ (_x : category_theory.monad C), {to_nat_trans := {app := λ (_x_1 : C), 𝟙 (↑((𝟭 (category_theory.monad C)).obj _x).obj _x_1), naturality' := _}, app_η' := _, app_μ' := _}, naturality' := _}

source

@[simp]

theorem category_theory.Monad.Monad_Mon_equiv.unit_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.Monad_Mon_equiv.unit_iso_inv.app _x).to_nat_trans.app _x_1 = 𝟙 (↑((category_theory.Monad.Monad_to_Mon C ⋙ category_theory.Monad.Mon_to_Monad C).obj _x).obj _x_1)

source

def category_theory.Monad.Monad_Mon_equiv.unit_iso_inv {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)

Auxiliary definition for Monad_Mon_equiv

Equations

category_theory.Monad.Monad_Mon_equiv.unit_iso_inv = {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).obj _x_1), naturality' := _}, app_η' := _, app_μ' := _}, naturality' := _}

source

@[simp]

theorem category_theory.Monad.Monad_Mon_equiv.unit_iso_hom_2 {C : Type u} [category_theory.category C] :

category_theory.Monad.Monad_Mon_equiv.unit_iso.hom = category_theory.Monad.Monad_Mon_equiv.unit_iso_hom

source

def category_theory.Monad.Monad_Mon_equiv.unit_iso {C : Type u} [category_theory.category C] :

𝟭 (category_theory.monad C) ≅ category_theory.Monad.Monad_to_Mon C ⋙ category_theory.Monad.Mon_to_Monad C

Isomorphism of functors used in Monad_Mon_equiv

Equations

category_theory.Monad.Monad_Mon_equiv.unit_iso = {hom := category_theory.Monad.Monad_Mon_equiv.unit_iso_hom _inst_1, inv := category_theory.Monad.Monad_Mon_equiv.unit_iso_inv _inst_1, hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

theorem category_theory.Monad.Monad_Mon_equiv.unit_iso_inv_2 {C : Type u} [category_theory.category C] :

category_theory.Monad.Monad_Mon_equiv.unit_iso.inv = category_theory.Monad.Monad_Mon_equiv.unit_iso_inv

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

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.Monad_Mon_equiv.unit_iso _inst_1, counit_iso := category_theory.Monad.Monad_Mon_equiv.counit_iso _inst_1, functor_unit_iso_comp' := _}

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.Monad_Mon_equiv.counit_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.Monad_Mon_equiv.unit_iso

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

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

Definitions/Theorems #

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