Birkhoff HSP Through Lawvere Theories
An algebra determines more than a collection of operations: it also determines which expressions in those operations are equal. In the language of Lawvere theories, this equational information forms a quotient theory.
Birkhoff's HSP theorem identifies the models of that quotient. Starting with an algebra
The mechanism becomes particularly transparent through free models: their elements can be represented as functions obtained by evaluating terms in
Equations as morphisms
Let
is an abstract operation in
A model is a finite-product-preserving functor
Writing
For parallel morphisms
We write
The theory detected by a model
Fix a model
This relation is compatible with composition and finite products, so it defines a quotient Lawvere theory
The quotient keeps the objects and identifies exactly those parallel operations that
Thus
The original model factors as
where
Models of the quotient theory
A model
for every pair of parallel morphisms.
In other words,
whose essential image is precisely that class of models. The morphisms remain the original algebra homomorphisms.
This describes the models logically. Birkhoff's theorem gives a construction of all of them.
The HSP theorem
Here
For a single algebra
The Lawvere theory formulation of Birkhoff's theorem is
where the right-hand side is the full subcategory of
The easy direction follows from preservation of equations. Equations hold coordinatewise in products, remain true on subalgebras, and descend along surjective homomorphisms. Hence every algebra constructed by HSP satisfies every identity valid in
The substantive direction is that these constructions produce every such model.
Free models as evaluation functions
Put
For a finite number
Indeed, Yoneda gives
Thus homomorphisms from the free model to
Taking all of these evaluation homomorphisms together gives
On underlying sets, this sends an abstract term to its term function:
This map is injective because
The same construction works for an arbitrary set
Every term uses only finitely many variables, so distinct elements of the free model are separated by an assignment into
Now let
sending the generator labelled by
Consequently,
This is exactly an HSP presentation of
Faithfulness and generation
The quotient map
A faithful model detects every distinction between abstract operations. The theorem turns this ability to distinguish operations into a statement about constructing models: every model is a quotient of a subalgebra of a power of
This also explains why checking an identity in a faithful model is sufficient. Faithfulness reflects it back to an equality in the theory, and every other model preserves that equality.
Here generation means generation under HSP. It is distinct from being a generator object in the categorical sense.
Modules and annihilators
Let
Set
Consequently,
Birkhoff's theorem now reads
In particular, an ordinary faithful module generates all left
Commutative rings and rational evaluation
For commutative unital rings, including the zero ring,
Distinct integer polynomials define distinct functions on
Thus
The construction is explicit. Every commutative ring
Hence
The quotient step explains how torsion and nilpotents can appear. For example, the subring
For each fixed matrix size, the adjugate identities and the Cayley–Hamilton identity are equations in this same theory. Proving them over
A class of models
The construction extends to a class
and form
The general theorem is
The evaluation proof now uses products of possibly different models from
The corresponding faithfulness statement is
This is the classical finitary, single-sorted HSP theorem expressed through Lawvere theories. The quotient theory records the identities shared by the chosen models, and HSP describes exactly the models those identities permit.
Further reading
S. Burris and H. P. Sankappanavar, A Course in Universal Algebra, Chapter II, Sections 9–11, for the classical HSP theorem.
R. B. B. Lucyshyn-Wright, Convex spaces, affine spaces, and commutants for algebraic theories, Sections 1–2, for Lawvere theories, faithful representations, and the matrix theory of modules.
No comments:
Post a Comment