mathlib documentation

category_theory.monad.basic

structure category_theory.monad (C : Type u₁) [category_theory.category 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)
structure category_theory.comonad (C : Type u₁) [category_theory.category 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)
@[protected, instance]
Equations

The unit for the monad T.

Equations

The multiplication for the monad T.

Equations

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₁} [category_theory.category C] (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₁} [category_theory.category C] (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₁} [category_theory.category C] (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₁} [category_theory.category C] (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₁} [category_theory.category C] (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₁} [category_theory.category C] (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₁} [category_theory.category C] (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₁} [category_theory.category C] (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₁} [category_theory.category C] (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₁} [category_theory.category C] (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₁} [category_theory.category C] (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₁} [category_theory.category C] (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 : category_theory.monad_hom T₁ T₂) (h : x.to_nat_trans = y.to_nat_trans) :
x = y
@[ext]
structure category_theory.monad_hom {C : Type u₁} [category_theory.category C] (T₁ T₂ : category_theory.monad C) :
Type (max u₁ v₁)

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

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

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

@[simp]
theorem category_theory.monad_hom.app_η {C : Type u₁} [category_theory.category C] {T₁ T₂ : category_theory.monad C} (self : category_theory.monad_hom T₁ 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₁} [category_theory.category C] {T₁ T₂ : category_theory.monad C} (self : category_theory.monad_hom T₁ 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₁} [category_theory.category C] {T₁ T₂ : category_theory.monad C} (self : category_theory.monad_hom T₁ 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₁} [category_theory.category C] {T₁ T₂ : category_theory.monad C} (self : category_theory.monad_hom T₁ 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]
@[simp]
@[simp]
theorem category_theory.comonad_hom.app_δ_assoc {C : Type u₁} [category_theory.category C] {M N : category_theory.comonad C} (self : category_theory.comonad_hom M 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₁} [category_theory.category C] {M N : category_theory.comonad C} (self : category_theory.comonad_hom M 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
@[simp]
theorem category_theory.monad_hom.comp_to_nat_trans {C : Type u₁} [category_theory.category C] {T₁ T₂ T₃ : category_theory.monad C} (f : T₁ T₂) (g : T₂ T₃) :
@[simp]
theorem category_theory.comp_to_nat_trans {C : Type u₁} [category_theory.category C] {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₁} [category_theory.category C] {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₁} [category_theory.category C] {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₁} [category_theory.category C] {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₁} [category_theory.category C] {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₁} [category_theory.category C] {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₁} [category_theory.category C] {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)) :

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

Equations
@[simp]
theorem category_theory.monad_to_functor_map_iso_monad_iso_mk (C : Type u₁) [category_theory.category C] {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) :

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

Equations
@[simp]
theorem category_theory.comonad_to_functor_map_iso_comonad_iso_mk (C : Type u₁) [category_theory.category C] {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)) :

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

Equations

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

Equations

The identity monad.

Equations

The identity comonad.

Equations