Eilenberg-Moore algebras for a monad

This file defines Eilenberg-Moore algebras for a 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.

References

[Riehl, Category theory in context, Section 5.2.4][riehl2017]

category_theory.monad.algebra

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

category_theory.monad.algebra.EilenbergMoore

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

category_theory.monad.adj

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