mathlib docs: category_theory.monad.basic

@[class]

structure category_theory.monad {C : Type u₁} [category_theory.category C] (T : 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

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

source

@[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)

source

@[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)

source

@[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'

source

@[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'

source

@[class]

structure category_theory.comonad {C : Type u₁} [category_theory.category C] (G : 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

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)

source

@[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)

source

@[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)

source

@[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'

source

@[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'

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

@[simp]

theorem category_theory.monad_hom.app_η {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 : C} :

(η_ M).app X ≫ c.to_nat_trans.app X = (η_ N).app X

source

@[simp]

theorem category_theory.monad_hom.app_μ {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 : 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

source

@[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'

source

@[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'

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

@[simp]

theorem category_theory.comonad_hom.app_ε {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 : C} :

c.to_nat_trans.app X ≫ (ε_ N).app X = (ε_ M).app X

source

@[simp]

theorem category_theory.comonad_hom.app_δ {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 : 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)

source

@[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'

source

@[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'

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] (f : category_theory.monad_hom M N) (g : 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] (f : category_theory.comonad_hom M N) (g : 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.functor.id.monad {C : Type u₁} [category_theory.category C] :

category_theory.monad (𝟭 C)

Equations

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

source

@[instance]

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

category_theory.comonad (𝟭 C)

Equations

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