# mathlibdocumentation

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
def category_theory.monad.η {C : Type u₁} (T : category_theory.monad C) :

The unit for the monad T.

Equations
def category_theory.monad.μ {C : Type u₁} (T : category_theory.monad C) :

The multiplication for the monad T.

Equations
Instances for category_theory.monad.μ
def category_theory.comonad.ε {C : Type u₁} (G : category_theory.comonad C) :

The counit for the comonad G.

Equations

The comultiplication for the comonad G.

Equations
def category_theory.monad.simps.coe {C : Type u₁} (T : category_theory.monad C) :
C C

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]
def category_theory.monad.category {C : Type u₁}  :
Equations
@[protected, instance]
def category_theory.comonad.category {C : Type u₁}  :
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)) :
@[simp]
theorem category_theory.monad_to_functor_obj (C : Type u₁) (T : category_theory.monad C) :
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]
@[simp]
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) :
def category_theory.comonad_to_functor (C : Type u₁)  :

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

Equations
Instances for category_theory.comonad_to_functor
@[simp]
@[protected, instance]
@[simp]
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) :
def category_theory.monad_iso.to_nat_iso {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]
theorem category_theory.comonad_iso.to_nat_iso_hom {C : Type u₁} {M N : category_theory.comonad C} (h : M N) :
@[simp]
theorem category_theory.comonad_iso.to_nat_iso_inv {C : Type u₁} {M N : category_theory.comonad C} (h : M N) :
def category_theory.comonad_iso.to_nat_iso {C : Type u₁} {M N : category_theory.comonad C} (h : M N) :

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]
def category_theory.monad.inhabited (C : Type u₁)  :
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)
def category_theory.comonad.id (C : Type u₁)  :