Solution (source code)

= Solution

A <Lawvere theory> is a small category with finite products generated by one object $[1]$, so every object is a finite power $[n]$. A model in a finite-product category $\mathcal C$ is a finite-product-preserving functor from the theory to $\mathcal C$. For a <finitary monad> $T$ on sets, take the opposite of the full subcategory of its Eilenberg-Moore category on the finitely generated free algebras; the resulting finite-power category is its Lawvere theory, and its set-valued models are $T$-algebras.

If $\mathbf{Set}^T$ is additive, its full subcategory of finite free algebras is additive, and passing to the opposite preserves biproducts and abelian-group enrichment. Thus the associated theory is an <additive category>. A product-preserving model sends the abelian-group object $[1]$ and its addition, zero, and inverse maps to an internal abelian group in $\mathcal C$.

In an additive theory the product $[n]=[1]^n$ is also a biproduct. If $\iota_i:[1]\to[n]$ and $\pi_i:[n]\to[1]$ are its injections and projections, every $n$-ary operation decomposes uniquely as
$$
\alpha=\sum_{i=1}^n\iota_i\alpha_i,
\qquad \alpha_i=\pi_i\alpha,
$$
which in a model reads $\alpha(x_1,\ldots,x_n)=\sum_i\alpha_i(x_i)$. Put $R=\operatorname{End}([1])$, with addition from the enrichment and multiplication from composition. The unary operations give every model an $R$-module structure, and the displayed decomposition says that all operations are exactly $R$-linear combinations. Conversely every $R$-module interprets them this way. Hence $\mathbf{Set}^T\simeq R\text{-}\mathbf{Mod}$, up to the conventional choice of left versus right modules.