Free Lawvere theory on a signature

Question

Let $\mathsf{Law}$ be the category of (single-sorted) Lawvere theories. There is a forgetful functor $U : \mathsf{Law} \to \mathsf{Set}^\mathbb{N}$ that sends a Lawvere theory to its associated "signature", i.e. the functor $\mathbb{N} \to \mathsf{Set}$ that sends each $n \in \mathbb{N}$ to the set of $n$-ary operations in the Lawvere theory. I believe it is known that this functor has a left adjoint, but I have not been able to find a proof of this fact. Can someone provide the proof that $U : \mathsf{Law} \to \mathsf{Set}^\mathbb{N}$ has a left adjoint, or point me to an appropriate reference? Also, is it possible to prove this without using the equivalence between Lawvere theories and finitary monads on $\mathsf{Set}$, or the fact that any Lawvere theory has a "syntactic" presentation (i.e. can this be proved just from the categorical definition of Lawvere theory)?

Answer 1

I'll sketch the proof strategy, but I think it's helpful to try filling in the details yourself if you're not familiar with the argument.

First, one should observe that the category $\mathbf{Law}$ of Lawvere theories is isomorphic to the category $\mathbf{Clone}$ of abstract clones. This follows fairly directly from the universal property of the cartesian product. By definition, the category $\mathbf{Clone}$ is clearly algebraic, in that it is presented by operations and equations. The sorts are given by the natural numbers $\mathbb N$, where each $n \in \mathbb N$ indexes the set $C_n$ of terms with $n$ free variables. Finally, every $S$-sorted algebraic theory is monadic over $\mathbf{Set}^S$: this follows from the equivalence between algebraic theories and finitary monads, but you can also prove it directly (e.g. by using Beck's monadicity theorem) if you want to avoid invoking that result.