nLab algebraic theory

Redirected from "equational theories".

Context

Categorical algebra

Higher algebra

Idea

An algebraic theory is a concept in universal algebra that describes a specific type of algebraic gadget, such as groups or rings. An individual group or ring is a model of the appropriate theory. Roughly speaking, an algebraic theory consists of a specification of operations and laws that these operations must satisfy.

Categorical formulation

Traditionally, algebraic theories were described in terms of logical syntax, as first-order theories whose signatures have only function symbols, no relation symbols, and all of whose axioms are equational law?s (universally quantified equations between terms built out of these function symbols). Such descriptions may be viewed as presentations of a theory, analogous to generators and relations as presentations of groups. In particular, different logical presentations can lead to equivalent mathematical objects.

In his thesis, Bill Lawvere undertook a more invariant description of (finitary) algebraic theories. Here all the definable operations of an algebraic theory, or rather their equivalence classes modulo the equational axioms imposed by the theory, are packaged together to form the morphisms of a category with finite products, called a Lawvere theory. None of these operations are considered “primitive”, so a Lawvere theory doesn’t play favorites among operations.

This article is about generalized Lawvere theories. The article Lawvere theory treats the traditional notion of finitary, single-sorted Lawvere theories, with worked examples. The core of the present article is a working out of the precise connection between infinitary (multi-sorted) Lawvere theories and monads.

Basic Intuitions

Intuitively, a Lawvere theory is the “generic category of products equipped with an object xx of given algebraic type TT”. For example, the Lawvere theory of groups is what you get by assuming a category with products and with a group object xx inside, and nothing more; xx can be considered “the generic group”. Every object in the Lawvere theory is a finite power x nx^n of the generic object xx. The morphisms x nxx^n \to x are nothing but the nn-ary operations it is possible to define on xx.

In other words, if we abstract away from the usual set-theoretic semantics, and consider a model for the theory of groups to be any category with finite products together with a specified group object inside, then the Lawvere theory of groups becomes a universal model of the theory, and carries all the information of the theory but independent of a particular presentation. In this way, theories and models of a theory are placed on an equal footing. A model of a Lawvere theory TT in a category with products CC is nothing but (i.e., is equivalent to) a product-preserving functor TCT \to C; where the generic object xx is sent to is the given model of TT in CC. If TT is the Lawvere theory of groups, then a product-preserving functor TSetT \to Set is tantamount to an ordinary group.

The actual categorical construction of a Lawvere theory is described very easily and elegantly: it is the category opposite to the category of (finitely generated) free algebras of the theory. The free algebra on one generator becomes the generic object.

If theories and models are placed on an equal footing, then what feature sets “theories” per se apart? In some very abstract sense, any category with products CC could be considered a theory, where the CC-models in DD are product-preserving functors CDC \to D. Sometimes this is a useful point of view, but it is far removed from traditional syntactic considerations. To give a more “honest” answer, we remember that an ordinary (finitary, single-sorted) algebraic theory a la Lawvere is generated from a single object xx, and that every other object should be (at least up to isomorphism) a finite power x nx^n. The exponent nn serves to keep track of arities of operations.

The generic “category of arities” nn is, in the finitary case, the category opposite to the category of finite sets (opposite because the nn appears contravariantly in powers x nx^n). This is also the Lawvere “theory of equality”, or if you prefer the theory generated by an empty signature. The answer to the question “what sets theories apart” is that a Lawvere theory TT should come equipped with a product-preserving functor

x :FinSet opTx^{-}: FinSet^{op} \to T

that is essentially surjective (each object of TT is isomorphic to x nx^n for some arity nn). As we see below, this definition is a cornerstone to a very elegant theory of algebraic theories.

Extensions

Infinitary operations

Lawvere’s program can be extended to cover many theories with infinitary operations as well. In the best-behaved case, one has algebraic theories involving only operations of arity bounded by some cardinal number — or, more precisely, belonging to some arity class — and these can be understood category-theoretically with a suitable generalization of Lawvere theories. In this bounded case, the Lawvere theory can be described by a small category, and the category of models will be very well behaved, in particular it is a locally presentable category. In such cases there is a satisfying duality between syntax and semantics along the lines of Gabriel-Ulmer duality.

Lawvere’s program can to some degree be extended further: one can work with Lawvere theories which are locally small (not just small) categories. Here, the theory might not be bounded, but at least there is only a small set of operations of each arity. Examples of such large theories include

  • The theory of algebras with arbitrary sums (one model of which is [0,][0,\infty]),

  • The theory of sup-lattices, in which there is one operation of each arity, and

  • The theory of compact Hausdorff spaces, where the operations are parametrized by ultrafilters.

These examples go outside the bounded (small theory) case. Locally small theories in this sense are co-extensive with the notion of monad (on SetSet): there is a free-forgetful adjunction between SetSet and the category of models, and algebras of the theory are equivalent to algebras of the monad.

In the worst case, there are algebraic theories where the number of definable operations explodes, so that there may be a proper class of operations of some fixed arity. In this case there are no free algebras, and Lawvere’s reformulation no longer applies. An example is the theory of complete Boolean algebras. (Note: category theorists who define a category U:ASetU: A \to Set over sets to be algebraic if it is monadic would therefore not consider the variety of algebras in such cases to be “algebraic”).

Further commentary on these aspects may be found in the dozen or so comments in this thread, dated April 13 - May 7, 2009.

In summary, then, here is the connection between the logical and categorial descriptions, based on Johnstone, §§3.7&8. Say that a category CC is:

  • small algebraic if it is given by a (small) set of operation symbols and equations;
  • algebraic if it is given by a monad on the category of (small) sets;
  • large algebraic if it is given by a (possibly proper) class of operation symbols and equations.

Then any small algebraic category is algebraic, and any algebraic category is large algebraic, but neither implication may be reversed.

Multi-sorted operations

Lawvere theories can also be generalized to handle multi-sorted operations. If SS is a set of sorts, then multisorted operations are of the form

sSs n st\prod_{s \in S} s^{n_s} \to t

so that arities are functors n:SSetn: S \to Set, where SS is seen as a discrete category. Thus, an infinitary multi-sorted Lawvere theory TT involves an essentially surjective product-preserving functor

(Set S) opT(Set^S)^{op} \to T

and the development goes through very much as in the single-sorted case.

Generalized Algebraic Theories

See generalized algebraic theory.

Definition

For the moment we discuss the single-sorted case. The many-sorted case should be a straightforward extension.

For any cardinal nn, let [n][n] be a set of that cardinality (sometimes we just use nn).

Definition:

A Lawvere theory or algebraic theory is a locally small category CC with small products that is equipped with an object xx such that the (unique-up-to-isomorphism) product-preserving functor

i:Set opC:[1]xi: Set^{op} \to C: [1] \mapsto x

is essentially surjective.

Variations

Algebraic theories can be extended or specialized in various directions. Here are a few variations on the theme.

Essentially algebraic theories

Essentially algebraic theories allow for partially-defined operations. Just as finitary algebraic theories can be understood as Lawvere theories, which live in the doctrine of cartesian monoidal categories, so finitary essentially algebraic theories can be understood by a generalisation to finitely complete categories.

Multisorted algebraic theories

Multi-sorted theories? allow for more than one sort or type in the theory.

Let SS be a set whose elements are called sorts. There is a canonical map

i:SOb(Set/S)i: S \to Ob(Set/S)

which sends sSs \in S to the object s:1Ss: 1 \to S in Set/SSet/S. Each object USU \to S of Set/SSet/S may be thought of as a monomial term sx s U s\prod_s x_{s}^{U_s} where {x s}\{x_s\} is a set of variables indexed by SS, although it makes better sense to think of it that way when it is regarded as an object of (Set/S) op(Set/S)^{op}.

Thus, objects of (Set/S) op(Set/S)^{op} are pairs (n,x:nS)(n, x: n \to S), where nn is any set, and morphisms (n,x)(m,y)(n, x) \to (m, y) are functions f:[m][n]f: [m] \to [n] such that y=xfy = x \circ f, or y i=x f(i)y_i = x_{f(i)} for all i[m]i \in [m]. Clearly, (Set/S) op(Set/S)^{op} has small products. In fact, any object (n,x)(n, x) of (Set/S) op(Set/S)^{op} is a product of objects of the form i(s)i(s).

Proposition

(Set/S) op(Set/S)^{op} is the free category with small products generated by the set SS.

Proof

Let CC be a category with small products and let Φ:SOb(C)\Phi: S \to Ob(C) be any function. Define a functor

Π:(Set/S) opC\Pi: (Set/S)^{op} \to C

so that (n,x:nS)(n, x: n \to S) is taken to inΦ(x(i))\prod_{i \in n} \Phi(x(i)). It is immediate that Π\Pi is a product-preserving functor and is, up to unique isomorphism, the unique product-preserving functor that extends Φ\Phi.

Definition

A multi-sorted algebraic theory over the set of sorts SS consists of a locally small category with small products, CC, together with a sort assignment Φ:SC\Phi: S \to C such that the product-preserving extension

Π:(Set/S) opC\Pi: (Set/S)^{op} \to C

is essentially surjective. An operation of arity x 1,,x nyx_1, \ldots, x_n \to y in CC is a morphism of the form Π(n,x)Φ(y)\Pi(n, x) \to \Phi(y) in CC. If DD has small products, a model of CC in DD is a product-preserving functor M:CDM: C \to D. A homomorphism of models is simply a natural transformation between product-preserving functors.

It violates the principle of equivalence, but is nevertheless harmless and sometimes convenient, to suppose Π\Pi is an isomorphism on objects, since we can define CC' to have the same objects as Set/SSet/S and define hom-sets by C(x,y)=C(Π(x),Π(y)C'(x, y) = C(\Pi(x), \Pi(y). Then, the functor (Set/S) opC(Set/S)^{op} \to C evidently factors as

(Set/S) opΠCC(Set/S)^{op} \stackrel{\Pi}{\to} C' \to C

where the second functor CCC' \to C is an equivalence, so we may as well work with the functor Π:(Set/S) opC\Pi: (Set/S)^{op} \to C'.

Commutative theories

Commutative algebraic theories are (single-sorted) algebraic theories for which each operation is an algebra homomorphism. These form an important subclass. Their categories of models are closed: the hom sets have a natural model-structure (algebra-structure), and the enriched Hom-functor has a left adjoint, tensor product.

The theory of RR-modules for a fixed commutative ring RR is perhaps the most familiar example. The theory of complete lattices and supremum-preserving functions is an interesting non-finitary example.

Relation to monads

We flesh out the relationships between algebraic theories and monads, starting from the most general situation and then adding conditions to cut down on the size of theories. The term “Lawvere theory” as used here will mean a large (but locally small) infinitary Lawvere theory. (Under this relation ordinary finitary Lawvere theories correspond to finitary monads.)

The monad of a locally small Lawvere theory

Suppose CC is a (locally small, multi-sorted) Lawvere theory, so we have a product-preserving functor

Π:(Set/S) opC\Pi: (Set/S)^{op} \to C

which we may assume to be the identity on objects. We define an adjoint pair between the category of models Mod(C,Set)Mod(C, Set), consisting of product-preserving functors CSetC \to Set and transformations between them, and the category Set/SSet/S. We also denote this model category by Prod(C,Set)Prod(C, Set).

Remark

Observe that (Set/S) op(Set/S)^{op} is a Lawvere theory which is the theory of SS-multi-sorted sets,

Prod((Set/S) op,Set)iSet SSet/S,Prod((Set/S)^{op}, Set) \stackrel{- \circ i}{\simeq} Set^S \simeq Set/S,

where the first equivalence obtains precisely because (Set/S) op(Set/S)^{op} is the free category with products generated by SS.

Let y:C opMod(C,Set)y: C^{op} \to Mod(C, Set) be the Yoneda embedding, taking cc to the product-preserving functor hom(c,):CSethom(c, -): C \to Set.

Theorem 1

The functor

Set/SΠ opC opyMod(C,Set)Set/S \stackrel{\Pi^{op}}{\to} C^{op} \stackrel{y}{\to} Mod(C, Set)

is left adjoint to the functor

Prod(C,Set)Prod(Π,Set)Prod((Set/S) op,Set)Set/SProd(C, Set) \stackrel{Prod(\Pi, Set)}{\to} Prod((Set/S)^{op}, Set) \simeq Set/S

(using the remark above).

Proof

We must exhibit a natural isomorphism

Nat((y(Π op(nxS)),G)Set/S(nxS,GΠi)Nat((y(\Pi^{op} (n \stackrel{x}{\to} S)), G) \cong Set/S(n \stackrel{x}{\to} S, G \circ \Pi \circ i)

where Nat(,)Nat(-, -) indicates the hom-functor on the functor category Mod(C,Set)Mod(C, Set). The left side is naturally isomorphic to

G(Π(nxS))G(\Pi(n \stackrel{x}{\to} S))

by the Yoneda lemma. The right side is isomorphic to

Set/S(nxS,GΠi)Set/S(n \stackrel{x}{\to} S, G\Pi i)

where i:S(Set/S) opi: S \to (Set/S)^{op} is the canonical embedding. Now both GΠG \circ \Pi and Set/S(,GΠi)Set/S(-, G\Pi i) are product-preserving functors (Set/S) opSet(Set/S)^{op} \to Set, so to check these functors are isomorphic, it suffices (by the universal property of (Set/S) op(Set/S)^{op} to check they give isomorphic results when restricted along ii:

GΠiSet/S(i,GΠi)G \Pi i \cong Set/S(i-, G\Pi i)

However, because i:S(Set/S) opi: S \to (Set/S)^{op} is itself a Yoneda embedding y op:S(Set S) opy^{op}: S \to (Set^S)^{op}, the last isomorphism is just an instance of the Yoneda lemma, and this concludes the proof.

The monad of a Lawvere theory CC is the monad T:Set/SSet/ST: Set/S \to Set/S associated with this adjunction.

Large Lawvere theory of a monad

Now let T:Set/SSet/ST: Set/S \to Set/S be a monad on Set/SSet/S, with unit u:1Tu: 1 \to T and multiplication m:TTTm: T T \to T.

Definition

The large Lawvere theory Th(T)Th(T) of TT is the opposite of the Kleisli category, Kl(T) opKl(T)^{op}.

The left adjoint Set/SKl(T)Set/S \to Kl(T) is coproduct-preserving, so we have a product-preserving functor

(Set/S) opKl(T) op(Set/S)^{op} \to Kl(T)^{op}

which is a bijection on the classes of objects. Therefore Kl(T) opKl(T)^{op} is indeed a (large, multi-sorted) Lawvere theory.

Theorem 2

Let TT be a monad on Set/SSet/S. The monad associated with the theory Th(T)Th(T) is isomorphic to TT.

Proof

In other words, we claim the monad of the adjunction

Set/SΠ opKl(T)yProd(Kl(T) op,Set))(Prod(Kl(T) op,Set)Prod(Π,1)Prod((Set/S) op,Set)Set/SSet/S \stackrel{\Pi^{op}}{\to} Kl(T) \stackrel{y}{\to} Prod(Kl(T)^{op}, Set)) \dashv (Prod(Kl(T)^{op}, Set) \stackrel{Prod(\Pi, 1)}{\to} Prod((Set/S)^{op}, Set) \simeq Set/S

is isomorphic to TT. Now the functor Π op:Set/SKl(T)\Pi^{op}: Set/S \to Kl(T) is left adjoint to the underlying functor U:Kl(T)Set/SU: Kl(T) \to Set/S, and the underlying monad there is of course TT. It is obvious that the composite

Set/SΠ opKl(T)yProd(Kl(T) op,Set)Prod(Π,1)Prod((Set/S) op,Set)Set/S \stackrel{\Pi^{op}}{\to} Kl(T) \stackrel{y}{\to} Prod(Kl(T)^{op}, Set) \stackrel{Prod(\Pi, 1)}{\to} Prod((Set/S)^{op}, Set)

takes an object f:XSf: X \to S to

Kl(T)(Π op,Π(f))Set/S(,UΠ(f))Set/S(,T(f))Kl(T)(\Pi^{op}-, \Pi(f)) \cong Set/S(-, U \Pi(f)) \cong Set/S(-, T(f))

and since the equivalence Prod((Set/S) op,Set)Set/SProd((Set/S)^{op}, Set) \to Set/S is adjoint to the yoneda embedding, it takes Set/S(,T(f))Set/S(-, T(f)) to T(f)T(f). This proves the claim.

In the other direction, we have

Theorem 3

Let CC be an SS-sorted Lawvere theory. Then the Lawvere theory of the monad of CC is equivalent to CC.

We assume for convenience that the product-preserving functor Π:(Set/S) opC\Pi: (Set/S)^{op} \to C is the identity on the class of objects.

Proof

We need to exhibit a comparison functor Kl(T) opCKl(T)^{op} \to C, where TT is the monad of CC. Such a comparison functor exists provided that Π:(Set/S) opC\Pi: (Set/S)^{op} \to C has a left adjoint whose associated monad is isomorphic to TT. Now the composite

C opyProd(C,Set)Prod(Π,1)Prod((Set/S) op,Set)C^{op} \stackrel{y}{\to} Prod(C, Set) \stackrel{Prod(\Pi, 1)}{\to} Prod((Set/S)^{op}, Set)

sends an object cc of C opC^{op} to the product-preserving functor C(c,Π):(Set/S) opSetC(c, \Pi-): (Set/S)^{op} \to Set which, by the remark above, is represented by an object of Set/SSet/S which we denote as U opcU^{op} c. In other words we have a natural isomorphism

C(c,Π)(Set/S) op(U opc,)C(c, \Pi-) \cong (Set/S)^{op}(U^{op} c, -)

and by the usual Yoneda yoga, we obtained a functor U op:C(Set/S) opU^{op}: C \to (Set/S)^{op} which is left adjoint to Π\Pi. The monad TT is, by definition (see theorem 1) the monad associated with the adjoint pair (Π op:Set/SC)(U:CSet/S)(\Pi^{op}: Set/S \to C) \dashv (U: C \to Set/S).

We thus obtain the comparison functor Kl(T) opCKl(T)^{op} \to C, and it is the identity on objects. On hom-sets it is given by the natural isomorphism

Kl(T) op(f,g)(Set/S) op(f,T(g))(Set/S) op(f,UΠ op(g))C(Π(f),Π(g))Kl(T)^{op}(f, g) \cong (Set/S)^{op}(f, T(g)) \cong (Set/S)^{op}(f, U\Pi^{op}(g)) \cong C(\Pi(f), \Pi(g))

and hence the comparison functor is an equivalence.

Algebras and models

Each algebra XX of the monad TT gives rise to a model M XM_X of the Lawvere theory:

Kl(T) opAlg(T) ophom(,X)SetKl(T)^{op} \hookrightarrow Alg(T)^{op} \stackrel{\hom(-, X)}{\to} Set

and similarly a morphism of algebras f:XYf: X \to Y gives rise to a homomorphism M f:M XM YM_f: M_X \to M_Y, so that we have a functor M:Alg(T)Mod(Th(T),Set)M: Alg(T) \to Mod(Th(T), Set). This functor is an equivalence.

It is convenient to proceed as follows. By Theorem 2, the underlying functor

Prod(Kl(T) op,Set)Set/SProd(Kl(T)^{op}, Set) \to Set/S

has a left adjoint such that the associated monad is TT, and this yields a comparison functor

A:Prod(Kl(T) op,Set)Alg(T)A: Prod(Kl(T)^{op}, Set) \to Alg(T)
Theorem 4

AA is an equivalence.

Proof

In outline, this proceeds as follows:

  • AA is essentially surjective, because if XX is a TT-algebra, then M X:Kl(T) opSetM_X: Kl(T)^{op} \to Set is a product-preserving functor such that A(M X)XA(M_X) \cong X.

  • AA is full, because any algebra map f:XYf: X \to Y gives rise to a model homomorphism M f:M XM YM_f: M_X \to M_Y.

  • AA is faithful. For this it suffices to prove that the underlying functor

    U:Prod(Kl(T) op,Set)Set/SU: Prod(Kl(T)^{op}, Set) \to Set/S

    is faithful. Let f:XYf: X \to Y be a morphism of Prod(Kl(T) op,Set)Prod(Kl(T)^{op}, Set). Now every object of Kl(T) opKl(T)^{op} is a product is i\prod_i s_i of objects in the image of

    Si(Set/S) opKl(T) opS \stackrel{i}{\to} (Set/S)^{op} \to Kl(T)^{op}

    From the naturality of the diagram

    X( is i) f( is i) Y( is i) X(π) Y(π i) X(s i) f(s i) Y(s i)\array{ X(\prod_i s_i) & \overset{f(\prod_i s_i)}{\to} & Y(\prod_i s_i) \\ \mathllap{X(\pi)} \downarrow & & \downarrow \mathrlap{Y(\pi_i)} \\ X(s_i) & \underset{f(s_i)}{\to} & Y(s_i) }

    and the fact that YY preserves products, we see that the component of ff at is i\prod_i s_i is uniquely determined from the components f(s):X(s)Y(s)f(s): X(s) \to Y(s) as ss ranges over the image of Πi:SKl(T) op\Pi i: S \to Kl(T)^{op}, in other words that the functor UU defined by U(X)=XΠiU(X) = X \Pi i is faithful.

Thus AA is an equivalence, with essential inverse MM.

Metaphor

Ring theory is a branch of mathematics with a well-developed terminology. A ring AA determines and is determined by an algebraic theory, whose models are left AA-modules and whose nn-ary operations have the form

(x 1,,x n)a 1x 1++a nx n(x_1,\ldots ,x_n) \to a_1 x_1 + \cdots + a_n x_n

for some n-tuple (a 1,,a n)(a_1,\ldots ,a_n) of elements of AA. We may call such an algebraic theory annular. The pun model/module is due to Jon Beck. The notion that an algebraic theory is a generalized ring is often a fertile one, that automatically provides a slew of suggestive terminology and interesting problems. Many fundamental ideas of ring/module-theory are simply the restriction to annular algebraic theories of ideas that apply more widely to algebraic theories and their models.

Let us denote the category of models and homomorphisms (in SetSet) of an algebraic theory AA by AModA Mod. Then compare the following to their counterparts in ring theory:

References

For a framework to compare different notions of algebraic theory see

Last revised on December 2, 2023 at 11:28:04. See the history of this page for a list of all contributions to it.