nLab algebraic theory (changes)

Showing changes from revision #71 to #72: Added | ~~Removed~~ | ~~Chan~~ged

Context

Categorical algebra

Higher algebra

Idea
Definition
- Variations
Relation to monads
Metaphor
Related concepts
References

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 $x$ of given algebraic type $T$ ”. For example, the Lawvere theory of groups is what you get by assuming a category with products and with a group object $x$ inside, and nothing more; $x$ can be considered “the generic group”. Every object in the Lawvere theory is a finite power $x^n$ of the generic object $x$ . The morphisms $x^n \to x$ are nothing but the $n$ -ary operations it is possible to define on $x$ .

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 $T$ in a category with products $C$ is nothing but (i.e., is equivalent to) a product-preserving functor $T \to C$ ; where the generic object $x$ is sent to is the given model of $T$ in $C$ . If $T$ is the Lawvere theory of groups, then a product-preserving functor $T \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 $C$ could be considered a theory, where the $C$ -models in $D$ are product-preserving functors $C \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 $x$ , and that every other object should be (at least up to isomorphism) a finite power $x^n$ . The exponent $n$ serves to keep track of arities of operations.

The generic “category of arities” $n$ is, in the finitary case, the category opposite to the category of finite sets (opposite because the $n$ appears contravariantly in powers $x^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 $T$ should come equipped with a product-preserving functor

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

that is essentially surjective (each object of $T$ is isomorphic to $x^n$ for some arity $n$ ). 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,\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 $Set$ ): there is a free-forgetful adjunction between $Set$ 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: 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 $C$ 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 $S$ is a set of sorts, then multisorted operations are of the form

\prod_{s \in S} s^{n_s} \to t

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

(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 $n$ , let $[n]$ be a set of that cardinality (sometimes we just use $n$ ).

Definition:

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

i: 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 $S$ be a set whose elements are called sorts. There is a canonical map

i: S \to Ob(Set/S)

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

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

Proposition

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

Proof

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

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

so that $(n, x: n \to S)$ is taken to $\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 $S$ consists of a locally small category with small products, $C$ , together with a sort assignment $\Phi: S \to C$ such that the product-preserving extension

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

is essentially surjective. An operation of arity $x_1, \ldots, x_n \to y$ in $C$ is a morphism of the form $\Pi(n, x) \to \Phi(y)$ in $C$ . If $D$ has small products, a model of $C$ in $D$ is a product-preserving functor $M: 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 $C'$ to have the same objects as $Set/S$ and define hom-sets by $C'(x, y) = C(\Pi(x), \Pi(y)$ . Then, the functor $(Set/S)^{op} \to C$ evidently factors as

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

where the second functor $C' \to C$ is an equivalence, so we may as well work with the functor $\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 $R$ -modules for a fixed commutative ring $R$ 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 $C$ is a (locally small, multi-sorted) Lawvere theory, so we have a product-preserving functor

\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)$ , consisting of product-preserving functors $C \to Set$ and transformations between them, and the category $Set/S$ . We also denote this model category by $Prod(C, Set)$ .

Remark

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

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

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

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

Theorem 1

The functor

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

is left adjoint to the functor

Prod(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(\Pi^{op} (n \stackrel{x}{\to} S)), G) \cong Set/S(n \stackrel{x}{\to} S, G \circ \Pi \circ i)

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

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

by the Yoneda lemma. The right side is isomorphic to

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

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

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

However, because $i: S \to (Set/S)^{op}$ is itself a Yoneda embedding $y^{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 $C$ is the monad $T: Set/S \to Set/S$ associated with this adjunction.

Large Lawvere theory of a monad

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

Definition

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

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

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

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

Theorem 2

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

Proof

In other words, we claim the monad of the adjunction

Set/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 $T$ . Now the functor $\Pi^{op}: Set/S \to Kl(T)$ is left adjoint to the underlying functor $U: Kl(T) \to Set/S$ , and the underlying monad there is of course $T$ . It is obvious that the composite

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: X \to S$ to

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) \to Set/S$ is adjoint to the yoneda embedding, it takes $Set/S(-, T(f))$ to $T(f)$ . This proves the claim.

In the other direction, we have

Theorem 3

Let $C$ be an $S$ -sorted Lawvere theory. Then the Lawvere theory of the monad of $C$ is equivalent to $C$ .

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

Proof

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

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

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

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

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

We thus obtain the comparison functor $Kl(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) \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 $X$ of the monad $T$ gives rise to a model $M_X$ of the Lawvere theory:

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

and similarly a morphism of algebras $f: X \to Y$ gives rise to a homomorphism $M_f: M_X \to M_Y$ , so that we have a functor $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) \to Set/S

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

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

Theorem 4

$A$ is an equivalence.

Proof

In outline, this proceeds as follows:

$A$ is essentially surjective, because if $X$ is a $T$ -algebra, then $M_X: Kl(T)^{op} \to Set$ is a product-preserving functor such that $A(M_X) \cong X$ .
$A$ is full, because any algebra map $f: X \to Y$ gives rise to a model homomorphism $M_f: M_X \to M_Y$ .
$A$ is faithful. For this it suffices to prove that the underlying functor

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

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

$S \stackrel{i}{\to} (Set/S)^{op} \to Kl(T)^{op}$

From the naturality of the diagram

$\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 $Y$ preserves products, we see that the component of $f$ at $\prod_i s_i$ is uniquely determined from the components $f(s): X(s) \to Y(s)$ as $s$ ranges over the image of $\Pi i: S \to Kl(T)^{op}$ , in other words that the functor $U$ defined by $U(X) = X \Pi i$ is faithful.

Thus $A$ is an equivalence, with essential inverse $M$ .

Metaphor

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

(x_1,\ldots ,x_n) \to a_1 x_1 + \cdots + a_n x_n

for some n-tuple $(a_1,\ldots ,a_n)$ of elements of $A$ . 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 $Set$ ) of an algebraic theory $A$ by $A Mod$ . Then compare the following to their counterparts in ring theory:

Related concepts

essentially algebraic theory
algebraic theory / Lawvere theory / 2-Lawvere theory / (∞,1)-algebraic theory
- algebraic side effect
generalized algebraic theory
globular theory
monad / (∞,1)-monad
operad / (∞,1)-operad
finitely complete category, cartesian functor, cartesian logic, cartesian theory
regular category, regular functor, regular logic, regular theory, regular coverage, regular topos
coherent category, coherent functor, coherent logic, coherent theory, coherent coverage, coherent topos
geometric category, geometric functor, geometric logic, geometric theory

References

Ernest G. Manes, Algebraic Theories, Springer (1976) [[doi:10.1007/978-1-4612-9860-1](https://doi.org/10.1007/978-1-4612-9860-1)]
Jiří Adámek, Jiří Rosický, Enrico Vitale, Algebraic theories, Cambridge University Press (2011) [[doi:10.1017/CBO9780511760754](https://doi.org/10.1017/CBO9780511760754), pdf]
Peter Johnstone, Stone Spaces
B. Badzioch, “Algebraic Theories in Homotopy Theory”, Annals of Mathematics, 155, 895–913 (2002).
Andreas Nuyts, Understanding Universal Algebra Using Kleisli-Eilenberg-Moore-Lawvere Diagrams, note

For a framework to compare different notions of algebraic theory see

Soichiro Fujii, A unified framework for notions of algebraic theory, (arXiv:1904.08541)

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

nLab algebraic theory (changes)

Context

Categorical algebra

Higher algebra

Algebraic theories

Algebras and modules

Higher algebras

Model category presentations

Geometry on formal duals of algebras

Theorems

Idea

Categorical formulation

Basic Intuitions

Extensions

Infinitary operations

Multi-sorted operations

Generalized Algebraic Theories

Definition

Definition:

Variations

Essentially algebraic theories

Multisorted algebraic theories

Proposition

Proof

Definition

Commutative theories

Relation to monads

The monad of a locally small Lawvere theory

Remark

Theorem 1

Proof

Large Lawvere theory of a monad

Definition

Theorem 2

Proof

Theorem 3

Proof

Algebras and models

Theorem 4

Proof

Metaphor

Related concepts

References