# mathlibdocumentation

@[class]
structure category_theory.monad {C : Type u₁}  :
C CType (max u₁ v₁)

The data of a monad on C consists of an endofunctor T together with natural transformations η : 𝟭 C ⟶ T and μ : T ⋙ T ⟶ T satisfying three equations:

• T μ_X ≫ μ_X = μ_(TX) ≫ μ_X (associativity)
• η_(TX) ≫ μ_X = 1_X (left unit)
• Tη_X ≫ μ_X = 1_X (right unit)
Instances
@[class]
structure category_theory.comonad {C : Type u₁}  :
C CType (max u₁ v₁)

The data of a comonad on C consists of an endofunctor G together with natural transformations ε : G ⟶ 𝟭 C and δ : G ⟶ G ⋙ G satisfying three equations:

• δ_X ≫ G δ_X = δ_X ≫ δ_(GX) (coassociativity)
• δ_X ≫ ε_(GX) = 1_X (left counit)
• δ_X ≫ G ε_X = 1_X (right counit)
Instances
structure category_theory.monad_hom {C : Type u₁} (M N : C C)  :
Type (max u₁ v₁)

A morphisms of monads is a natural transformation compatible with η and μ.

structure category_theory.comonad_hom {C : Type u₁} (M N : C C)  :
Type (max u₁ v₁)

A morphisms of comonads is a natural transformation compatible with η and μ.

@[ext]
theorem category_theory.monad_hom.ext {C : Type u₁} {M N : C C} (f g : N) :
f = g

def category_theory.monad_hom.id {C : Type u₁} (M : C C)  :

The identity natural transformations is a morphism of monads.

Equations
@[instance]
def category_theory.monad_hom.inhabited {C : Type u₁} {M : C C}  :

Equations
def category_theory.monad_hom.comp {C : Type u₁} {M N L : C C}  :

The composition of two morphisms of monads.

Equations
@[simp]
theorem category_theory.monad_hom.id_comp {C : Type u₁} {M N : C C} (f : N) :

@[simp]
theorem category_theory.monad_hom.comp_id {C : Type u₁} {M N : C C} (f : N) :

@[simp]
theorem category_theory.monad_hom.assoc {C : Type u₁} {M N L K : C C} (f : N) (g : L) (h : K) :
(f.comp g).comp h = f.comp (g.comp h)

Note: category_theory.monad.bundled provides a category instance for bundled monads.

@[ext]
theorem category_theory.comonad_hom.ext {C : Type u₁} {M N : C C} (f g : N) :
f = g

def category_theory.comonad_hom.id {C : Type u₁} (M : C C)  :

The identity natural transformations is a morphism of comonads.

Equations
@[instance]
def category_theory.comonad_hom.inhabited {C : Type u₁} {M : C C}  :

Equations
def category_theory.comonad_hom.comp {C : Type u₁} {M N L : C C}  :

The composition of two morphisms of comonads.

Equations
@[simp]
theorem category_theory.comonad_hom.id_comp {C : Type u₁} {M N : C C} (f : N) :

@[simp]
theorem category_theory.comonad_hom.comp_id {C : Type u₁} {M N : C C} (f : N) :

@[simp]
theorem category_theory.comonad_hom.assoc {C : Type u₁} {M N L K : C C} (f : N) (g : L) (h : K) :
(f.comp g).comp h = f.comp (g.comp h)

Note: category_theory.monad.bundled provides a category instance for bundled comonads.