mathlib3 documentation

category_theory.monad.algebra

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

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

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

Instances for category_theory.monad.algebra
theorem category_theory.monad.algebra.unit {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} (self : T.algebra) :
T.η.app self.A self.a = 𝟙 self.A
theorem category_theory.monad.algebra.assoc {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} (self : T.algebra) :
T.μ.app self.A self.a = T.map self.a self.a
theorem category_theory.monad.algebra.unit_assoc {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} (self : T.algebra) {X' : C} (f' : self.A X') :
T.η.app self.A self.a f' = f'
theorem category_theory.monad.algebra.assoc_assoc {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} (self : T.algebra) {X' : C} (f' : self.A X') :
T.μ.app self.A self.a f' = T.map self.a self.a f'
@[ext]

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

Instances for category_theory.monad.algebra.hom
theorem category_theory.monad.algebra.hom.ext {C : Type u₁} {_inst_1 : category_theory.category C} {T : category_theory.monad C} {A B : T.algebra} (x y : A.hom B) (h : x.f = y.f) :
x = y
theorem category_theory.monad.algebra.hom.ext_iff {C : Type u₁} {_inst_1 : category_theory.category C} {T : category_theory.monad C} {A B : T.algebra} (x y : A.hom B) :
x = y x.f = y.f
@[simp]
theorem category_theory.monad.algebra.hom.h {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {A B : T.algebra} (self : A.hom B) :
T.map self.f B.a = A.a self.f
@[simp]
theorem category_theory.monad.algebra.hom.h_assoc {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {A B : T.algebra} (self : A.hom B) {X' : C} (f' : B.A X') :
T.map self.f B.a f' = A.a self.f f'

The identity homomorphism for an Eilenberg–Moore algebra.

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

Composition of Eilenberg–Moore algebra homomorphisms.

Equations
@[simp]
theorem category_theory.monad.algebra.comp_f {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {A A' A'' : T.algebra} (f : A A') (g : A' A'') :
(f g).f = f.f g.f
def category_theory.monad.algebra.iso_mk {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {A B : T.algebra} (h : A.A B.A) (w : T.map h.hom B.a = A.a h.hom) :
A B

To construct an isomorphism of algebras, it suffices to give an isomorphism of the carriers which commutes with the structure morphisms.

Equations
@[simp]
theorem category_theory.monad.forget_map {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) (A B : T.algebra) (f : A B) :
T.forget.map f = f.f

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

Equations
@[simp]
@[simp]
theorem category_theory.monad.free_map_f {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) (X Y : C) (f : X Y) :
(T.free.map f).f = T.to_functor.map f

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

Equations
@[simp]
theorem category_theory.monad.adj_counit {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) :
T.adj.counit = {app := λ (Y : T.algebra), {f := Y.a, h' := _}, naturality' := _}

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

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

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

Given a monad morphism from T₂ to T₁, we get a functor from the algebras of T₁ to algebras of T₂.

Equations
@[simp]
theorem category_theory.monad.algebra_functor_of_monad_hom_map_f {C : Type u₁} [category_theory.category C] {T₁ T₂ : category_theory.monad C} (h : T₂ T₁) (A₁ A₂ : T₁.algebra) (f : A₁ A₂) :

The identity monad morphism induces the identity functor from the category of algebras to itself.

Equations

If f and g are two equal morphisms of monads, then the functors of algebras induced by them are isomorphic. We define it like this as opposed to using eq_to_iso so that the components are nicer to prove lemmas about.

Equations
@[nolint]

An Eilenberg-Moore coalgebra for a comonad T.

Instances for category_theory.comonad.coalgebra
theorem category_theory.comonad.coalgebra.coassoc {C : Type u₁} [category_theory.category C] {G : category_theory.comonad C} (self : G.coalgebra) :
self.a G.δ.app self.A = self.a G.map self.a
theorem category_theory.comonad.coalgebra.counit_assoc {C : Type u₁} [category_theory.category C] {G : category_theory.comonad C} (self : G.coalgebra) {X' : C} (f' : self.A X') :
self.a G.ε.app self.A f' = f'
theorem category_theory.comonad.coalgebra.coassoc_assoc {C : Type u₁} [category_theory.category C] {G : category_theory.comonad C} (self : G.coalgebra) {X' : C} (f' : G.obj (G.obj self.A) X') :
self.a G.δ.app self.A f' = self.a G.map self.a f'
theorem category_theory.comonad.coalgebra.hom.ext_iff {C : Type u₁} {_inst_1 : category_theory.category C} {G : category_theory.comonad C} {A B : G.coalgebra} (x y : A.hom B) :
x = y x.f = y.f
@[nolint, ext]

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

Instances for category_theory.comonad.coalgebra.hom
  • category_theory.comonad.coalgebra.hom.has_sizeof_inst
theorem category_theory.comonad.coalgebra.hom.ext {C : Type u₁} {_inst_1 : category_theory.category C} {G : category_theory.comonad C} {A B : G.coalgebra} (x y : A.hom B) (h : x.f = y.f) :
x = y
@[simp]
theorem category_theory.comonad.coalgebra.hom.h {C : Type u₁} [category_theory.category C] {G : category_theory.comonad C} {A B : G.coalgebra} (self : A.hom B) :
A.a G.map self.f = self.f B.a
@[simp]
theorem category_theory.comonad.coalgebra.hom.h_assoc {C : Type u₁} [category_theory.category C] {G : category_theory.comonad C} {A B : G.coalgebra} (self : A.hom B) {X' : C} (f' : G.obj B.A X') :
A.a G.map self.f f' = self.f B.a f'

The identity homomorphism for an Eilenberg–Moore coalgebra.

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

Composition of Eilenberg–Moore coalgebra homomorphisms.

Equations
@[simp]
theorem category_theory.comonad.coalgebra.comp_f {C : Type u₁} [category_theory.category C] {G : category_theory.comonad C} {A A' A'' : G.coalgebra} (f : A A') (g : A' A'') :
(f g).f = f.f g.f
def category_theory.comonad.coalgebra.iso_mk {C : Type u₁} [category_theory.category C] {G : category_theory.comonad C} {A B : G.coalgebra} (h : A.A B.A) (w : A.a G.map h.hom = h.hom B.a) :
A B

To construct an isomorphism of coalgebras, it suffices to give an isomorphism of the carriers which commutes with the structure morphisms.

Equations
@[simp]

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

Equations
Instances for category_theory.comonad.forget
@[simp]
theorem category_theory.comonad.cofree_map_f {C : Type u₁} [category_theory.category C] (G : category_theory.comonad C) (X Y : C) (f : X Y) :

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

Equations

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

Equations
@[simp]
theorem category_theory.comonad.adj_unit {C : Type u₁} [category_theory.category C] (G : category_theory.comonad C) :
G.adj.unit = {app := λ (X : G.coalgebra), {f := X.a, h' := _}, naturality' := _}

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

Given a coalgebra morphism whose carrier part is an epimorphism, we get an algebra epimorphism.

Given a coalgebra morphism whose carrier part is a monomorphism, we get an algebra monomorphism.