# mathlib3documentation

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

We construct the categories of monads and comonads, and their forgetful functors to endofunctors.

(Note that these are the category theorist's monads, not the programmers monads. For the translation, see the file category_theory.monad.types.)

For the fact that monads are "just" monoids in the category of endofunctors, see the file category_theory.monad.equiv_mon.

structure category_theory.monad (C : Type u₁)  :
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 for category_theory.monad
structure category_theory.comonad (C : Type u₁)  :
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 for category_theory.comonad
@[protected, instance]
def category_theory.coe_monad {C : Type u₁}  :
(C C)
Equations
@[protected, instance]
def category_theory.coe_comonad {C : Type u₁}  :
(C C)
Equations

The unit for the monad T.

Equations

The multiplication for the monad T.

Equations
Instances for category_theory.monad.μ

The counit for the comonad G.

Equations

The comultiplication for the comonad G.

Equations

A custom simps projection for the functor part of a monad, as a coercion.

Equations

A custom simps projection for the unit of a monad, in simp normal form.

Equations

A custom simps projection for the multiplication of a monad, in simp normal form.

Equations

A custom simps projection for the functor part of a comonad, as a coercion.

Equations

A custom simps projection for the counit of a comonad, in simp normal form.

Equations

A custom simps projection for the comultiplication of a comonad, in simp normal form.

Equations
theorem category_theory.monad.assoc {C : Type u₁} (T : category_theory.monad C) (X : C) :
T.map (T.μ.app X) T.μ.app X = T.μ.app (T.obj X) T.μ.app X
theorem category_theory.monad.assoc_assoc {C : Type u₁} (T : category_theory.monad C) (X : C) {X' : C} (f' : T.obj X X') :
T.map (T.μ.app X) T.μ.app X f' = T.μ.app (T.obj X) T.μ.app X f'
@[simp]
theorem category_theory.monad.left_unit_assoc {C : Type u₁} (T : category_theory.monad C) (X : C) {X' : C} (f' : T.obj X X') :
T.η.app (T.obj X) T.μ.app X f' = f'
@[simp]
theorem category_theory.monad.left_unit {C : Type u₁} (T : category_theory.monad C) (X : C) :
T.η.app (T.obj X) T.μ.app X = 𝟙 (T.obj X)
@[simp]
theorem category_theory.monad.right_unit_assoc {C : Type u₁} (T : category_theory.monad C) (X : C) {X' : C} (f' : T.obj X X') :
T.map (T.η.app X) T.μ.app X f' = f'
@[simp]
theorem category_theory.monad.right_unit {C : Type u₁} (T : category_theory.monad C) (X : C) :
T.map (T.η.app X) T.μ.app X = 𝟙 (T.obj X)
theorem category_theory.comonad.coassoc_assoc {C : Type u₁} (G : category_theory.comonad C) (X : C) {X' : C} (f' : G.obj ((G G).obj X) X') :
G.δ.app X G.map (G.δ.app X) f' = G.δ.app X G.δ.app (G.obj X) f'
theorem category_theory.comonad.coassoc {C : Type u₁} (G : category_theory.comonad C) (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_assoc {C : Type u₁} (G : category_theory.comonad C) (X : C) {X' : C} (f' : (𝟭 C).obj (G.obj X) X') :
G.δ.app X G.ε.app (G.obj X) f' = f'
@[simp]
theorem category_theory.comonad.left_counit {C : Type u₁} (G : category_theory.comonad C) (X : C) :
G.δ.app X G.ε.app (G.obj X) = 𝟙 (G.obj X)
@[simp]
theorem category_theory.comonad.right_counit {C : Type u₁} (G : category_theory.comonad C) (X : C) :
G.δ.app X G.map (G.ε.app X) = 𝟙 (G.obj X)
@[simp]
theorem category_theory.comonad.right_counit_assoc {C : Type u₁} (G : category_theory.comonad C) (X : C) {X' : C} (f' : G.obj ((𝟭 C).obj X) X') :
G.δ.app X G.map (G.ε.app X) f' = f'
theorem category_theory.monad_hom.ext {C : Type u₁} {_inst_1 : category_theory.category C} {T₁ T₂ : category_theory.monad C} (x y : T₂) (h : x.to_nat_trans = y.to_nat_trans) :
x = y
@[ext]
structure category_theory.monad_hom {C : Type u₁} (T₁ T₂ : category_theory.monad C) :
Type (max u₁ v₁)

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

Instances for category_theory.monad_hom
theorem category_theory.monad_hom.ext_iff {C : Type u₁} {_inst_1 : category_theory.category C} {T₁ T₂ : category_theory.monad C} (x y : T₂) :
x = y
theorem category_theory.comonad_hom.ext_iff {C : Type u₁} {_inst_1 : category_theory.category C} {M N : category_theory.comonad C} (x y : N) :
x = y
theorem category_theory.comonad_hom.ext {C : Type u₁} {_inst_1 : category_theory.category C} {M N : category_theory.comonad C} (x y : N) (h : x.to_nat_trans = y.to_nat_trans) :
x = y
@[ext]
structure category_theory.comonad_hom {C : Type u₁} (M N : category_theory.comonad C) :
Type (max u₁ v₁)

A morphism of comonads is a natural transformation compatible with ε and δ.

Instances for category_theory.comonad_hom
@[simp]
theorem category_theory.monad_hom.app_η {C : Type u₁} {T₁ T₂ : category_theory.monad C} (self : T₂) (X : C) :
T₁.η.app X self.to_nat_trans.app X = T₂.η.app X
@[simp]
theorem category_theory.monad_hom.app_μ {C : Type u₁} {T₁ T₂ : category_theory.monad C} (self : T₂) (X : C) :
T₁.μ.app X self.to_nat_trans.app X = (T₁.map (self.to_nat_trans.app X) self.to_nat_trans.app (T₂.obj X)) T₂.μ.app X
@[simp]
theorem category_theory.monad_hom.app_μ_assoc {C : Type u₁} {T₁ T₂ : category_theory.monad C} (self : T₂) (X : C) {X' : C} (f' : T₂.obj X X') :
T₁.μ.app X self.to_nat_trans.app X f' = T₁.map (self.to_nat_trans.app X) self.to_nat_trans.app (T₂.obj X) T₂.μ.app X f'
@[simp]
theorem category_theory.monad_hom.app_η_assoc {C : Type u₁} {T₁ T₂ : category_theory.monad C} (self : T₂) (X : C) {X' : C} (f' : T₂.obj X X') :
T₁.η.app X self.to_nat_trans.app X f' = T₂.η.app X f'
@[simp]
theorem category_theory.comonad_hom.app_ε {C : Type u₁} {M N : category_theory.comonad C} (self : N) (X : C) :
self.to_nat_trans.app X N.ε.app X = M.ε.app X
@[simp]
theorem category_theory.comonad_hom.app_δ {C : Type u₁} {M N : category_theory.comonad C} (self : N) (X : C) :
self.to_nat_trans.app X N.δ.app X = M.δ.app X self.to_nat_trans.app (M.obj X) N.map (self.to_nat_trans.app X)
@[simp]
theorem category_theory.comonad_hom.app_δ_assoc {C : Type u₁} {M N : category_theory.comonad C} (self : N) (X : C) {X' : C} (f' : N.obj (N.obj X) X') :
self.to_nat_trans.app X N.δ.app X f' = M.δ.app X self.to_nat_trans.app (M.obj X) N.map (self.to_nat_trans.app X) f'
@[simp]
theorem category_theory.comonad_hom.app_ε_assoc {C : Type u₁} {M N : category_theory.comonad C} (self : N) (X : C) {X' : C} (f' : X X') :
self.to_nat_trans.app X N.ε.app X f' = M.ε.app X f'
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem category_theory.monad_hom.comp_to_nat_trans {C : Type u₁} {T₁ T₂ T₃ : category_theory.monad C} (f : T₁ T₂) (g : T₂ T₃) :
@[protected, instance]
Equations
@[simp]
theorem category_theory.comp_to_nat_trans {C : Type u₁} {T₁ T₂ T₃ : category_theory.comonad C} (f : T₁ T₂) (g : T₂ T₃) :
@[simp]
theorem category_theory.monad_iso.mk_inv_to_nat_trans {C : Type u₁} {M N : category_theory.monad C} (f : M N) (f_η : (X : C), M.η.app X f.hom.app X = N.η.app X) (f_μ : (X : C), M.μ.app X f.hom.app X = (M.map (f.hom.app X) f.hom.app (N.obj X)) N.μ.app X) :
@[simp]
theorem category_theory.monad_iso.mk_hom_to_nat_trans {C : Type u₁} {M N : category_theory.monad C} (f : M N) (f_η : (X : C), M.η.app X f.hom.app X = N.η.app X) (f_μ : (X : C), M.μ.app X f.hom.app X = (M.map (f.hom.app X) f.hom.app (N.obj X)) N.μ.app X) :
def category_theory.monad_iso.mk {C : Type u₁} {M N : category_theory.monad C} (f : M N) (f_η : (X : C), M.η.app X f.hom.app X = N.η.app X) (f_μ : (X : C), M.μ.app X f.hom.app X = (M.map (f.hom.app X) f.hom.app (N.obj X)) N.μ.app X) :
M N

Construct a monad isomorphism from a natural isomorphism of functors where the forward direction is a monad morphism.

Equations
def category_theory.comonad_iso.mk {C : Type u₁} {M N : category_theory.comonad C} (f : M N) (f_ε : (X : C), f.hom.app X N.ε.app X = M.ε.app X) (f_δ : (X : C), f.hom.app X N.δ.app X = M.δ.app X f.hom.app (M.obj X) N.map (f.hom.app X)) :
M N

Construct a comonad isomorphism from a natural isomorphism of functors where the forward direction is a comonad morphism.

Equations
@[simp]
theorem category_theory.comonad_iso.mk_hom_to_nat_trans {C : Type u₁} {M N : category_theory.comonad C} (f : M N) (f_ε : (X : C), f.hom.app X N.ε.app X = M.ε.app X) (f_δ : (X : C), f.hom.app X N.δ.app X = M.δ.app X f.hom.app (M.obj X) N.map (f.hom.app X)) :
@[simp]
theorem category_theory.comonad_iso.mk_inv_to_nat_trans {C : Type u₁} {M N : category_theory.comonad C} (f : M N) (f_ε : (X : C), f.hom.app X N.ε.app X = M.ε.app X) (f_δ : (X : C), f.hom.app X N.δ.app X = M.δ.app X f.hom.app (M.obj X) N.map (f.hom.app X)) :
def category_theory.monad_to_functor (C : Type u₁)  :
C C

The forgetful functor from the category of monads to the category of endofunctors.

Equations
Instances for category_theory.monad_to_functor
@[simp]
theorem category_theory.monad_to_functor_map (C : Type u₁) (M N : category_theory.monad C) (f : M N) :
@[protected, instance]
theorem category_theory.monad_to_functor_map_iso_monad_iso_mk (C : Type u₁) {M N : category_theory.monad C} (f : M N) (f_η : (X : C), M.η.app X f.hom.app X = N.η.app X) (f_μ : (X : C), M.μ.app X f.hom.app X = (M.map (f.hom.app X) f.hom.app (N.obj X)) N.μ.app X) :
f_μ) = f
@[protected, instance]
@[simp]
theorem category_theory.comonad_to_functor_map (C : Type u₁) (M N : category_theory.comonad C) (f : M N) :

The forgetful functor from the category of comonads to the category of endofunctors.

Equations
Instances for category_theory.comonad_to_functor
@[protected, instance]
theorem category_theory.comonad_to_functor_map_iso_comonad_iso_mk (C : Type u₁) {M N : category_theory.comonad C} (f : M N) (f_ε : (X : C), f.hom.app X N.ε.app X = M.ε.app X) (f_δ : (X : C), f.hom.app X N.δ.app X = M.δ.app X f.hom.app (M.obj X) N.map (f.hom.app X)) :
= f
@[protected, instance]
@[simp]
theorem category_theory.monad_iso.to_nat_iso_hom {C : Type u₁} {M N : category_theory.monad C} (h : M N) :
@[simp]
theorem category_theory.monad_iso.to_nat_iso_inv {C : Type u₁} {M N : category_theory.monad C} (h : M N) :

An isomorphism of monads gives a natural isomorphism of the underlying functors.

Equations
@[simp]
@[simp]

An isomorphism of comonads gives a natural isomorphism of the underlying functors.

Equations
def category_theory.monad.id (C : Type u₁)  :

Equations
@[simp]
theorem category_theory.monad.id_μ (C : Type u₁)  :
= 𝟙 (𝟭 C)
@[simp]
theorem category_theory.monad.id_η (C : Type u₁)  :
= 𝟙 (𝟭 C)
@[simp]
theorem category_theory.monad.id_coe (C : Type u₁)  :
@[protected, instance]
Equations
@[simp]
theorem category_theory.comonad.id_δ (C : Type u₁)  :
= 𝟙 (𝟭 C)
@[simp]
theorem category_theory.comonad.id_coe (C : Type u₁)  :
@[simp]
theorem category_theory.comonad.id_ε (C : Type u₁)  :
= 𝟙 (𝟭 C)