category_theory.monad.basic

structure category_theory.monad (C : Type u₁) [category_theory.category C] :

Type (max u₁ v₁)

to_functor : C ⥤ C
η' : 𝟭 C ⟶ c.to_functor
μ' : c.to_functor ⋙ c.to_functor ⟶ c.to_functor
assoc' : (∀ (X : C), c.to_functor.map (c.μ'.app X) ≫ c.μ'.app X = c.μ'.app (c.to_functor.obj X) ≫ c.μ'.app X) . "obviously"
left_unit' : (∀ (X : C), c.η'.app (c.to_functor.obj X) ≫ c.μ'.app X = 𝟙 ((𝟭 C).obj (c.to_functor.obj X))) . "obviously"
right_unit' : (∀ (X : C), c.to_functor.map (c.η'.app X) ≫ c.μ'.app X = 𝟙 (c.to_functor.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)

source

structure category_theory.comonad (C : Type u₁) [category_theory.category C] :

Type (max u₁ v₁)

to_functor : C ⥤ C
ε' : c.to_functor ⟶ 𝟭 C
δ' : c.to_functor ⟶ c.to_functor ⋙ c.to_functor
coassoc' : (∀ (X : C), c.δ'.app X ≫ c.to_functor.map (c.δ'.app X) = c.δ'.app X ≫ c.δ'.app (c.to_functor.obj X)) . "obviously"
left_counit' : (∀ (X : C), c.δ'.app X ≫ c.ε'.app (c.to_functor.obj X) = 𝟙 (c.to_functor.obj X)) . "obviously"
right_counit' : (∀ (X : C), c.δ'.app X ≫ c.to_functor.map (c.ε'.app X) = 𝟙 (c.to_functor.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)

source

@[instance]

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

has_coe (category_theory.monad C) (C ⥤ C)

Equations

category_theory.coe_monad = {coe := λ (T : category_theory.monad C), T.to_functor}

source

@[instance]

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

has_coe (category_theory.comonad C) (C ⥤ C)

Equations

category_theory.coe_comonad = {coe := λ (G : category_theory.comonad C), G.to_functor}

source

@[simp]

theorem category_theory.monad_to_functor_eq_coe {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) :

T.to_functor = ↑T

source

@[simp]

theorem category_theory.comonad_to_functor_eq_coe {C : Type u₁} [category_theory.category C] (G : category_theory.comonad C) :

G.to_functor = ↑G

source

def category_theory.monad.η {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) :

𝟭 C ⟶ ↑T

The unit for the monad T.

Equations

T.η = T.η'

source

def category_theory.monad.μ {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) :

↑T ⋙ ↑T ⟶ ↑T

The multiplication for the monad T.

Equations

T.μ = T.μ'

source

def category_theory.comonad.ε {C : Type u₁} [category_theory.category C] (G : category_theory.comonad C) :

↑G ⟶ 𝟭 C

The counit for the comonad G.

Equations

G.ε = G.ε'

source

def category_theory.comonad.δ {C : Type u₁} [category_theory.category C] (G : category_theory.comonad C) :

↑G ⟶ ↑G ⋙ ↑G

The comultiplication for the comonad G.

Equations

G.δ = G.δ'

source

def category_theory.monad.simps.coe {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) :

C ⥤ C

A custom simps projection for the functor part of a monad, as a coercion.

Equations

category_theory.monad.simps.coe T = ↑T

source

def category_theory.monad.simps.η {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) :

𝟭 C ⟶ ↑T

A custom simps projection for the unit of a monad, in simp normal form.

Equations

category_theory.monad.simps.η T = T.η

source

def category_theory.monad.simps.μ {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) :

↑T ⋙ ↑T ⟶ ↑T

A custom simps projection for the multiplication of a monad, in simp normal form.

Equations

category_theory.monad.simps.μ T = T.μ

source

def category_theory.comonad.simps.coe {C : Type u₁} [category_theory.category C] (G : category_theory.comonad C) :

C ⥤ C

A custom simps projection for the functor part of a comonad, as a coercion.

Equations

category_theory.comonad.simps.coe G = ↑G

source

def category_theory.comonad.simps.ε {C : Type u₁} [category_theory.category C] (G : category_theory.comonad C) :

↑G ⟶ 𝟭 C

A custom simps projection for the counit of a comonad, in simp normal form.

Equations

category_theory.comonad.simps.ε G = G.ε

source

def category_theory.comonad.simps.δ {C : Type u₁} [category_theory.category C] (G : category_theory.comonad C) :

↑G ⟶ ↑G ⋙ ↑G

A custom simps projection for the comultiplication of a comonad, in simp normal form.

Equations

category_theory.comonad.simps.δ G = G.δ

source

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

source

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'

source

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

source

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

source

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

source

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

source

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'

source

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)

source

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

source

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

source

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

source

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

source

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

source

@[ext]

structure category_theory.monad_hom {C : Type u₁} [category_theory.category C] (T₁ T₂ : category_theory.monad C) :

Type (max u₁ v₁)

to_nat_trans : category_theory.nat_trans ↑T₁ ↑T₂
app_η' : (∀ {X : C}, T₁.η.app X ≫ c.to_nat_trans.app X = T₂.η.app X) . "obviously"
app_μ' : (∀ {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) . "obviously"

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

source

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₂) :

x = y ↔ x.to_nat_trans = y.to_nat_trans

source

theorem category_theory.comonad_hom.ext_iff {C : Type u₁} {_inst_1 : category_theory.category C} {M N : category_theory.comonad C} (x y : category_theory.comonad_hom M N) :

x = y ↔ x.to_nat_trans = y.to_nat_trans

source

theorem category_theory.comonad_hom.ext {C : Type u₁} {_inst_1 : category_theory.category C} {M N : category_theory.comonad C} (x y : category_theory.comonad_hom M N) (h : x.to_nat_trans = y.to_nat_trans) :

x = y

source

@[ext]

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

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.to_functor.obj X) ≫ N.to_functor.map (c.to_nat_trans.app X)) . "obviously"

A morphism of comonads is a natural transformation compatible with ε and δ.

source

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

source

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

source

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

source

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

source

@[simp]

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

source

@[instance]

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

category_theory.category (category_theory.monad C)

Equations

category_theory.monad.category = {to_category_struct := {to_has_hom := {hom := category_theory.monad_hom _inst_1}, id := λ (M : category_theory.monad C), {to_nat_trans := 𝟙 ↑M, app_η' := _, app_μ' := _}, comp := λ (_x _x_1 _x_2 : category_theory.monad C) (f : _x ⟶ _x_1) (g : _x_1 ⟶ _x_2), {to_nat_trans := {app := λ (X : C), f.to_nat_trans.app X ≫ g.to_nat_trans.app X, naturality' := _}, app_η' := _, app_μ' := _}}, id_comp' := _, comp_id' := _, assoc' := _}

source

@[instance]

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

category_theory.category (category_theory.comonad C)

Equations

category_theory.comonad.category = {to_category_struct := {to_has_hom := {hom := category_theory.comonad_hom _inst_1}, id := λ (M : category_theory.comonad C), {to_nat_trans := 𝟙 ↑M, app_ε' := _, app_δ' := _}, comp := λ (M N L : category_theory.comonad C) (f : M ⟶ N) (g : N ⟶ L), {to_nat_trans := {app := λ (X : C), f.to_nat_trans.app X ≫ g.to_nat_trans.app X, naturality' := _}, app_ε' := _, app_δ' := _}}, id_comp' := _, comp_id' := _, assoc' := _}

source

@[instance]

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

inhabited (category_theory.monad_hom T T)

Equations

category_theory.monad_hom.inhabited = {default := 𝟙 T}

source

@[simp]

theorem category_theory.monad_hom.id_to_nat_trans {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) :

(𝟙 T).to_nat_trans = 𝟙 ↑T

source

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

(f ≫ g).to_nat_trans = f.to_nat_trans ≫ g.to_nat_trans

source

@[instance]

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

inhabited (category_theory.comonad_hom G G)

Equations

category_theory.comonad_hom.inhabited = {default := 𝟙 G}

source

@[simp]

theorem category_theory.comonad_hom.id_to_nat_trans {C : Type u₁} [category_theory.category C] (T : category_theory.comonad C) :

(𝟙 T).to_nat_trans = 𝟙 ↑T

source

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

(f ≫ g).to_nat_trans = f.to_nat_trans ≫ g.to_nat_trans

source

@[simp]

theorem category_theory.monad_to_functor_obj (C : Type u₁) [category_theory.category C] (T : category_theory.monad C) :

(category_theory.monad_to_functor C).obj T = ↑T

source

def category_theory.monad_to_functor (C : Type u₁) [category_theory.category C] :

category_theory.monad C ⥤ C ⥤ C

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

Equations

category_theory.monad_to_functor C = {obj := λ (T : category_theory.monad C), ↑T, map := λ (M N : category_theory.monad C) (f : M ⟶ N), f.to_nat_trans, map_id' := _, map_comp' := _}

source

@[simp]

theorem category_theory.monad_to_functor_map (C : Type u₁) [category_theory.category C] (M N : category_theory.monad C) (f : M ⟶ N) :

(category_theory.monad_to_functor C).map f = f.to_nat_trans

source

@[instance]

def category_theory.monad_to_functor.faithful (C : Type u₁) [category_theory.category C] :

category_theory.faithful (category_theory.monad_to_functor C)

source

@[simp]

theorem category_theory.comonad_to_functor_map (C : Type u₁) [category_theory.category C] (M N : category_theory.comonad C) (f : M ⟶ N) :

(category_theory.comonad_to_functor C).map f = f.to_nat_trans

source

def category_theory.comonad_to_functor (C : Type u₁) [category_theory.category C] :

category_theory.comonad C ⥤ C ⥤ C

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

Equations

category_theory.comonad_to_functor C = {obj := λ (G : category_theory.comonad C), ↑G, map := λ (M N : category_theory.comonad C) (f : M ⟶ N), f.to_nat_trans, map_id' := _, map_comp' := _}

source

@[simp]

theorem category_theory.comonad_to_functor_obj (C : Type u₁) [category_theory.category C] (G : category_theory.comonad C) :

(category_theory.comonad_to_functor C).obj G = ↑G

source

@[instance]

def category_theory.comonad_to_functor.faithful (C : Type u₁) [category_theory.category C] :

category_theory.faithful (category_theory.comonad_to_functor C)

source

@[simp]

theorem category_theory.monad_iso.to_nat_iso_hom {C : Type u₁} [category_theory.category C] {M N : category_theory.monad C} (h : M ≅ N) :

(category_theory.monad_iso.to_nat_iso h).hom = (category_theory.monad_to_functor C).map h.hom

source

@[simp]

theorem category_theory.monad_iso.to_nat_iso_inv {C : Type u₁} [category_theory.category C] {M N : category_theory.monad C} (h : M ≅ N) :

(category_theory.monad_iso.to_nat_iso h).inv = (category_theory.monad_to_functor C).map h.inv

source

def category_theory.monad_iso.to_nat_iso {C : Type u₁} [category_theory.category C] {M N : category_theory.monad C} (h : M ≅ N) :

↑M ≅ ↑N

An isomorphism of monads gives a natural isomorphism of the underlying functors.

Equations

category_theory.monad_iso.to_nat_iso h = (category_theory.monad_to_functor C).map_iso h

source

@[simp]

theorem category_theory.comonad_iso.to_nat_iso_hom {C : Type u₁} [category_theory.category C] {M N : category_theory.comonad C} (h : M ≅ N) :

(category_theory.comonad_iso.to_nat_iso h).hom = (category_theory.comonad_to_functor C).map h.hom

source

@[simp]

theorem category_theory.comonad_iso.to_nat_iso_inv {C : Type u₁} [category_theory.category C] {M N : category_theory.comonad C} (h : M ≅ N) :

(category_theory.comonad_iso.to_nat_iso h).inv = (category_theory.comonad_to_functor C).map h.inv

source

def category_theory.comonad_iso.to_nat_iso {C : Type u₁} [category_theory.category C] {M N : category_theory.comonad C} (h : M ≅ N) :

↑M ≅ ↑N

An isomorphism of comonads gives a natural isomorphism of the underlying functors.

Equations

category_theory.comonad_iso.to_nat_iso h = (category_theory.comonad_to_functor C).map_iso h

source

def category_theory.monad.id (C : Type u₁) [category_theory.category C] :

category_theory.monad C

The identity monad.

Equations

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

source

@[simp]

theorem category_theory.monad.id_μ (C : Type u₁) [category_theory.category C] :

(category_theory.monad.id C).μ = 𝟙 (𝟭 C)

source

@[simp]

theorem category_theory.monad.id_η (C : Type u₁) [category_theory.category C] :

(category_theory.monad.id C).η = 𝟙 (𝟭 C)

source

@[simp]

theorem category_theory.monad.id_coe (C : Type u₁) [category_theory.category C] :

↑(category_theory.monad.id C) = 𝟭 C

source

@[instance]

def category_theory.monad.inhabited (C : Type u₁) [category_theory.category C] :

inhabited (category_theory.monad C)

Equations

category_theory.monad.inhabited C = {default := category_theory.monad.id C _inst_1}

source

@[simp]

theorem category_theory.comonad.id_δ (C : Type u₁) [category_theory.category C] :

(category_theory.comonad.id C).δ = 𝟙 (𝟭 C)

source

@[simp]

theorem category_theory.comonad.id_coe (C : Type u₁) [category_theory.category C] :

↑(category_theory.comonad.id C) = 𝟭 C

source

@[simp]

theorem category_theory.comonad.id_ε (C : Type u₁) [category_theory.category C] :

(category_theory.comonad.id C).ε = 𝟙 (𝟭 C)

source

def category_theory.comonad.id (C : Type u₁) [category_theory.category C] :

category_theory.comonad C

The identity comonad.

Equations

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

source

@[instance]

def category_theory.comonad.inhabited (C : Type u₁) [category_theory.category C] :

inhabited (category_theory.comonad C)

Equations

category_theory.comonad.inhabited C = {default := category_theory.comonad.id C _inst_1}