mathlib documentation

category_theory.monad.basic

@[class]
structure category_theory.monad {C : Type u₁} [category_theory.category C] (T : C 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)
Instances
theorem category_theory.monad.assoc {C : Type u₁} [category_theory.category C] {T : C C} [c : category_theory.monad T] (X : C) :
T.map ((μ_ T).app X) (μ_ T).app X = (μ_ T).app (T.obj X) (μ_ T).app X

@[simp]
theorem category_theory.monad.left_unit {C : Type u₁} [category_theory.category C] {T : C C} [c : category_theory.monad T] (X : C) :
(η_ T).app (T.obj X) (μ_ T).app X = 𝟙 (T.obj X)

@[simp]
theorem category_theory.monad.right_unit {C : Type u₁} [category_theory.category C] {T : C C} [c : category_theory.monad T] (X : C) :
T.map ((η_ T).app X) (μ_ T).app X = 𝟙 (T.obj X)

@[simp]
theorem category_theory.monad.left_unit_assoc {C : Type u₁} [category_theory.category C] {T : C C} [c : category_theory.monad T] (X : C) {X' : C} (f' : T.obj X X') :
(η_ T).app (T.obj X) (μ_ T).app X f' = f'

@[simp]
theorem category_theory.monad.right_unit_assoc {C : Type u₁} [category_theory.category C] {T : C C} [c : category_theory.monad T] (X : C) {X' : C} (f' : T.obj X X') :
T.map ((η_ T).app X) (μ_ T).app X f' = f'

@[class]
structure category_theory.comonad {C : Type u₁} [category_theory.category C] (G : C 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)
Instances
theorem category_theory.comonad.coassoc {C : Type u₁} [category_theory.category C] {G : C C} [c : category_theory.comonad G] (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 {C : Type u₁} [category_theory.category C] {G : C C} [c : category_theory.comonad G] (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 : C C} [c : category_theory.comonad G] (X : C) :
(δ_ G).app X G.map ((ε_ G).app X) = 𝟙 (G.obj X)

@[simp]
theorem category_theory.comonad.left_counit_assoc {C : Type u₁} [category_theory.category C] {G : C C} [c : category_theory.comonad G] (X : C) {X' : C} (f' : G.obj X X') :
(δ_ G).app X (ε_ G).app (G.obj X) f' = f'

@[simp]
theorem category_theory.comonad.right_counit_assoc {C : Type u₁} [category_theory.category C] {G : C C} [c : category_theory.comonad G] (X : C) {X' : C} (f' : G.obj X X') :
(δ_ G).app X G.map ((ε_ G).app X) f' = f'

structure category_theory.monad_hom {C : Type u₁} [category_theory.category C] (M N : C C) [category_theory.monad M] [category_theory.monad N] :
Type (max u₁ v₁)

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

@[simp]

@[simp]
theorem category_theory.monad_hom.app_μ_assoc {C : Type u₁} [category_theory.category C] {M N : C C} [category_theory.monad M] [category_theory.monad N] (c : category_theory.monad_hom M N) {X X' : C} (f' : N.obj X X') :
(μ_ M).app X c.to_nat_trans.app X f' = M.map (c.to_nat_trans.app X) c.to_nat_trans.app (N.obj X) (μ_ N).app X f'

@[simp]
theorem category_theory.monad_hom.app_η_assoc {C : Type u₁} [category_theory.category C] {M N : C C} [category_theory.monad M] [category_theory.monad N] (c : category_theory.monad_hom M N) {X X' : C} (f' : N.obj X X') :
(η_ M).app X c.to_nat_trans.app X f' = (η_ N).app X f'

structure category_theory.comonad_hom {C : Type u₁} [category_theory.category C] (M N : C C) [category_theory.comonad M] [category_theory.comonad N] :
Type (max u₁ v₁)

A morphisms of comonads is a natural transformation compatible with η and μ.

@[simp]
theorem category_theory.comonad_hom.app_δ_assoc {C : Type u₁} [category_theory.category C] {M N : C C} [category_theory.comonad M] [category_theory.comonad N] (c : category_theory.comonad_hom M N) {X X' : C} (f' : N.obj (N.obj X) X') :
c.to_nat_trans.app X (δ_ N).app X f' = (δ_ M).app X c.to_nat_trans.app (M.obj X) N.map (c.to_nat_trans.app X) f'

@[simp]
theorem category_theory.comonad_hom.app_ε_assoc {C : Type u₁} [category_theory.category C] {M N : C C} [category_theory.comonad M] [category_theory.comonad N] (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'

The identity natural transformations is a morphism of monads.

Equations

The composition of two morphisms of monads.

Equations
@[simp]

Note: category_theory.monad.bundled provides a category instance for bundled monads.

The identity natural transformations is a morphism of comonads.

Equations

The composition of two morphisms of comonads.

Equations
@[simp]

Note: category_theory.monad.bundled provides a category instance for bundled comonads.