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]
An Eilenberg-Moore algebra for a monad T
.
cf Definition 5.2.3 in [Riehl][riehl2017].
- A : C
The underlying object associated to an algebra.
The structure morphism associated to an algebra.
The unit axiom associated to an algebra.
The associativity axiom associated to an algebra.
A morphism of Eilenberg–Moore algebras for the monad T
.
The underlying morphism associated to a morphism of algebras.
Compatibility with the structure morphism, for a morphism of algebras.
Instances For
The identity homomorphism for an Eilenberg–Moore algebra.
Equations
- CategoryTheory.Monad.Algebra.Hom.id A = { f := CategoryTheory.CategoryStruct.id A.A, h := ⋯ }
Equations
- CategoryTheory.Monad.Algebra.Hom.instInhabited A = { default := { f := CategoryTheory.CategoryStruct.id A.A, h := ⋯ } }
Equations
- One or more equations did not get rendered due to their size.
The category of Eilenberg-Moore algebras for a monad. cf Definition 5.2.4 in [Riehl][riehl2017].
Equations
- CategoryTheory.Monad.Algebra.eilenbergMoore = { toCategoryStruct := CategoryTheory.Monad.Algebra.instCategoryStruct, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }
To construct an isomorphism of algebras, it suffices to give an isomorphism of the carriers which commutes with the structure morphisms.
The forgetful functor from the Eilenberg-Moore category, forgetting the algebraic structure.
Equations
The free functor from the Eilenberg-Moore category, constructing an algebra for any object.
The adjunction between the free and forgetful constructions for Eilenberg-Moore algebras for a monad. cf Lemma 5.2.8 of [Riehl][riehl2017].
Equations
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
The identity monad morphism induces the identity functor from the category of algebras to itself.
Equations
- One or more equations did not get rendered due to their size.
A composition of monad morphisms gives the composition of corresponding functors.
Equations
- One or more equations did not get rendered due to their size.
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 eqToIso
so that the components are nicer to prove
lemmas about.
Equations
- One or more equations did not get rendered due to their size.
Isomorphic monads give equivalent categories of algebras. Furthermore, they are equivalent as
categories over C
, that is, we have algebraEquivOfIsoMonads h ⋙ forget = forget
.
Equations
- One or more equations did not get rendered due to their size.
An Eilenberg-Moore coalgebra for a comonad T
.
- A : C
The underlying object associated to a coalgebra.
The structure morphism associated to a coalgebra.
The counit axiom associated to a coalgebra.
The coassociativity axiom associated to a coalgebra.
A morphism of Eilenberg-Moore coalgebras for the comonad G
.
The underlying morphism associated to a morphism of coalgebras.
Compatibility with the structure morphism, for a morphism of coalgebras.
The identity homomorphism for an Eilenberg–Moore coalgebra.
Equations
- CategoryTheory.Comonad.Coalgebra.Hom.id A = { f := CategoryTheory.CategoryStruct.id A.A, h := ⋯ }
The category of Eilenberg-Moore coalgebras for a comonad.
Equations
- One or more equations did not get rendered due to their size.
The category of Eilenberg-Moore coalgebras for a comonad.
Equations
- CategoryTheory.Comonad.Coalgebra.eilenbergMoore = { toCategoryStruct := CategoryTheory.Comonad.Coalgebra.instCategoryStruct, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }
To construct an isomorphism of coalgebras, it suffices to give an isomorphism of the carriers which commutes with the structure morphisms.
The forgetful functor from the Eilenberg-Moore category, forgetting the coalgebraic structure.
Equations
The cofree functor from the Eilenberg-Moore category, constructing a coalgebra for any object.
The adjunction between the cofree and forgetful constructions for Eilenberg-Moore coalgebras for a comonad.
Equations
- One or more equations did not get rendered due to their size.
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.