# mathlibdocumentation

@[class]
structure category_theory.monad {C : Type u₁} (T : C C) :
Type (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
theorem category_theory.monad.assoc {C : Type u₁} {T : C C} [c : category_theory.monad T] (X : C) :
T.map ((μ_ T).app X) (μ_ T).app X = (μ_ T).app (T.obj X) (μ_ T).app X

@[simp]
theorem category_theory.monad.left_unit {C : Type u₁} {T : C C} [c : category_theory.monad T] (X : C) :
(η_ T).app (T.obj X) (μ_ T).app X = 𝟙 (T.obj X)

@[simp]
theorem category_theory.monad.right_unit {C : Type u₁} {T : C C} [c : category_theory.monad T] (X : C) :
T.map ((η_ T).app X) (μ_ T).app X = 𝟙 (T.obj X)

@[simp]
theorem category_theory.monad.left_unit_assoc {C : Type u₁} {T : C C} [c : category_theory.monad T] (X : C) {X' : C} (f' : T.obj X X') :
(η_ T).app (T.obj X) (μ_ T).app X f' = f'

@[simp]
theorem category_theory.monad.right_unit_assoc {C : Type u₁} {T : C C} [c : category_theory.monad T] (X : C) {X' : C} (f' : T.obj X X') :
T.map ((η_ T).app X) (μ_ T).app X f' = f'

@[class]
structure category_theory.comonad {C : Type u₁} (G : C C) :
Type (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
theorem category_theory.comonad.coassoc {C : Type u₁} {G : C C} [c : category_theory.comonad G] (X : C) :
(δ_ G).app X G.map ((δ_ G).app X) = (δ_ G).app X (δ_ G).app (G.obj X)

@[simp]
theorem category_theory.comonad.left_counit {C : Type u₁} {G : C C} [c : category_theory.comonad G] (X : C) :
(δ_ G).app X (ε_ G).app (G.obj X) = 𝟙 (G.obj X)

@[simp]
theorem category_theory.comonad.right_counit {C : Type u₁} {G : C C} [c : category_theory.comonad G] (X : C) :
(δ_ G).app X G.map ((ε_ G).app X) = 𝟙 (G.obj X)

@[simp]
theorem category_theory.comonad.left_counit_assoc {C : Type u₁} {G : C C} [c : category_theory.comonad G] (X : C) {X' : C} (f' : G.obj X X') :
(δ_ G).app X (ε_ G).app (G.obj X) f' = f'

@[simp]
theorem category_theory.comonad.right_counit_assoc {C : Type u₁} {G : C C} [c : category_theory.comonad G] (X : C) {X' : C} (f' : G.obj X X') :
(δ_ G).app X G.map ((ε_ G).app X) f' = f'

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 μ.

@[simp]
theorem category_theory.monad_hom.app_η {C : Type u₁} {M N : C C} (c : N) {X : C} :
(η_ M).app X c.to_nat_trans.app X = (η_ N).app X

@[simp]
theorem category_theory.monad_hom.app_μ {C : Type u₁} {M N : C C} (c : N) {X : C} :
(μ_ M).app X c.to_nat_trans.app X = (M.map (c.to_nat_trans.app X) c.to_nat_trans.app (N.obj X)) (μ_ N).app X

@[simp]
theorem category_theory.monad_hom.app_μ_assoc {C : Type u₁} {M N : C C} (c : N) {X X' : C} (f' : N.obj X X') :
(μ_ M).app X c.to_nat_trans.app X f' = M.map (c.to_nat_trans.app X) c.to_nat_trans.app (N.obj X) (μ_ N).app X f'

@[simp]
theorem category_theory.monad_hom.app_η_assoc {C : Type u₁} {M N : C C} (c : N) {X X' : C} (f' : N.obj X X') :
(η_ M).app X c.to_nat_trans.app X f' = (η_ N).app X f'

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 μ.

@[simp]
theorem category_theory.comonad_hom.app_ε {C : Type u₁} {M N : C C} (c : N) {X : C} :
c.to_nat_trans.app X (ε_ N).app X = (ε_ M).app X

@[simp]
theorem category_theory.comonad_hom.app_δ {C : Type u₁} {M N : C C} (c : N) {X : C} :

@[simp]
theorem category_theory.comonad_hom.app_δ_assoc {C : Type u₁} {M N : C C} (c : N) {X X' : C} (f' : N.obj (N.obj X) X') :
c.to_nat_trans.app X (δ_ N).app X f' = (δ_ M).app X c.to_nat_trans.app (M.obj X) N.map (c.to_nat_trans.app X) f'

@[simp]
theorem category_theory.comonad_hom.app_ε_assoc {C : Type u₁} {M N : C C} (c : N) {X X' : C} (f' : X X') :
c.to_nat_trans.app X (ε_ N).app X f' = (ε_ M).app X f'

@[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} (f : N) (g : L) :

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} (f : N) (g : L) :

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.