nLab
Lawvere theory

Idea

The notion of Lawvere theory is a joint generalization of the notions of group, ring, associative algebra, etc.

In his 1963 doctoral dissertation, Bill Lawvere introduced a new categorical method for doing universal algebra, alternative to the usual way of presenting an algebraic concept by means of its logical signature (with generating operations satisfying equational axioms). The rough idea is to define an algebraic theory as a category with finite products and possessing a “generic algebra” (e.g., a generic group), and then define a model of that theory (e.g., a group) as a product-preserving functor out of that category. This type of category is what is nowadays called a Lawvere algebraic theory, or just Lawvere theory.

Definition

Definition

A Lawvere theory or finite-product theory is (equivalently encoded by its syntactic category which is) a category $T$ with finite products in which every object is isomorphic to a finite cartesian power $x^n=x\times x\times \cdots \times x$ of a distinguished object $x$ (called the generic object for the theory $T$).

A homomorphism of such theories $T\to T\prime$ is a product-preserving functor.

Remark

For $T$ a Lawvere theory, we are to think of the hom-set $T(n,1)$ as the set of $n$-ary operations definable in the theory. For instance for $T$ the theory of abelian groups, $T(2,1)$ includes operations like $+:(x,y)\mapsto x+y$, $-:(x,y)\mapsto x-y$, and $(x,y)\mapsto 2x-3y$. For $0$-ary or nullary operations, we have $T(0,1)=\{0\}$.

Definition

A model of $T$ – an algebra over the Lawvere theory or simply $T$-algebra – is a product-preserving functor

$$A:T\to \mathrm{Set},$$A : T \to Set \,,

and homomorphism of $T$-algebras is a natural transformation between such functors.

Remark

Such a functor picks out a single set $U(A):=A(1)$ and picks for every $n$-ary abstract operation $\varphi \in T(n,1)$ an actual $n$-ary operation on the elements of this set

$$A(\varphi ):U(A{)}^n\to U(A)$$A(\phi) : U(A)^n \to U(A)

such that these operations are all compatible with each other in the way governed by the composition rules of morphisms in $T$.

Remarks

1. It is common to adopt the (slightly evil) convention that every object of $T$ is equal to a chosen power of $x$. Thus, if $\mathrm{Fin}$ is the category of finite cardinals and functions between them, then the unique (up to isomorphism) product-preserving functor ${\mathrm{Fin}}^{\mathrm{op}}\to T$ that takes the 1-element cardinal to $x$ is commonly supposed to be surjective on objects (rather than, less evilly, essentially surjective), or even an isomorphism on objects so that each morphism $x^n\to x$ has a well-defined arity $n$.

2. Some people use ‘finite-product theory’ to mean any (small) category with finite products, reserving ‘Lawvere theory’ to refer to finite product theories with the property that every object is isomorphic to a product of finitely many copies of a given object $x$. Finite-product theories $C$ can be regarded as a special case of multisorted Lawvere theories (see below) where the set of sorts is $\mathrm{Ob}(C)$ itself. Some, but not all, the above discussion generalizes to this case.

3. As finite-product theories, Lawvere theories are at one end of a spectrum of theories of differing logical strengths. For example, there are left exact theories, regular theories, geometric theories, and so on, which require for their interpretation categories of differing degrees of strength in their internal logic. See also classifying topos.

4. If $C$ is a category with finite products, then a group (object) in $C$ may be defined as a product-preserving functor $T_{\mathrm{Grp}}\to C$. For example, a topological group may be identified with a functor $T_{\mathrm{Grp}}\to \mathrm{Top}$, and a Lie group with a product-preserving functor $T_{\mathrm{Grp}}\to \mathrm{Man}$ into the category of smooth manifolds. An analogous statement holds for any finitary algebraic theory, when formulated in terms of its Lawvere theory $T$.

Variations

• A multisorted or multityped Lawvere theory for a given set of sorts $S$ is a category with finite products $C$ together with a function $i:S\to \mathrm{Ob}(C)$ such that every object of $C$ is isomorphic to a finite product of objects of the form $i(S)$. An example is the theory for ring-module pairs, which may be regarded as a two-sorted theory in which one sort is interpreted as a ring and the other as a module over that ring.

• An infinitary Lawvere theory allows for infinitary operations. An example is the theory of suplattices, where we have, for every cardinal number $n$, an operation to take the supremum of $n$ elements. While Lawvere theories correspond to finitary monads on $\mathrm{Set}$, infinitary Lawvere theories correspond to arbitrary monads.

• A Fermat theory is a Lawvere theory equipped with a notion of differentiation.

• A finite-product theory can also be presented without including all the products of the basic types as actual objects. This yields the notion of cartesian multicategory.

Examples

The theory of sets

The tautological example of a Lawvere theory is the algebraic theory of no operations. This is also called the theory of equality.

Its syntactic category is the category $𝒮$ on objects $n\in \mathbb{N}$ with morphisms generated by the projections ${\pi }_i:n\to 1$. This is the opposite category of the category FinSet

$$𝒮\simeq {\mathrm{FinSet}}^{\mathrm{op}}.$$\mathcal{S} \simeq FinSet^{op} \,.

This is the initial object in the category of Lawvere theories.

An algebra over this theory is just a bare set:

$$𝒮\mathrm{Alg}\simeq \mathrm{Set}.$$\mathcal{S} Alg \simeq Set \,.

For $T$ any Lawvere theory, there is a canonical morphism $𝒮\to T$. On categories of algebras this induces the functor

$$U_T:T\mathrm{Alg}\to 𝒮\mathrm{Alg}\simeq \mathrm{Set}.$$U_T : T Alg \to \mathcal{S}Alg \simeq Set \,.

This sends each algebra to its underlying set . For more on this see the section Free T-algebras below.

The theory of groups

We consider here the theory of groups (defined however you like). To get the corresponding Lawvere theory $T$, let $F(n)$ (for any natural number $n\ge 0$) be a free group on $n$ generators, and define the Lawvere theory $T_{\mathrm{Grp}}$ to be the category opposite to the category of free groups $F(n)$ and group homomorphisms. The generic object $x$ of $T_{\mathrm{Grp}}$ is taken to be $F(1)$.

The category of free groups has finite coproducts since $F(m)+F(n)\cong F(m+n)$ (in other words, the inclusion

$$\mathrm{FreeGroup}\hookrightarrow \mathrm{Group}$$FreeGroup \hookrightarrow Group

creates coproducts in $\mathrm{FreeGroup}$), so $T_{\mathrm{Grp}}$ has finite products, and we have $F(n)=x^n$ in $T_{\mathrm{Grp}}$. Any group $G$ defines a product-preserving functor

$$T_{\mathrm{Grp}}={\mathrm{FreeGroup}}^{\mathrm{op}}\hookrightarrow {\mathrm{Group}}^{\mathrm{op}}\stackrel{\mathrm{hom}(-,G)}{\to }\mathrm{Set}$$T_{Grp} = FreeGroup^{op} \hookrightarrow Group^{op} \stackrel{\hom(-, G)}{\to} Set

since contravariant hom-functors take coproducts to products. Thus any group gives a model of $T_{\mathrm{Grp}}$.

The other direction is more interesting. Let

$$M:T_{\mathrm{Grp}}\to \mathrm{Set}$$M: T_{Grp} \to Set

be a model of $T_{\mathrm{Grp}}$, i.e., a product-preserving functor. We will define a group structure on $G=M(x)$, the underlying set of the group.

To understand this, let’s consider how group multiplication would be defined. The idea is that $x$ in $T_{\mathrm{Grp}}$ is a “generic group”, so we first need to understand how multiplication works there. The idea is that the product in the generic group

$$m:x^2\to x^1$$m: x^2 \to x^1

corresponds to a homomorphism

$$F(1)\to F(2)$$F(1) \to F(2)

which by freeness corresponds to an element $1\to F(2)$, and the element we are after should the product $ab$ of the generators $a,b$ of the free group $F(2)=F(a,b)$. The generators $a,b$ themselves correspond to the two coproduct inclusions

$$i_1:F(1)\to F(1)+F(1)=F(2)i_2:F(1)\to F(1)+F(1)=F(2)$$i_1: F(1) \to F(1) + F(1) = F(2) \qquad i_2: F(1) \to F(1) + F(1) = F(2)

Then, since $M$ is assumed to preserve products, we obtain a map

$$G\times G=M(x)\times M(x)\cong M(x^2)\stackrel{M(m)}{\to }M(x)=G$$G \times G = M(x) \times M(x) \cong M(x^2) \stackrel{M(m)}{\to} M(x) = G

and this defines the group multiplication on $G$. The group identity and group inversion on $G$ are defined by following similar recipes.

It may be checked that the notion of homomorphism of $T_{\mathrm{Grp}}$-models (as defined above) coincides with the usual notion of group homomorphism. In summary, the category of groups is equivalent to the category of models of $T_{\mathrm{Grp}}$.

In particular, any hom-functor

$${\mathrm{hom}}_{T_{\mathrm{Grp}}}(x^n,-):T_{\mathrm{Grp}}\to \mathrm{Set}$$\hom_{T_{Grp}}(x^n, -): T_{Grp} \to Set

preserves products, and so defines a group. This group is precisely the free group on $n$ generators, and a little thought shows that the $n$ generators correspond to the natural transformations

$${\mathrm{hom}}_{T_{\mathrm{Grp}}}(x,-)\to {\mathrm{hom}}_{T_{\mathrm{Grp}}}(x^n,-)$$\hom_{T_{Grp}}(x, -) \to \hom_{T_{Grp}}(x^n, -)

induced by the $n$ projection maps $x^n\to x$.

All of the discussion above for the case of groups generalizes to any finitary algebraic theory (i.e., any single-sorted theory whose signature consists of function symbols of finite arity, subject to universally quantified equational axioms). In summary:

• The Lawvere theory $T$ is the category opposite to the category of free algebras on finitely many generators,

• The category of algebras is in turn equivalent to the category of product-preserving functors $T\to \mathrm{Set}$, and

• The free algebras are retrieved as the representable functors $T\to \mathrm{Set}$.

As discussed in the article on operads, the notion of Lawvere theory may also be formulated in terms of operads relative to the theory of cartesian monoidal categories.

Other examples

• For $k$ a field, the category of free $k$-associative algebras is the (syntactic category of the) theory of ordinary associative algebras over $k$.

• The category CartSp is the (syntactic category of the) theory of smooth algebras. This is also a Fermat theory.

Properties

Coequalizers of $T$-algebras

Definition (congruence)

Let $T$ be a Lawvere theory and $A$ a $T$-algebra. A congruence on $A$ is an equivalence relation on the set $A(1)$ such that whenever for all $n\in \mathbb{N}$ whenever any $(a_i\in A(1){)}_{i=1}^n$ and $(b_i\in A(1){)}_{i=1}^n$ are pairwise eqivalent, $a_i\sim b_i$, then also for every operation $f\in T(n,1)$ the results are equivalent: $f(a_1,\cdot ,a_n)\sim f(b_1,\cdots ,b_n)$.

Observation/Definition

For $A$ a $T$-algebra and for every relation $R\subset A(1)\times A(1)$ there is a smallest congruence on $A$ containing $R$. Write $⟨R⟩\subset A(1)\times A(1)$ for this smallest congruence.

Proposition

For $A$ a $T$-algebra and $C$ a congruence on $A$, the relation $A/C(f)\subset (A/C{)}^n\times A/C$ induced by $A(f)$ for each $f:\in T(n,1)$ are functions and define a $T$-algebra structure on $A(1)/C$.

Proposition

For $f,g:A\to B$ two morphisms of $T$-algebras, the canonical morphism $B\to B/⟨f(a)\sim g(a)\mid a\in A(1)⟩$ is the coequalizer of $f$ and $g$.

Free $T$-algebras and underlying sets

Write $𝒮$ for the (syntactic category of the) algebraic theory of sets (described above). Then for $T$ any other (syntactic category of a) Lawvere theory, there is a canonical morphism

$$i_T:𝒮\to T.$$i_T : \mathcal{S} \to T \,.

By precomposition with $i_T$ we obtain a corresponding functor on $T$-algebras, which we write

$$U_T:T\mathrm{Alg}\to \mathrm{Set}$$U_T : T Alg \to Set

and call the underlying set functor.

Lemma

The functor $U_T$ has a left adjoint $F_T:\mathrm{Set}\to T\mathrm{Alg}$.

This is a standard example of a free functor, called the free $T$-algebra functor.

Proof

For $S\in$ Set, let $F_T(S)$ be the $T$-algebra whose underlying set is the set of formal expressions $\{f(s_1,\cdots ,f_n)\mid f\in T(n,1),s_i\in S\}$ with the evident composition operation.

Observation

For $S=(n)\in$ FinSet a finite set with $n$ elements , the free $T$-algebra on $S$ is just the representable

$$F_T(S)=T(n,-):T\to \mathrm{Set}.$$F_T(S) = T(n,-) : T \to Set \,.

The adjunction isomorphism

$$T\mathrm{Alg}(F_T(S),A)\simeq \mathrm{Set}(S,U_T(A))\simeq (A(1){)}^n\simeq A(n)$$T Alg(F_T(S), A) \simeq Set(S, U_T(A)) \simeq (A(1))^n \simeq A(n)

is in this case just the Yoneda lemma.

$$T\mathrm{Alg}(T(n,-),A)\simeq A(n).$$T Alg(T(n,-),A) \simeq A(n) \,.

Notice that this extends to a functor

$$F_T(-):\mathrm{FinSet}\to T\mathrm{Alg}$$F_T(-) : FinSet \to T Alg

which is the composite

$$F_T(-):\mathrm{FinSet}\stackrel{i_T^{\mathrm{op}}}{\to }{T}^{\mathrm{op}}\stackrel{j}{\to }T\mathrm{Alg}$$F_T(-) : FinSet \stackrel{i_T^{op}}{\to} T^{op} \stackrel{j}{\to} T Alg

of the Yoneda embedding with the opposite of the canonical functor $i_T:{\mathrm{FinSet}}^{\mathrm{op}}\simeq 𝒮\to T$ from the theory of sets, described above.

More generally, for $S\in \mathrm{Set}$ not necessarily finite, let $\mathrm{Sub}(S)$ be the poset of finite subsets of $S$ and their inclusions.

Then $F_T(S)$ is the filtered colimit of the representables corresponding to the finite subsets

$$F_T(S)\simeq {\underrightarrow{\lim }}_{n\in \mathrm{Sub}(S)}T(n,-).$$F_T(S) \simeq {\lim_{\to}}_{{n \in Sub(S)}} T(n,-) \,.

As discussed below, these filtered colimits of $T$-algebras are computed objectwise.

Adjunctions of relatively free $T$-algebras

The following establishes that more generally any morphism of Lawvere theories leads to an adjunction between their categories of algebras.

Let $T_1$ and $T_2$ be Lawvere theories and $f:T_1\to T_2$ a morphism. Write $f^{*}:T_2\mathrm{Alg}\to T_1\mathrm{Alg}$ for the functor on categories of algebras induced by precomposition with $f$.

Lemma

The functor $f^{*}$ has a left adjoint $f_{*}:T_1\mathrm{Alg}\to T_2\mathrm{Alg}$.

Proof

Here is an elementary proof:

Let $F_{T_i}⊣U_{T_i}$ be the two free algebra/underlying-set adjunctions. For $A$ a $T_1$-algebra there is a $T_1$-congruence $\Gamma$ such that

$$A\simeq F_{T_1}{U}_{T_1}(A)/\Gamma .$$A \simeq F_{T_1} U_{T_1}(A) / \Gamma \,.

Since for any set $S$ we have $U_{T_1}{F}_{T_1}(S)\subset U_{T_2}{F}_{T_2}(S)$ it follows that $\Gamma \subset T_{T_2}{F}_{T_2}{U}_{T_1}(A)$. For $⟨\Gamma ⟩$ the smallest $T_2$-congruence containing $\Gamma$ we have that $F_{T_2}{U}_{T_1}(A)/⟨\Gamma ⟩$ is a $T_2$-algebra.

This one checks is $f_{*}A$.

Here is a more high-powered way to obtain this using the monads $K_i$ whose algebras are $T_i$-algebras:

for $A$ a $T_1$-algebra let $f_{*}A:=K_2{\circ }_{K_1}A$ the the evident reflexive [[coequalizer]}

$$K_2{K}_{1}A\overrightarrow{\to }{K}_{2}A\to K_2{\circ }_{K_1}A$$K_2 K_1 A \stackrel{\to}{\to} K_2 A \to K_2 \circ_{K_1} A

in $T_2\mathrm{Alg}$.

Limits and colimits of $T$-algebras

Proposition

For $T$ a Lawvere theory, the category $T\mathrm{Alg}$ has all small limits and colimits.

The limits and the filtered colimits in $T\mathrm{Alg}$ are computed pointwise.

Related concepts

• algebraic theory / generalized algebraic theory / Lawvere theory / 2-Lawvere theory (∞,1)-algebraic theory

  • globular theory

• monad / (∞,1)-monad

• operad / (∞,1)-operad

References

The origin of the categorical formulation of algebraic theories as Lawvere theories is in

• Bill Lawvere, Functorial Semantics of algebraic theories Originally published as: Ph.D. thesis, Columbia University, 1963 and in Reports of the Midwest Category Seminar II, 1968, 41-61, Republished in: Reprints in Theory and Applications of Categories, No. 5 (2004) pp 1-121 (tac)

A standard textbook treatment is chapter 3 of

• Francis Borceux, Handbook of categorical algebra 2 – Categories and structures , Encyclopedia of Mathematics and its Applications, Cambridge University Press (1994)

Other references are

• Steve Lack, Jiri Rosicky, Notions of Lawvere theory (arXiv:0810.2578)