Blog Archive

Saturday, October 24, 2026

Birkhoff HSP Through Lawvere Theories

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 A, we can either impose every identity valid in A and take all models, or construct algebras from A using products, subalgebras, and homomorphic images. Both procedures give the same class.

The mechanism becomes particularly transparent through free models: their elements can be represented as functions obtained by evaluating terms in A.

Equations as morphisms

Let T be a finitary Lawvere theory. Its objects are the natural numbers, with n the designated n-fold power of 1. A morphism

t:n⟶1

is an abstract operation in n variables. Composition expresses substitution, while the product structure supplies projections, repeated variables, and tuples of operations.

A model is a finite-product-preserving functor

A:T⟶Set.

Writing |A|=A(1), we identify A(n) with |A|n. The operation t becomes a function

A(t):|A|n⟶|A|.

For parallel morphisms s,t:n→1, the equation s=t holds in A precisely when A(s)=A(t) as functions: the equality must hold under every assignment of the variables.

We write Mod(T) for the category of models and natural transformations. These natural transformations are exactly the usual algebra homomorphisms.

The theory detected by a model

Fix a model A. On each hom-set of T, define

f∼Ag⟺A(f)=A(g).

This relation is compatible with composition and finite products, so it defines a quotient Lawvere theory

q:T⟶TA,TA=T/∼A.

The quotient keeps the objects and identifies exactly those parallel operations that A cannot distinguish. Concretely,

TA(n,m)≅im(T(n,m)⟶Set(|A|n,|A|m)).

Thus TA consists of the term operations of A arising from the original theory. Its construction depends on the specified algebraic structure on A.

The original model factors as

T→qTA→A―Set,

where A― is faithful. The quotient has made every equality visible in A into an equality in the theory itself.

Models of the quotient theory

A model B:T→Set factors through q exactly when

A(f)=A(g)⟹B(f)=B(g)

for every pair of parallel morphisms.

In other words, B must satisfy every identity satisfied by A. Restriction along q therefore gives a fully faithful functor

q∗:Mod(TA)↪Mod(T),

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 H, S, and P stand for homomorphic images, subalgebras, and arbitrary set-indexed products. We include the empty product and work up to isomorphism.

For a single algebra A, membership in HSP(A) means that, for some set I, there is a subalgebra C of AI and a surjective homomorphism from C onto the given algebra B:

C↪AI,C↠B.

The Lawvere theory formulation of Birkhoff's theorem is

Mod(TA)≃HSP(A),

where the right-hand side is the full subcategory of Mod(T) on these algebras.

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 A.

The substantive direction is that these constructions produce every such model.

Free models as evaluation functions

Put S=TA, and regard A as the faithful S-model A―.

For a finite number n of generators, the free S-model is the representable functor

FS(n)=S(n,−).

Indeed, Yoneda gives

HomMod(S)(FS(n),A)≅A(n)≅|A|n.

Thus homomorphisms from the free model to A are exactly assignments of its generators.

Taking all of these evaluation homomorphisms together gives

FS(n)⟶A|A|n.

On underlying sets, this sends an abstract term to its term function:

S(n,1)⟶|A||A|n,t⟼(a⟼A(t)(a)).

This map is injective because A is faithful. It is a homomorphism because each coordinate is an evaluation homomorphism. We have therefore embedded the free model into a power of A.

The same construction works for an arbitrary set X of generators:

eX:FS(X)↪A|A|X.

Every term uses only finitely many variables, so distinct elements of the free model are separated by an assignment into A. The image is the subalgebra of the function algebra generated by the coordinate functions

πx:|A|X⟶|A|,πx(v)=v(x).

Now let B be any S-model. The free model on its underlying set has a canonical surjective homomorphism

εB:FS(|B|)↠B,

sending the generator labelled by b to b.

Consequently,

FS(|B|)↪A|A||B|,FS(|B|)↠B.

This is exactly an HSP presentation of B. Products collect all evaluations; the embedding realizes the free model as a subalgebra; the quotient imposes the relations defining B.

Faithfulness and generation

The quotient map q is an isomorphism precisely when the original model A:T→Set is faithful. Birkhoff's theorem therefore yields

A is faithful⟺TA≅T via q⟺HSP(A)=Mod(T).

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 A.

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 R be an associative unital ring, and let M be a left R-module. The Lawvere theory of left R-modules is the matrix theory

TR(n,m)=Matm×n(R).

Set I=AnnR(M). Two matrices induce the same function on Mn exactly when their corresponding entries differ by elements of I: testing vectors with just one nonzero coordinate detects each entry.

Consequently,

(TR)M≅TR/I.

Birkhoff's theorem now reads

HSP(M)={N∈R-Mod:IN=0}≃(R/I)-Mod.

In particular, an ordinary faithful module generates all left R-modules under HSP. The familiar condition AnnR(M)=0 is exactly the faithfulness of its model functor.

Commutative rings and rational evaluation

For commutative unital rings, including the zero ring,

TCRing(n,m)=Z[x1,…,xn]m.

Distinct integer polynomials define distinct functions on Qn. This follows by induction on the number of variables from the fact that a nonzero univariate polynomial over a field has only finitely many roots.

Thus Q, regarded as a commutative ring, is a faithful model, and

HSP(Q)=CRing.

The construction is explicit. Every commutative ring B is a quotient of a polynomial ring Z[X], and evaluation gives an embedding

Z[X]↪QQX.

Hence

Z[X]↪QQX,Z[X]↠B.

The quotient step explains how torsion and nilpotents can appear. For example, the subring Z⊆Q has quotients Z/pZ, while the embedded polynomial ring Z[t]⊆QQ has the quotient Z[t]/(t2).

For each fixed matrix size, the adjugate identities and the Cayley–Hamilton identity are equations in this same theory. Proving them over Q therefore proves them over every commutative ring.

A class of models

The construction extends to a class K of T-models. Define

f∼Kg⟺A(f)=A(g)for every A∈K,

and form

TK=T/∼K.

The general theorem is

Mod(TK)≃HSP(K).

The evaluation proof now uses products of possibly different models from K. Only a set-sized product is needed: for each pair of distinct elements of the relevant free model, choose a model and an evaluation that distinguish them.

The corresponding faithfulness statement is

K is jointly faithful⟺HSP(K)=Mod(T).

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

No comments:

Post a Comment

Popular Posts