10.3 The Eilenberg-Moore category

The Eilenberg-Moore category provides a framework for understanding algebras associated with monads. It defines objects as T-algebras and morphisms as T-algebra homomorphisms, creating a structured environment to study monadic computations.

This category encapsulates the algebraic structure of monads, allowing for analysis of relationships between algebras. It also enables the interpretation of monadic computations as morphisms between algebras, ensuring well-behaved and compositional semantics for these computations.

The Eilenberg-Moore Category

Definition of Eilenberg-Moore category

• Eilenberg-Moore category $\mathcal{C}^T$ for a monad $(T, \eta, \mu)$ on a category $\mathcal{C}$ consists of:
  • Objects: T-algebras $(A, a)$ where $A$ is an object in $\mathcal{C}$ and $a: TA \to A$ is a morphism satisfying:
    • $a \circ \eta_A = id_A$ (unit law)
    • $a \circ Ta = a \circ \mu_A$ (associativity law)
  • Morphisms: T-algebra homomorphisms $f: (A, a) \to (B, b)$ where $f: A \to B$ is a morphism in $\mathcal{C}$ such that:
    • $f \circ a = b \circ Tf$ (homomorphism condition)
• Composition of morphisms inherited from the base category $\mathcal{C}$
• Identity morphisms for each object $(A, a)$ given by $id_A: A \to A$

Relationship to monad algebras

• Eilenberg-Moore category $\mathcal{C}^T$ encapsulates algebras for the monad $T$
  • Each object in $\mathcal{C}^T$ is an algebra for $T$ with a specific structure
  • Morphisms in $\mathcal{C}^T$ preserve the algebra structure and respect the monad operations
• Provides a categorical framework to study and compare algebras for a monad
  • Allows analyzing relationships between algebras through morphisms ($\mathcal{C}^T$ morphisms)
• Generalizes the notion of algebras for a monad to a category-theoretic setting

Proof of category axioms

• Identity morphism axiom: For each T-algebra $(A, a)$, $id_A: A \to A$ is a T-algebra homomorphism
  • $id_A \circ a = a \circ T(id_A)$ holds by the identity law in $\mathcal{C}$
• Composition axiom: If $f: (A, a) \to (B, b)$ and $g: (B, b) \to (C, c)$ are T-algebra homomorphisms, then $g \circ f: (A, a) \to (C, c)$ is also a T-algebra homomorphism
  • $(g \circ f) \circ a = g \circ (f \circ a) = g \circ (b \circ Tf) = (g \circ b) \circ Tf = c \circ T(g \circ f)$ (by associativity and homomorphism conditions)
• Associativity axiom: Composition of T-algebra homomorphisms is associative
  • Inherited from the associativity of composition in the base category $\mathcal{C}$

Framework for monadic computations

• Eilenberg-Moore category allows interpreting monadic computations as morphisms between algebras
  • A monadic computation $m: TA \to TB$ can be lifted to a morphism $m^\sharp: (A, a) \to (B, b)$ in $\mathcal{C}^T$ where:
    • $m^\sharp = b \circ m$ (lifting operation)
• Ensures well-behaved and compositional semantics for monadic computations
  • Composition of lifted morphisms corresponds to composition of monadic computations
  • Identity morphism represents the trivial computation $\eta_A$
• Enables studying properties and relationships of monadic computations using categorical tools
  • Monadic laws expressible as commutative diagrams in $\mathcal{C}^T$
  • Morphisms between algebras allow comparing and transforming monadic computations ($\mathcal{C}^T$ morphisms)