mathlib docs: category_theory.monad.algebra

source

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

Type (max u₁ v₁)

A : C
a : T.obj c.A ⟶ c.A
unit' : (η_ T).app c.A ≫ c.a = 𝟙 c.A . "obviously"
assoc' : (μ_ T).app c.A ≫ c.a = T.map c.a ≫ c.a . "obviously"

An Eilenberg-Moore algebra for a monad T. cf Definition 5.2.3 in [Riehl][riehl2017].

source

@[ext]

structure category_theory.monad.algebra.hom {C : Type u₁} [category_theory.category C] {T : C ⥤ C} [category_theory.monad T] (A B : category_theory.monad.algebra T) :

Type v₁

f : A.A ⟶ B.A
h' : T.map c.f ≫ B.a = A.a ≫ c.f . "obviously"

A morphism of Eilenberg–Moore algebras for the monad T.

source

theorem category_theory.monad.algebra.hom.ext {C : Type u₁} {_inst_1 : category_theory.category C} {T : C ⥤ C} {_inst_2 : category_theory.monad T} {A B : category_theory.monad.algebra T} (x y : A.hom B) (h : x.f = y.f) :

x = y

source

theorem category_theory.monad.algebra.hom.ext_iff {C : Type u₁} {_inst_1 : category_theory.category C} {T : C ⥤ C} {_inst_2 : category_theory.monad T} {A B : category_theory.monad.algebra T} (x y : A.hom B) :

x = y ↔ x.f = y.f

source

def category_theory.monad.algebra.hom.id {C : Type u₁} [category_theory.category C] {T : C ⥤ C} [category_theory.monad T] (A : category_theory.monad.algebra T) :

A.hom A

The identity homomorphism for an Eilenberg–Moore algebra.

Equations

category_theory.monad.algebra.hom.id A = {f := 𝟙 A.A, h' := _}

source

@[simp]

theorem category_theory.monad.algebra.hom.id_f {C : Type u₁} [category_theory.category C] {T : C ⥤ C} [category_theory.monad T] (A : category_theory.monad.algebra T) :

(category_theory.monad.algebra.hom.id A).f = 𝟙 A.A

source

def category_theory.monad.algebra.hom.comp {C : Type u₁} [category_theory.category C] {T : C ⥤ C} [category_theory.monad T] {P Q R : category_theory.monad.algebra T} (f : P.hom Q) (g : Q.hom R) :

P.hom R

Composition of Eilenberg–Moore algebra homomorphisms.

Equations

f.comp g = {f := f.f ≫ g.f, h' := _}

source

@[simp]

theorem category_theory.monad.algebra.hom.comp_f {C : Type u₁} [category_theory.category C] {T : C ⥤ C} [category_theory.monad T] {P Q R : category_theory.monad.algebra T} (f : P.hom Q) (g : Q.hom R) :

(f.comp g).f = f.f ≫ g.f

source

@[simp]

theorem category_theory.monad.algebra.EilenbergMoore_to_category_struct_to_has_hom_hom {C : Type u₁} [category_theory.category C] {T : C ⥤ C} [category_theory.monad T] (A B : category_theory.monad.algebra T) :

(A ⟶ B) = A.hom B

source

@[simp]

theorem category_theory.monad.algebra.EilenbergMoore_to_category_struct_comp {C : Type u₁} [category_theory.category C] {T : C ⥤ C} [category_theory.monad T] {P Q R : category_theory.monad.algebra T} (f : P.hom Q) (g : Q.hom R) :

f ≫ g = f.comp g

source

@[instance]

def category_theory.monad.algebra.EilenbergMoore {C : Type u₁} [category_theory.category C] {T : C ⥤ C} [category_theory.monad T] :

category_theory.category (category_theory.monad.algebra T)

The category of Eilenberg-Moore algebras for a monad. cf Definition 5.2.4 in [Riehl][riehl2017].

Equations

category_theory.monad.algebra.EilenbergMoore = {to_category_struct := {to_has_hom := {hom := category_theory.monad.algebra.hom _inst_2}, id := category_theory.monad.algebra.hom.id _inst_2, comp := category_theory.monad.algebra.hom.comp _inst_2}, id_comp' := _, comp_id' := _, assoc' := _}

source

@[simp]

theorem category_theory.monad.algebra.EilenbergMoore_to_category_struct_id {C : Type u₁} [category_theory.category C] {T : C ⥤ C} [category_theory.monad T] (A : category_theory.monad.algebra T) :

𝟙 A = category_theory.monad.algebra.hom.id A

source

@[simp]

theorem category_theory.monad.forget_map {C : Type u₁} [category_theory.category C] (T : C ⥤ C) [category_theory.monad T] (A B : category_theory.monad.algebra T) (f : A ⟶ B) :

(category_theory.monad.forget T).map f = f.f

source

@[simp]

theorem category_theory.monad.forget_obj {C : Type u₁} [category_theory.category C] (T : C ⥤ C) [category_theory.monad T] (A : category_theory.monad.algebra T) :

(category_theory.monad.forget T).obj A = A.A

source

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

category_theory.monad.algebra T ⥤ C

The forgetful functor from the Eilenberg-Moore category, forgetting the algebraic structure.

Equations

category_theory.monad.forget T = {obj := λ (A : category_theory.monad.algebra T), A.A, map := λ (A B : category_theory.monad.algebra T) (f : A ⟶ B), f.f, map_id' := _, map_comp' := _}

source

@[simp]

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

((category_theory.monad.free T).obj X).A = T.obj X

source

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

C ⥤ category_theory.monad.algebra T

The free functor from the Eilenberg-Moore category, constructing an algebra for any object.

Equations

category_theory.monad.free T = {obj := λ (X : C), {A := T.obj X, a := (μ_ T).app X, unit' := _, assoc' := _}, map := λ (X Y : C) (f : X ⟶ Y), {f := T.map f, h' := _}, map_id' := _, map_comp' := _}

source

@[simp]

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

((category_theory.monad.free T).obj X).a = (μ_ T).app X

source

@[simp]

theorem category_theory.monad.free_map_f {C : Type u₁} [category_theory.category C] (T : C ⥤ C) [category_theory.monad T] (X Y : C) (f : X ⟶ Y) :

((category_theory.monad.free T).map f).f = T.map f

source

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

category_theory.monad.free T ⊣ category_theory.monad.forget T

The adjunction between the free and forgetful constructions for Eilenberg-Moore algebras for a monad. cf Lemma 5.2.8 of [Riehl][riehl2017].

Equations

category_theory.monad.adj T = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : C) (Y : category_theory.monad.algebra T), {to_fun := λ (f : (category_theory.monad.free T).obj X ⟶ Y), (η_ T).app X ≫ f.f, inv_fun := λ (f : X ⟶ (category_theory.monad.forget T).obj Y), {f := T.map f ≫ Y.a, h' := _}, left_inv := _, right_inv := _}, hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}

source

def category_theory.monad.algebra_iso_of_iso {C : Type u₁} [category_theory.category C] (T : C ⥤ C) [category_theory.monad T] {A B : category_theory.monad.algebra T} (f : A ⟶ B) [i : category_theory.is_iso f.f] :

category_theory.is_iso f

Given an algebra morphism whose carrier part is an isomorphism, we get an algebra isomorphism.

Equations

category_theory.monad.algebra_iso_of_iso T f = {inv := {f := category_theory.is_iso.inv f.f i, h' := _}, hom_inv_id' := _, inv_hom_id' := _}

source

@[instance]

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

category_theory.reflects_isomorphisms (category_theory.monad.forget T)

Equations

category_theory.monad.forget_reflects_iso T = {reflects := λ (A B : category_theory.monad.algebra T), category_theory.monad.algebra_iso_of_iso T}

source

@[instance]

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

category_theory.faithful (category_theory.monad.forget T)

source

@[nolint]

structure category_theory.comonad.coalgebra {C : Type u₁} [category_theory.category C] (G : C ⥤ C) [category_theory.comonad G] :

Type (max u₁ v₁)

A : C
a : c.A ⟶ G.obj c.A
counit' : c.a ≫ (ε_ G).app c.A = 𝟙 c.A . "obviously"
coassoc' : c.a ≫ (δ_ G).app c.A = c.a ≫ G.map c.a . "obviously"

An Eilenberg-Moore coalgebra for a comonad T.

source

theorem category_theory.comonad.coalgebra.hom.ext_iff {C : Type u₁} {_inst_1 : category_theory.category C} {G : C ⥤ C} {_inst_2 : category_theory.comonad G} {A B : category_theory.comonad.coalgebra G} (x y : A.hom B) :

x = y ↔ x.f = y.f

source

@[nolint, ext]

structure category_theory.comonad.coalgebra.hom {C : Type u₁} [category_theory.category C] {G : C ⥤ C} [category_theory.comonad G] (A B : category_theory.comonad.coalgebra G) :

Type v₁

f : A.A ⟶ B.A
h' : A.a ≫ G.map c.f = c.f ≫ B.a . "obviously"

A morphism of Eilenberg-Moore coalgebras for the comonad G.

source

theorem category_theory.comonad.coalgebra.hom.ext {C : Type u₁} {_inst_1 : category_theory.category C} {G : C ⥤ C} {_inst_2 : category_theory.comonad G} {A B : category_theory.comonad.coalgebra G} (x y : A.hom B) (h : x.f = y.f) :

x = y

source

@[simp]

theorem category_theory.comonad.coalgebra.hom.id_f {C : Type u₁} [category_theory.category C] {G : C ⥤ C} [category_theory.comonad G] (A : category_theory.comonad.coalgebra G) :

(category_theory.comonad.coalgebra.hom.id A).f = 𝟙 A.A

source

def category_theory.comonad.coalgebra.hom.id {C : Type u₁} [category_theory.category C] {G : C ⥤ C} [category_theory.comonad G] (A : category_theory.comonad.coalgebra G) :

A.hom A

The identity homomorphism for an Eilenberg–Moore coalgebra.

Equations

category_theory.comonad.coalgebra.hom.id A = {f := 𝟙 A.A, h' := _}

source

@[simp]

theorem category_theory.comonad.coalgebra.hom.comp_f {C : Type u₁} [category_theory.category C] {G : C ⥤ C} [category_theory.comonad G] {P Q R : category_theory.comonad.coalgebra G} (f : P.hom Q) (g : Q.hom R) :

(f.comp g).f = f.f ≫ g.f

source

def category_theory.comonad.coalgebra.hom.comp {C : Type u₁} [category_theory.category C] {G : C ⥤ C} [category_theory.comonad G] {P Q R : category_theory.comonad.coalgebra G} (f : P.hom Q) (g : Q.hom R) :

P.hom R

Composition of Eilenberg–Moore coalgebra homomorphisms.

Equations

f.comp g = {f := f.f ≫ g.f, h' := _}

source

@[simp]

theorem category_theory.comonad.coalgebra.EilenbergMoore_to_category_struct_id {C : Type u₁} [category_theory.category C] {G : C ⥤ C} [category_theory.comonad G] (A : category_theory.comonad.coalgebra G) :

𝟙 A = category_theory.comonad.coalgebra.hom.id A

source

@[simp]

theorem category_theory.comonad.coalgebra.EilenbergMoore_to_category_struct_comp {C : Type u₁} [category_theory.category C] {G : C ⥤ C} [category_theory.comonad G] {P Q R : category_theory.comonad.coalgebra G} (f : P.hom Q) (g : Q.hom R) :

f ≫ g = f.comp g

source

@[instance]

def category_theory.comonad.coalgebra.EilenbergMoore {C : Type u₁} [category_theory.category C] {G : C ⥤ C} [category_theory.comonad G] :

category_theory.category (category_theory.comonad.coalgebra G)

The category of Eilenberg-Moore coalgebras for a comonad.

Equations

category_theory.comonad.coalgebra.EilenbergMoore = {to_category_struct := {to_has_hom := {hom := category_theory.comonad.coalgebra.hom _inst_2}, id := category_theory.comonad.coalgebra.hom.id _inst_2, comp := category_theory.comonad.coalgebra.hom.comp _inst_2}, id_comp' := _, comp_id' := _, assoc' := _}

source

@[simp]

theorem category_theory.comonad.coalgebra.EilenbergMoore_to_category_struct_to_has_hom_hom {C : Type u₁} [category_theory.category C] {G : C ⥤ C} [category_theory.comonad G] (A B : category_theory.comonad.coalgebra G) :

(A ⟶ B) = A.hom B

source

@[simp]

theorem category_theory.comonad.forget_map {C : Type u₁} [category_theory.category C] (G : C ⥤ C) [category_theory.comonad G] (A B : category_theory.comonad.coalgebra G) (f : A ⟶ B) :

(category_theory.comonad.forget G).map f = f.f

source

@[simp]

theorem category_theory.comonad.forget_obj {C : Type u₁} [category_theory.category C] (G : C ⥤ C) [category_theory.comonad G] (A : category_theory.comonad.coalgebra G) :

(category_theory.comonad.forget G).obj A = A.A

source

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

category_theory.comonad.coalgebra G ⥤ C

The forgetful functor from the Eilenberg-Moore category, forgetting the coalgebraic structure.

Equations

category_theory.comonad.forget G = {obj := λ (A : category_theory.comonad.coalgebra G), A.A, map := λ (A B : category_theory.comonad.coalgebra G) (f : A ⟶ B), f.f, map_id' := _, map_comp' := _}

source

@[simp]

theorem category_theory.comonad.cofree_map_f {C : Type u₁} [category_theory.category C] (G : C ⥤ C) [category_theory.comonad G] (X Y : C) (f : X ⟶ Y) :

((category_theory.comonad.cofree G).map f).f = G.map f

source

@[simp]

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

((category_theory.comonad.cofree G).obj X).a = (δ_ G).app X

source

@[simp]

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

((category_theory.comonad.cofree G).obj X).A = G.obj X

source

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

C ⥤ category_theory.comonad.coalgebra G

The cofree functor from the Eilenberg-Moore category, constructing a coalgebra for any object.

Equations

category_theory.comonad.cofree G = {obj := λ (X : C), {A := G.obj X, a := (δ_ G).app X, counit' := _, coassoc' := _}, map := λ (X Y : C) (f : X ⟶ Y), {f := G.map f, h' := _}, map_id' := _, map_comp' := _}

source

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

category_theory.comonad.forget G ⊣ category_theory.comonad.cofree G

The adjunction between the cofree and forgetful constructions for Eilenberg-Moore coalgebras for a comonad.

Equations

category_theory.comonad.adj G = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : category_theory.comonad.coalgebra G) (Y : C), {to_fun := λ (f : (category_theory.comonad.forget G).obj X ⟶ Y), {f := X.a ≫ G.map f, h' := _}, inv_fun := λ (g : X ⟶ (category_theory.comonad.cofree G).obj Y), g.f ≫ (ε_ G).app Y, left_inv := _, right_inv := _}, hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}

source

@[instance]

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

category_theory.faithful (category_theory.comonad.forget G)

mathlib documentation

Eilenberg-Moore (co)algebras for a (co)monad

References