mathlib docs: category_theory.monad.basic

@[class]

structure category_theory.monad {C : Type u₁} [category_theory.category C] :

C ⥤ C → Type (max u₁ v₁)

η : 𝟭 C ⟶ T
μ : T ⋙ T ⟶ T
assoc' : (∀ (X : C), T.map ((μ_ T).app X) ≫ (μ_ T).app X = (μ_ T).app (T.obj X) ≫ (μ_ T).app X) . "obviously"
left_unit' : (∀ (X : C), (η_ T).app (T.obj X) ≫ (μ_ T).app X = 𝟙 ((𝟭 C).obj (T.obj X))) . "obviously"
right_unit' : (∀ (X : C), T.map ((η_ T).app X) ≫ (μ_ T).app X = 𝟙 (T.obj ((𝟭 C).obj X))) . "obviously"

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

source

@[class]

structure category_theory.comonad {C : Type u₁} [category_theory.category C] :

C ⥤ C → Type (max u₁ v₁)

ε : G ⟶ 𝟭 C
δ : G ⟶ G ⋙ G
coassoc' : (∀ (X : C), (δ_ G).app X ≫ G.map ((δ_ G).app X) = (δ_ G).app X ≫ (δ_ G).app (G.obj X)) . "obviously"
left_counit' : (∀ (X : C), (δ_ G).app X ≫ (ε_ G).app (G.obj X) = 𝟙 (G.obj X)) . "obviously"
right_counit' : (∀ (X : C), (δ_ G).app X ≫ G.map ((ε_ G).app X) = 𝟙 (G.obj X)) . "obviously"

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

source

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₁)

to_nat_trans : category_theory.nat_trans M N
app_η' : (∀ {X : C}, (η_ M).app X ≫ c.to_nat_trans.app X = (η_ N).app X) . "obviously"
app_μ' : (∀ {X : C}, (μ_ M).app X ≫ c.to_nat_trans.app X = (M.map (c.to_nat_trans.app X) ≫ c.to_nat_trans.app (N.obj X)) ≫ (μ_ N).app X) . "obviously"

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

source

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₁)

to_nat_trans : category_theory.nat_trans M N
app_ε' : (∀ {X : C}, c.to_nat_trans.app X ≫ (ε_ N).app X = (ε_ M).app X) . "obviously"
app_δ' : (∀ {X : C}, c.to_nat_trans.app X ≫ (δ_ N).app X = (δ_ M).app X ≫ c.to_nat_trans.app (M.obj X) ≫ N.map (c.to_nat_trans.app X)) . "obviously"

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

source

@[ext]

theorem category_theory.monad_hom.ext {C : Type u₁} [category_theory.category C] {M N : C ⥤ C} [category_theory.monad M] [category_theory.monad N] (f g : category_theory.monad_hom M N) :

f.to_nat_trans = g.to_nat_trans → f = g

source

def category_theory.monad_hom.id {C : Type u₁} [category_theory.category C] (M : C ⥤ C) [category_theory.monad M] :

category_theory.monad_hom M M

The identity natural transformations is a morphism of monads.

Equations

category_theory.monad_hom.id M = {to_nat_trans := {app := (𝟙 M).app, naturality' := _}, app_η' := _, app_μ' := _}

source

@[instance]

def category_theory.monad_hom.inhabited {C : Type u₁} [category_theory.category C] {M : C ⥤ C} [category_theory.monad M] :

inhabited (category_theory.monad_hom M M)

Equations

category_theory.monad_hom.inhabited = {default := category_theory.monad_hom.id M _inst_2}

source

def category_theory.monad_hom.comp {C : Type u₁} [category_theory.category C] {M N L : C ⥤ C} [category_theory.monad M] [category_theory.monad N] [category_theory.monad L] :

category_theory.monad_hom M N → category_theory.monad_hom N L → category_theory.monad_hom M L

The composition of two morphisms of monads.

Equations

f.comp g = {to_nat_trans := {app := λ (X : C), f.to_nat_trans.app X ≫ g.to_nat_trans.app X, naturality' := _}, app_η' := _, app_μ' := _}

source

@[simp]

theorem category_theory.monad_hom.id_comp {C : Type u₁} [category_theory.category C] {M N : C ⥤ C} [category_theory.monad M] [category_theory.monad N] (f : category_theory.monad_hom M N) :

(category_theory.monad_hom.id M).comp f = f

source

@[simp]

theorem category_theory.monad_hom.comp_id {C : Type u₁} [category_theory.category C] {M N : C ⥤ C} [category_theory.monad M] [category_theory.monad N] (f : category_theory.monad_hom M N) :

f.comp (category_theory.monad_hom.id N) = f

source

@[simp]

theorem category_theory.monad_hom.assoc {C : Type u₁} [category_theory.category C] {M N L K : C ⥤ C} [category_theory.monad M] [category_theory.monad N] [category_theory.monad L] [category_theory.monad K] (f : category_theory.monad_hom M N) (g : category_theory.monad_hom N L) (h : category_theory.monad_hom L K) :

(f.comp g).comp h = f.comp (g.comp h)

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

source

@[ext]

theorem category_theory.comonad_hom.ext {C : Type u₁} [category_theory.category C] {M N : C ⥤ C} [category_theory.comonad M] [category_theory.comonad N] (f g : category_theory.comonad_hom M N) :

f.to_nat_trans = g.to_nat_trans → f = g

source

def category_theory.comonad_hom.id {C : Type u₁} [category_theory.category C] (M : C ⥤ C) [category_theory.comonad M] :

category_theory.comonad_hom M M

The identity natural transformations is a morphism of comonads.

Equations

category_theory.comonad_hom.id M = {to_nat_trans := {app := (𝟙 M).app, naturality' := _}, app_ε' := _, app_δ' := _}

source

@[instance]

def category_theory.comonad_hom.inhabited {C : Type u₁} [category_theory.category C] {M : C ⥤ C} [category_theory.comonad M] :

inhabited (category_theory.comonad_hom M M)

Equations

category_theory.comonad_hom.inhabited = {default := category_theory.comonad_hom.id M _inst_2}

source

def category_theory.comonad_hom.comp {C : Type u₁} [category_theory.category C] {M N L : C ⥤ C} [category_theory.comonad M] [category_theory.comonad N] [category_theory.comonad L] :

category_theory.comonad_hom M N → category_theory.comonad_hom N L → category_theory.comonad_hom M L

The composition of two morphisms of comonads.

Equations

f.comp g = {to_nat_trans := {app := λ (X : C), f.to_nat_trans.app X ≫ g.to_nat_trans.app X, naturality' := _}, app_ε' := _, app_δ' := _}

source

@[simp]

theorem category_theory.comonad_hom.id_comp {C : Type u₁} [category_theory.category C] {M N : C ⥤ C} [category_theory.comonad M] [category_theory.comonad N] (f : category_theory.comonad_hom M N) :

(category_theory.comonad_hom.id M).comp f = f

source

@[simp]

theorem category_theory.comonad_hom.comp_id {C : Type u₁} [category_theory.category C] {M N : C ⥤ C} [category_theory.comonad M] [category_theory.comonad N] (f : category_theory.comonad_hom M N) :

f.comp (category_theory.comonad_hom.id N) = f

source

@[simp]

theorem category_theory.comonad_hom.assoc {C : Type u₁} [category_theory.category C] {M N L K : C ⥤ C} [category_theory.comonad M] [category_theory.comonad N] [category_theory.comonad L] [category_theory.comonad K] (f : category_theory.comonad_hom M N) (g : category_theory.comonad_hom N L) (h : category_theory.comonad_hom L K) :

(f.comp g).comp h = f.comp (g.comp h)

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

source

@[instance]

def category_theory.monad.category_theory.monad {C : Type u₁} [category_theory.category C] :

category_theory.monad (𝟭 C)

Equations

category_theory.monad.category_theory.monad = {η := 𝟙 (𝟭 C), μ := 𝟙 (𝟭 C ⋙ 𝟭 C), assoc' := _, left_unit' := _, right_unit' := _}

source

@[instance]

def category_theory.comonad.category_theory.comonad {C : Type u₁} [category_theory.category C] :

category_theory.comonad (𝟭 C)

Equations

category_theory.comonad.category_theory.comonad = {ε := 𝟙 (𝟭 C), δ := 𝟙 (𝟭 C), coassoc' := _, left_counit' := _, right_counit' := _}