MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).

## Presenting Lawvere theories?

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

-
you can make models $\Omega(\mathcal{C})$ category of a algebraic theory $\Omega$ on any cartesian category $\mathcal{C}$ (ie. with finite limits, or finite products is enought I seem), you have the 2-funtor: $\mathcal{C} \mapsto \Omega(\mathcal{C})$, THe Lawvere categry make a realization of this functor. "Categories" H. ScHubert, or Theory of categories - Nicolae Popescu give a good exposition of LAvwere theory. in the general setting of classifing catgories of some type of logic, see: B. Jacobs, Categorical Logic and Type Crole, R. L.: Categories for Types. CUP – Buschi Sergio Jan 8 2012 at 17:28
I am not sure exactly what you mean here by present. Is it something like to describe a monoid one needs from the point of view of universal algebra to say an associative multiplication and a nullary operation while one needs the whoe clone to describe the Lawvere theory? – Benjamin Steinberg Jan 8 2012 at 21:14
You could present them as single-sorted equational theories... – Andrej Bauer Jan 9 2012 at 0:21
I agree with Andrej. In fact, I think the first of Lawvere's contributions here was exactly to point out what abstract entities are presented by (single-sorted) equational theories, in exactly the same sense as groups are the abstract entities presented by generators and relations. – Andreas Blass Jan 9 2012 at 1:06
@Andrej: I like that 'answer', definitely something I can work with! – Jacques Carette Jan 9 2012 at 2:55

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)

-
 I am sure that, mathematically, this makes perfect sense. However, it does not answer my questions nearly as well as Andrej Bauer's short comment does... Fundamentally I think the issue is that I am asking the question from the point of view of Computer Science, with the ultimate aim of using theory presentations as a specification for an actual implementation. So my question really was about syntax and not so concerned with semantics. – Jacques Carette Aug 25 at 14:30