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.


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.

  • $\begingroup$ So a categorical construction of the quotient should be given by the coequalizer of the two projections of the Lawvere theory freely generated (by your construction) by the pairs of operations you want to make equal, right? (then the question is how to construct the coequalizer but that doesn't look too hard) $\endgroup$ – Daniel Satanove Oct 1 '18 at 4:57
  • $\begingroup$ Yes, that's right. $\endgroup$ – Qiaochu Yuan Oct 1 '18 at 4:58
  • $\begingroup$ @Daniel: oops, also I lied, the left adjoint is a bit more complicated than what I said. I also need to allow diagonal maps / copying of variables or else I'm really talking about operads. $\endgroup$ – Qiaochu Yuan Oct 4 '18 at 5:05
  • $\begingroup$ Yeah I realized that later. An easy way to describe it would be by using a basic type theory with rules for the operations and contraction/weakening/exchange $\endgroup$ – Daniel Satanove Oct 5 '18 at 6:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.