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)

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} (c : category_theory.monad_hom T₁ T₂) (X : C) :
T₁.η.app X c.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} (c : category_theory.monad_hom T₁ T₂) (X : C) :
T₁.μ.app X c.to_nat_trans.app X = (T₁.map (c.to_nat_trans.app X) c.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} (c : category_theory.monad_hom T₁ T₂) (X : C) {X' : C} (f' : T₂.obj X X') :
T₁.μ.app X c.to_nat_trans.app X f' = T₁.map (c.to_nat_trans.app X) c.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} (c : category_theory.monad_hom T₁ T₂) (X : C) {X' : C} (f' : T₂.obj X X') :
T₁.η.app X c.to_nat_trans.app X f' = T₂.η.app X f'
@[simp]
theorem category_theory.comonad_hom.app_δ_assoc {C : Type u₁} [category_theory.category C] {M N : category_theory.comonad C} (c : category_theory.comonad_hom M N) (X : C) {X' : C} (f' : N.obj (N.obj X) X') :
@[simp]
theorem category_theory.comonad_hom.app_ε_assoc {C : Type u₁} [category_theory.category C] {M N : category_theory.comonad C} (c : category_theory.comonad_hom M N) (X : C) {X' : C} (f' : X X') :
c.to_nat_trans.app X N.ε.app X f' = M.ε.app X f'
@[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