Eilenberg-Moore (co)algebras for a (co)monad
This file defines Eilenberg-Moore (co)algebras for a (co)monad, and provides the category instance for them. Further it defines the adjoint pair of free and forgetful functors, respectively from and to the original category, as well as the adjoint pair of forgetful and cofree functors, respectively from and to the original category.
References
- [Riehl, Category theory in context, Section 5.2.4][riehl2017]
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].
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) :
@[ext]
structure
category_theory.monad.algebra.hom
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad T] :
category_theory.monad.algebra T → category_theory.monad.algebra T → Type v₁
A morphism of Eilenberg–Moore algebras for the monad T.
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) :
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.
@[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
@[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) :
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} :
Composition of Eilenberg–Moore algebra homomorphisms.
@[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) :
@[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) :
@[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) :
@[instance]
def
category_theory.monad.algebra.EilenbergMoore
{C : Type u₁}
[category_theory.category C]
{T : C ⥤ C}
[category_theory.monad 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' := _}
@[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
def
category_theory.monad.forget
{C : Type u₁}
[category_theory.category C]
(T : C ⥤ C)
[category_theory.monad T] :
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' := _}
@[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
@[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
def
category_theory.monad.free
{C : Type u₁}
[category_theory.category C]
(T : C ⥤ C)
[category_theory.monad T] :
The free functor from the Eilenberg-Moore category, constructing an algebra for any object.
@[simp]
theorem
category_theory.monad.free_obj_a
{C : Type u₁}
[category_theory.category C]
(T : C ⥤ C)
[category_theory.monad T]
(X : C) :
@[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
def
category_theory.monad.adj
{C : Type u₁}
[category_theory.category C]
(T : C ⥤ C)
[category_theory.monad 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' := _}
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] :
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' := _}
@[instance]
def
category_theory.monad.forget_reflects_iso
{C : Type u₁}
[category_theory.category C]
(T : C ⥤ C)
[category_theory.monad T] :
Equations
@[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.
@[nolint, ext]
structure
category_theory.comonad.coalgebra.hom
{C : Type u₁}
[category_theory.category C]
{G : C ⥤ C}
[category_theory.comonad G] :
category_theory.comonad.coalgebra G → category_theory.comonad.coalgebra G → Type v₁
A morphism of Eilenberg-Moore coalgebras for the comonad G.
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) :
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) :
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.
@[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) :
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} :
Composition of Eilenberg–Moore coalgebra homomorphisms.
@[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) :
@[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) :
@[instance]
def
category_theory.comonad.coalgebra.EilenbergMoore
{C : Type u₁}
[category_theory.category C]
{G : C ⥤ C}
[category_theory.comonad 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' := _}
@[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) :
@[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) :
@[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
@[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
def
category_theory.comonad.forget
{C : Type u₁}
[category_theory.category C]
(G : C ⥤ C)
[category_theory.comonad G] :
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' := _}
@[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
def
category_theory.comonad.cofree
{C : Type u₁}
[category_theory.category C]
(G : C ⥤ C)
[category_theory.comonad G] :
The cofree functor from the Eilenberg-Moore category, constructing a coalgebra for any object.
@[simp]
theorem
category_theory.comonad.cofree_obj_a
{C : Type u₁}
[category_theory.category C]
(G : C ⥤ C)
[category_theory.comonad G]
(X : C) :
@[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
def
category_theory.comonad.adj
{C : Type u₁}
[category_theory.category C]
(G : C ⥤ C)
[category_theory.comonad 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' := _}