Presenting Lawvere theories?

Question

(Re)Reading Lawvere theories versus classical universal algebra, I was reminded of a question I have had for quite some time:

What is the best way to present Lawvere theories?

By present, I mean give a (mathematical) description of the theory, by means of syntax. The Lawvere theory will be the denotation of that syntax.

I believe I understand the technical advantages that they provide over classical universal algebra (basically in terms of proving theorems over the models). My 'problem' is that I am trying to mechanize (parts of) mathematics. And to do that, one needs examples, which means constructing particular theories; more precisely, that means writing something down, in finite terms which denotes a theory.

Lawvere theories seems to largely abstract this away, unlike classical universal algebra, which gives quite explicit tools for writing things down explicitly. With Lawvere theories, I am reduced to figuring out how to present a small category with finite products such that every object is isomorphic to a finite product of copies of a distinguished object x. I have read quite a bit of CT, and I have yet to find a book which gives me tools as convenient as those of universal algebra for that purpose.

Answer 1

Developing @AndrejBauer's suggestion to present them as single-sorted equational theories, you could write something like:

Let $\mathsf{Grp}$ denote the Lawvere theory with the following presentation.

Generators:

1. $c : 2 \rightarrow 1$

2. $e : 0 \rightarrow 1$

3. $i : 1 \rightarrow 1$

Relations:

1. $c(c(x,y),z) \equiv (x,c(y,z))$

2. $c(e,x) \equiv x,\;\; c(x,e) \equiv x$

3. $c(i(x),x) \equiv e, \;\; c(x,i(x)) \equiv e$

But, perhaps you were looking for something a little deeper.

Answer 2

Maybe the following explanation might help a bit:

I think you should not compare Lawvere theories with clones from universal algebra, as the two things are not on the same level of generality even within their respective field. What, in my oppinion, you should compare are

models of Lawvere theories in Set and clones from UA,

Lawvere theories and Abstract clones.

Obviously, Lawvere theories describe the "abstract behaviour" of their models, the category-theoretic core, so to speak. Similarly, the abstract clone describe the abstract behaviour of the clones of universal algebra (in terms of: it gives you what function you obtain if you compose some functions; but you cannot look into the composition).

Therefore, I do not think it makes much sense to discuss whether you should use Lawvere theories or the concrete notions from UA. The question is rather whether you would like to study models of Lawvere theories or concrete realizations of an abstract clone.

I also find it somewhat misleading to say that you have more explicit tools in the classical framework. Depending on the category where your model is in, you might also have very explicit tools for working with them. You can look at identities (they can all be formulated in a category-theoretic way by using tuplings and projections), look at images (if the category is concrete) and you might even get something from the form of the product.

What I am trying to say is the following: Abstract clones are equivalent to Lawvere theories and concrete clones in UA are equivalent to models in Set.

However, and this is something that affected my personal research, looking at models in categories different from Set might even be interesting if you are only interested in clones in Set.

To understand why that is, let us look at models without their Lawvere theory in the background, just like Universal algebraists often look at concrete clones in UA without having the corresponding abstract clone in mind. This will indicate how close the notions actually are. Let $\mathcal{C}$ be a category with an object $\mathbf{A}$ such that all finite powers of $\mathbf{A}$ also exist in $\mathcal{C}$ (apart from that, the category can be whatever you like), then we can define a clone in the following way:

Let $O_{\mathbf{A}}^{(n)} := \mathcal{C}(\mathbf{A}^n,\mathbf{A})$ and $O_{\mathbf{A}} = \bigcup_{n \geq 0} O_{\mathbf{A}}^{(n)}$. A subset $C \subseteq O_{\mathbf{A}}$ is called a clone over $\mathbf{A}$ if $C$ contains all projection morphisms $\pi_i \colon \mathbf{A}^n \rightarrow \mathbf{A}$ and it closed with respect to superposition in the following way: If $f_1,\ldots,f_n \in C^{(k)} (= O_{\mathbf{A}}^{(n)} \cap C)$ and $f \in C^{(n)}$, then we require $f \circ \langle f_1,\ldots,f_n \rangle \in C$.

Cearly, this definition is just the classical definition of a clone if $\mathcal{C} = Set$ (except that the nullary operations are often excluded from the classical definition, but please let us not get into that). It is also "essentially" a model of a Lawvere theory. By that, I mean the following: A set of morphisms $C$ is a clone over the object $\mathbf{A}$ in the sense given above if any only if there exists a Lawvere theory $\mathcal{L}$ with objects $\mathbf{t_0},\mathbf{t_1},\ldots$ (where $\mathbf{t_i}$ is the $i$-th power of $\mathbf{t_1}$) and a model $M \colon \mathcal{L} \rightarrow \mathcal{C}$ such that $\mathbf{A} = M(\mathbf{t_1})$ and $C = \{ M(f) \mid f \in \mathcal{L}(\mathbf{t_n},\mathbf{t_1}) \}$.

These thoughts at least helped me to understand the connection between models and clones as defined in UA more precisely. I, in fact, like to think of clones as I have described above, so this would be my suggestion how to present them. However, I can hardly clame that this is the best way - it depends on what you want and, of course, your personal taste. In fact, what I find most interesting is to find categories $\mathcal{C}$ and an object $\mathbf{A} \in \mathcal{C}$ such that the clone $O_{\mathbf{A}}$ is equivalent to a certain clone in $Set$, but can now be investigated differently since the categorical environment has changed. This might give universal algebraist some results that would have been much harder to get without the aforementioned change in the environment. In particular, applying duality is then possible and might be interesting (as I have tried to describe in the thread Lawvere theories versus classical universal algebra)

Answer 3

One way to present a Lawvere theory would be via a finite-product sketch. A finite-product sketch $(\mathcal{A}, \mathbb{L})$ is a small category $\mathcal{A}$ equipped with a collection $\mathbb{L}$ of cones over finite discrete diagrams in $\mathcal{A}$; a model in a category $\mathcal{E}$ is a functor $\mathcal{A} \to \mathcal{E}$ which sends the cones in $\mathbb{L}$ to product cones. A Lawvere theory $\mathcal{T}$ can naturally be regarded as a sketch $(\mathcal{T},\mathbb{L})$ where $\mathbb{L}$ consists of all the finite product cones; the sketch $(\mathcal{T},\mathbb{L})$ has the same models as the Lawvere theory $\mathcal{T}$.

Conversely, every sketch $(\mathcal{A},\mathbb{L})$ ``freely generates" a Lawvere theory $\mathcal{T}$ with the same models. One way to put it is this. The sketches form a 2-category $Sketch$ where a 1-cell $(\mathcal{A},\mathbb{L}) \to (\mathcal{A}',\mathbb{L}')$ is a functor $\mathcal{A} \to \mathcal{A}'$ which sends cones in $\mathbb{L}$ to cones in $\mathbb{L}'$, and 2-cells are natural transformations. Lawvere theories also form a 2-category $Law$ where 1-cells are product-preserving functors and 2-cells are natural transformations. By regarding a Lawvere theory as a sketch, we obtain a fully-faithful 2-functor $Law \to Sketch$, and this 2-functor has a left 2-adjoint.

A single-sorted sketch is a sketch $(\mathcal{A},\mathbb{L})$ equipped with a designated object $A_0$ such that for every object $A \in \mathcal{A}$, there is a cone in $\mathbb{L}$ with vertex $A$ and all of its legs equal to $A_0$. Modifying the notion of 1-cell in $Sketch$ accordingly yields a similar relation to 1-sorted Lawvere theories.

For example, a sketch for the category of groups might consist of the opposite of the category of free groups on $\leq 3$ generators, with all product diagrams indicated.

We could get even more syntactic and, following Barr and Wells (see Chapter 4 - a great resource on sketches) define a sketch to consist merely of a reflexive graph $\mathcal{G}$ eqipped with certain diagrams $\mathbb{D}$ in the free category on $\mathcal{G}$ and certain (finite-product) cones $\mathbb{L}$ in the free category on $\mathcal{G}$; a model in a category $\mathcal{E}$ is a morphism of reflexive graphs from $\mathcal{G}$ to the underlying reflexive graph of $\mathcal{E}$ which sends the diagrams of $\mathbb{D}$ to commutative diagrams and the cones of $\mathbb{L}$ to limiting cones. We can view Barr-Wells sketches as containing $Sketch$ and $Law$ as reflective subcategories just as before.

If we use a Barr-Wells sketch, we can give a truly finite presentation of the theory of groups. It is a reflexive graph with objects $G^0,G^1,G^2,G^3$ with arrows $e:G^0 \to G^1$, $m:G^2 \to G^1$, $i: G^1 \to G^1$, various projection arrows, cones which are designated by $\mathbb{L}$ to make $G^i$ into a product of $i$ copies of $G^1$, and one diagram each for associativity, left and right unitality, and left and right inverse laws.