Eilenberg-Moore Category

definition theorem proof example

A monad algebra (Eilenberg–Moore algebra) for a Monad $(T,\eta ,\mu )$ is an algebra $(a,\alpha :Ta\to a)$ compatible with the monad: the unit law $\alpha \circ {\eta }_a={\mathrm{id}}_a$ and the multiplication law $\alpha \circ {\mu }_a=\alpha \circ T\alpha$. The second says $\alpha$ is itself an algebra morphism $(Ta,{\mu }_a)\to (a,\alpha )$. Monad algebras and algebra morphisms form the Eilenberg–Moore category ${\mathcal{C}}^T$.

Sources: DaoFP §15.5 (“Monad Algebras”, “Eilenberg-Moore category”, “Kleisli category”); §14.7 (the expression monad Ex); 7 Sketches §1.4.4 (fixed points of a Closure Operator); Kittenlab Lecture 5 (monoids as algebras).

Intuition. Monads generate expressions, algebras evaluate them; compatibility says evaluating a bare variable returns it (alg . return = id, ruling out alg (Var c) = 'a') and evaluating a flattened nested expression equals evaluating inside first (alg (join mma) = alg (fmap alg mma)). For the free monoid monad, algebras are exactly monoids; for a closure operator on a preorder, algebras are its fixed points.

Theorem (every monad comes from an adjunction). Define $U^T:{\mathcal{C}}^T\to \mathcal{C}$, $(a,\alpha )\mapsto a$, and $F^{T}a:=(Ta,{\mu }_a)$ (a monad algebra by the monad laws), $F^{T}f=Tf$ (an algebra morphism by naturality of $\mu$). Take unit $\eta$ and counit ${\epsilon }_{(a,\alpha )}:=\alpha$ (an algebra morphism $F^T{U}^T(a,\alpha )\to (a,\alpha )$ by the multiplication law); the triangle identities follow from the unit laws. Then $U^T{F}^T=T$ on objects and arrows, the unit agrees by construction, and $U^T\epsilon F^T$ at $a$ is ${\epsilon }_{(Ta,{\mu }_a)}={\mu }_a$. So $T$ is generated by $F^T⊣U^T$ (Monads from Adjunctions). $■$

The Kleisli Category is the full subcategory of free algebras $(Ta,{\mu }_a)$; among adjunctions generating $T$ (a 2-category), Kleisli is initial and Eilenberg–Moore terminal.

JuliaLeanHaskell

Docs: Kittenlab Lecture 5

# monad algebras for the list monad are monoids: α : [m] -> m must satisfy the two laws
α_sum(xs) = sum(xs; init=0)                       # (Int, +, 0)
α_sum([5]) == 5                                   # unit law: α ∘ η = id
xss = [[1, 2], [3]]
α_sum(reduce(vcat, xss)) == α_sum(map(α_sum, xss))  # multiplication law: α ∘ μ = α ∘ T α
# a non-example: α(xs) = length(xs) fails the unit law (α([5]) = 1 ≠ 5)

import Mathlib
open CategoryTheory
#check @CategoryTheory.Monad.Algebra          -- A, a : T.obj A ⟶ A, unit, assoc
#check @CategoryTheory.Monad.Algebra.Hom
#check @CategoryTheory.Monad.forget           -- U^T : Algebra T ⥤ C
#check @CategoryTheory.Monad.free             -- F^T
#check @CategoryTheory.Monad.adj              -- free ⊣ forget
#check @CategoryTheory.Monad.algebraFunctorOfMonadHom

-- an algebra for the expression monad Ex compatible with return and join
data Ex x = Val Int | Var x | Plus (Ex x) (Ex x) deriving Functor
algChar :: Ex Char -> Char
algChar (Val n)      = toEnum n
algChar (Var c)      = c                          -- alg . return = id
algChar (Plus e1 e2) = maximum [algChar e1, algChar e2]
-- monad algebras for [] are Monoids: alg = mconcat