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 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 X' : C} (f' : T₂.obj X X') :
T₁.η.app X c.to_nat_trans.app X f' = T₂.η.app X f'
@[simp]
@[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 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₃) :

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

Equations

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

Equations

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