# 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).
def category_theory.Monad.to_Mon {C : Type u}  :
Mon_ (C C)

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

Equations
@[simp]
@[simp]
@[simp]
Mon_ (C C)

Passing from Monad C to Mon_ (C ⥤ C) is functorial.

Equations
@[simp]
@[simp]
@[simp]
theorem category_theory.Monad.of_Mon_μ {C : Type u} (ᾰ : Mon_ (C C)) :
@[simp]
theorem category_theory.Monad.of_Mon_coe {C : Type u} (ᾰ : Mon_ (C C)) :
def category_theory.Monad.of_Mon {C : Type u}  :
Mon_ (C C)

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

Equations
@[simp]
theorem category_theory.Monad.of_Mon_η {C : Type u} (ᾰ : Mon_ (C C)) :
Mon_ (C C)

Passing from Mon_ (C ⥤ C) to Monad C is functorial.

Equations
@[simp]
theorem category_theory.Monad.Mon_to_Monad_map_to_nat_trans_app (C : Type u) (_x _x_1 : Mon_ (C C)) (f : _x _x_1) (X : C) :
= f.hom.app X
@[simp]
theorem category_theory.Monad.Mon_to_Monad_obj (C : Type u) (ᾰ : Mon_ (C C)) :
@[simp]
theorem category_theory.Monad.Monad_Mon_equiv.counit_iso_hom_app_hom_app {C : Type u} (_x : Mon_ (C C)) (X : C) :
@[simp]
theorem category_theory.Monad.Monad_Mon_equiv.counit_iso_inv_app_hom_app {C : Type u} (_x : Mon_ (C C)) (X : C) :
= 𝟙 (((𝟭 (Mon_ (C C))).obj _x).X.obj X)

Isomorphism of functors used in Monad_Mon_equiv

Equations

Auxiliary definition for Monad_Mon_equiv

Equations

Auxiliary definition for Monad_Mon_equiv

Equations
@[simp]

Isomorphism of functors used in Monad_Mon_equiv

Equations
@[simp]