What is a presentation of a Lawvere theory formally, and how do you generate the associated Lawvere theory?

143 Views Asked by At

A Lawvere theory for a specific algebraic theory is usually given by some sort of presentation. You have generating functions and constants $f_i:A^n \to A$, and relations $(r_1,r_2) \in ``\mathrm{Hom}(A^n,A)" \times ``\mathrm{Hom}(A^n,A)"$, usually expressed in diagrams, and the Lawvere theory associated to it is in some sense the free Lawvere theory mod relations that set each $r_1=r_2$.

So there are two problems here, the first alluded to with my use of quotes. We don't a priori have a category to define the relations over. What is the category? I have two ideas but they both run into issues.

First, generate the free monoid on the set $\{A\}$ to get the underlying set of objects $T_0$, then define a graph for our functions $s,t : G \to T_0 \times T_0$ where $G = \{f_i\} $ and s and t are the appropriate source and target maps. Now we want to define our relations on arbitrary compositions of our graph edges with projections and pairings. Here we run into a problem. We might try to take the free category with strict products on the graph, but this will create new products that don't line up with the $A^n \in T_0$. Perhaps, though, there is a way to create a free category with strict products on a graph with a free monoid structure on the underlying set of vertices (for which the product structure on objects coincides with the free monoid structure)?

The second attempt is to instead start with the initial Lawvere theory, take the forgetful functor to graphs, adjoin the function and constant symbols, and then take the free category on this graph. This doesn't change the underlying set of objects. The obvious problem here is that we don't get pairings of our new function symbols so first we won't be able to define relations between terms with pairs in them, and second, we won't end up with a category with products. If there is a way to make this into a category with products and you don't care about equations between pairs, then this might be suitable, but it seems that a solution to this problem would be close to or similar to a solution to the problem in the first attempt.

The second issue (which might be a straightforward calculation?) is constructing the final Lawvere theory modulo relations. This would require generating an equivalence relation from the relations given that is a congruence with respect to the categorical structure. I'm not sure how to do that but perhaps it will become more obvious if I have a solution to the first problem.

So I'm looking for how to do this construction, and perhaps some references since this surely has been done before. Secondly, my initial goal was the theory of categories which is a finite limit theory, a bit more complicated, and I found I didn't really know how to do it with Lawvere theories so I here I am trying to figure this gout first. So a way to do finite limit theories too, or a way or general method in which this can extend to finite limit theories would be appreciated.

1

There are 1 best solutions below

4
On

I'm not sure I understand your attempts; here is what seems to me to be the obvious construction, which works. $\text{Law}$ admits a forgetful functor to $\text{Set}^{\mathbb{N}}$ given by taking a Lawvere theory $L$ to the function $\mathbb{N} \to \text{Set}$ sending $n \in \mathbb{N}$ to the set of $n$-ary operations in $L$ (for the purposes of this answer $\mathbb{N}$ contains zero). This forgetful functor has a left adjoint which constructs the free Lawvere theory on a bunch of $k$-ary operations. This free functor is slightly annoying to describe in rigorous detail. An $n$-ary operation in it looks like a rooted tree with $n$ leaves, where vertices with $k$ children are labeled by one of the original $k$-ary operations. Then you impose relations by identifying some of these trees.