This material is in reply to a query of John Baez at the n-Category Café.
This section is just to provide some background for notions of multisorted Lawvere theories, to state a form of John’s desired theorem, and to fix some general notation.
Let $i: Fin \to Set$ be the inclusion of the category of finite sets $\{1, \ldots, n\}$ into the category of all sets. Let $\Lambda$ be a set, and let $i \downarrow \Lambda$, or just $Fin/\Lambda$, be the comma category whose objects are pairs $(F, x: S \to \Lambda)$ where $S$ is a finite set.
We can think of such a pair $(S, x)$ as a finite set fibered over $\Lambda$, so that all but finitely many fibers are empty. The category $Fin/\Lambda$ has finite coproducts (they are just coproducts in each separate fiber).
A key fact we need is that $Fin/\Lambda$ is the free category with finite coproducts generated by $\Lambda$. More formally: treat the set $\Lambda$ as a discrete category; there is an evident functor $\iota: \Lambda \to Fin/\Lambda$ which takes $\lambda \in \Lambda$ to the evident fibered set $\lambda: 1 \to \Lambda$.
Let $C$ be a category with finite coproducts, and let $f: \Lambda \to C$ be a functor. There is (up to unique isomorphism) a unique coproduct-preserving functor $\tilde{f}: Fin/\Lambda \to C$ that extends $f$ along $\iota: \Lambda \to Fin/\Lambda$. If $C$ has chosen coproducts, we can demand preservation on the nose.
The idea of proof is that $\tilde{f}$ takes a fibered set $x: S \to \Lambda$ to the coproduct $\sum_{i \in S} f(x(i))$ in $C$.
Dually, the free category with finite products generated by $\Lambda$ is $(Fin/\Lambda)^{op}$. For $C$ a category with finite products, the product-preserving extension of $f: \Lambda \to C$ to $(Fin/\Lambda)^{op} \to C$ will be denoted $f^-$.
A $\Lambda$-sorted Lawvere theory is a category with finite products $\Theta$ equipped with a finite-product preserving functor $k: (Fin/\Lambda)^{op} \to \Theta$ that is the identity on objects. (Thus we can think of $\Theta$ as having chosen products.)
Yes, this is “evil”, but it can be a convenient (and harmless) evil. Even in the usual one-sorted case, if we purge this evil, we can have a Lawvere theory in which the generic object $x$ is isomorphic to its square $x^2$. Whereas it is convenient to think of them as distinct so that $n$-ary operations in the theory are identified with morphisms $x^n \to x$, and the arity is well-defined. But anyone who is offended by this evil can rewrite matters, at the cost of some extra words (replacing “identity/bijective on objects” with “essentially surjective”).
As usual, a model of a Lawvere theory $\Theta$ in a category with finite products $C$ is a product-preserving functor $F: \Theta \to C$. A homomorphism of models is a natural transformation between such functors. Thus we define the category of models,
and there is a forgetful functor $Mod_C(\Theta) \to C^\Lambda$ obtained by an obvious composition:
We will prove
Let $C$ be a category which admits general colimits and finite products that distribute over colimits. Then the forgetful functor $Mod_C(\Theta) \to C^\Lambda$ is monadic.
There are a number of ways of proving this theorem. One idea is to invoke a monadicity theorem, say a crude monadicity theorem, and in fact we will pursue this first. If all we are after is monadicity, then this approach is arguably overkill: the monadicity can be proved in a much “softer” and more direct fashion (by adapting some of Kelly’s ideas on operad theory). This approach is touched upon here; perhaps at some point we’ll go through it in more detail. However, an extra bonus of the approach via crude monadicity is that it makes cocompleteness of $Mod_C(\Theta)$ immediate, by an old result of Linton.
Recall the crude monadicity theorem: a functor $U: A \to B$ is monadic if
$U$ has a left adjoint $F: B \to A$,
The category $A$ has reflexive coequalizers,
The functor $U: A \to B$ preserves reflexive coequalizers and reflects isomorphisms.
In the case of the forgetful functor $U: \mathbf{Prod}(\Theta, C) \to C^\Lambda$, these conditions are not difficult to check, although for our purposes the existence of the left adjoint will require some preface, so we save this for later.
$U: \mathbf{Prod}(\Theta, C) \to C^\Lambda$ reflects isomorphisms.
On account of $\mathbf{Prod}((Fin/\Lambda)^{op}, C) \simeq C^\Lambda$, this is equivalent to saying the functor $G: \mathbf{Prod}(\Theta, C) \to \mathbf{Prod}((Fin/\Lambda)^{op}, C)$, induced from the product-preserving functor $k: (Fin/\Lambda)^{op} \to \Theta$, reflects isomorphisms.
Suppose $M, N: \Theta \to C$ are product-preserving functors and $\psi: M \to N$ is a natural transformation, such that the whiskering $\psi k: M k \to N k$ is invertible. But such a natural transformation is invertible iff all its components $\psi k (x)$ are invertible. Since $k$ is the identity on objects, this means each component $\psi (x)$ is invertible, so $\psi$ itself is invertible, as was to be shown.
Suppose $C$ has finite products and reflexive coequalizers, and that products distribute over reflexive coequalizers. Then the product functor $C \times C \to C$ preserves reflexive coequalizers.
The following proof is based on a neat argument given by Steve Lack. Another proof may be based on lemma 0.17 from Johnstone’s Topos Theory, page 4 (you can see it by looking inside the book at Amazon).
The walking reflexive fork $a \to b \stackrel{\to}{\to} a$ is a sifted category $D$, meaning precisely that the diagonal functor $\Delta: D \to D \times D$ is a final functor. (See Adámek, Rosický, Vitale for basic information on sifted categories and sifted colimits; see particularly their example 1.2.)
Now suppose we have a reflexive fork diagram $D \to C \times C$ given by two reflexive fork diagrams $F, G: D \to C$ in our category $C$. We have
where the first two isomorphisms are come from products distributing over reflexive coequalizers, the third comes from a “Fubini theorem”, and the last from the finality of $\Delta: D \to D \times D$. This shows the product applied to a reflexive coequalizer of $\langle F, G\rangle: D \to C \times C$ is canonically isomorphic to the reflexive coequalizer of the product $F \times G: D \to C$, as was to be shown.
If products distribute over reflexive coequalizers in $C$, then $\mathbf{Prod}(\Theta, C)$ admits reflexive coequalizers and $U: \mathbf{Prod}(\Theta, C) \to C^\Lambda$ preserves them.
Let $[\Theta, C]$ denote the category of all functors $\Theta \to C$; this certainly has reflexive coequalizers if $C$ has them. For any category $A$, let $A^D$ be the category of reflexive fork diagrams in $A$. Let
be the full inclusion. We show $\mathbf{Prod}(\Theta, C)$ is closed under reflexive coequalizers as computed in $[\Theta, C]$, i.e., that the composite (where “$colim$” means coequalizer)
factors through the full inclusion $j: \mathbf{Prod}(\Theta, C) \hookrightarrow [\Theta, C]$. This will mean both that $\mathbf{Prod}(\Theta, C)$ has reflexive coequalizers and that $j$ preserves them, whence $U$ which is the composite
also preserves them.
But if $\theta_1, \theta_2$ are two objects of $\Theta$, and if $F: D \to \mathbf{Prod}(\Theta, C)$ is a reflexive fork, then $colim\; j F$ preserves the product $\theta_1 \times \theta_2$ since
where the first and last isomorphisms hold since colimits in $[\Theta, C]$ are computed pointwise, the second isomorphism holds by the lemma, and the third holds since each $F(d): \Theta \to C$ is product-preserving.
Now we show that $U: \mathbf{Prod}(\Theta, C) \to C^\Lambda$ has a left adjoint $Free: C^\Lambda \to \mathbf{Prod}(\Theta, C)$, under the following assumptions
$C$ has all colimits (we don’t actually need all, but that’s certainly the most natural assumption),
$C$ has finite products, and
Products distribute over colimits.
We will call such a category cartesian monoidally cocomplete, or CMC. (Another name for it could be ‘cartesian 2-rig’, and indeed some of the material below is a cartesian analogue of the formalism of typed operads in the context of 2-rigs; see Baez-Dolan, section 2.3.)
It’s possible to dive right in and write down a coend formula for the asserted left adjoint $Free$, but it is clarifying to introduce it by telling a little abstract story. The basic theme is the idea of the free cartesian monoidally cocomplete category on a set $\Lambda$ and suitable monads thereon as being “$\Lambda$-typed cartesian operads”; this kind of idea has been used by various authors (Kelly, Baez-Dolan) in the symmetric monoidal case instead of the cartesian monoidal case undertaken here, but the development is conceptually almost identical. We will see that typed or multisorted Lawvere theories canonically give rise to such typed cartesian operads.
Let $D$ be a category with finite products. For CMC categories $A, B$, let $\mathbf{CMC}(A, B)$ denote the category of finite-product preserving, cocontinuous functors between them. Then, if $D$ is a category with finite products, then the Day convolution product on $Set^{D^{op}}$ induced by the cartesian monoidal structure on $D$ is also cartesian, and $Set^{D^{op}}$ is CMC. Furthermore, $Set^{D^{op}}$ is the free CMC category generated by $D$ as a cartesian monoidal category, in the sense that for any CMC category there is an equivalence
which takes a finite-product preserving functor $H: D \to C$ to the left Kan extension $\widehat{H}$, of $H$ along the Yoneda embedding $D \to Set^{D^{op}}$.
I won’t go through the proof here (which is outlined for example here), but it will be handy to recall the coend formula for the left Kan extension: it is
where $W: D^{op} \to Set$ is a weight over $D$.
$Set^{Fin/\Lambda}$ is the free cartesian monoidally cocomplete category generated by the discrete category $\Lambda$.
The point is that for a cartesian monoidally cocomplete $C$, there are equivalences of categories
both of which have been described above. Putting them together: there is in the first place, for each typing $f: \Lambda \to C$ an induced finite-product preserving map $f^-: (Fin/\Lambda)^{op} \to C$; here we think of $f^x$ as being a fiberwise finite power of $f$ if $x: S \to \Lambda$ is a finite set over $\Lambda$, i.e.,
where $x_\lambda$ denotes the fiber over $\lambda$. In the second place, we pass from $f^-$ to a CMC functor $Set^{Fin/\Lambda} \to C$ defined on weights $W: Fin/\Lambda \to Set$ by
Now for a key definition:
A $\Lambda$-typed or $\Lambda$-sorted cartesian operad is a monoid in the monoidal category $\mathbf{CMC}(Set^{Fin/\Lambda}, Set^{Fin/\Lambda})$ (taking endofunctor composition as the monoidal product and the identity as monoidal unit).
A principal moral of our story is that a $\Lambda$-typed cartesian operad is essentially the same thing as $\Lambda$-sorted Lawvere theory. We need just a little from that story here.
Let $\Theta$ be a $\Lambda$-sorted Lawvere theory (with canonical product-preserving functor $k: (Fin/\Lambda)^{op} \to \Theta$; recall also our earlier notation $\iota: \Lambda \to (Fin/\Lambda)^{op}$ for the canonical inclusion). The Lawvere theory $\Theta$ gives rise to a product-preserving functor $(Fin/\Lambda)^{op} \to Set^{Fin/\Lambda}$ defined by
According to our development, this gives rise to a CMC endofunctor which we denote $Op(\Theta): Set^{Fin/\Lambda} \to Set^{Fin/\Lambda}$:
Composition in $\Theta$ induces a monad multiplication for $Op(\Theta)$:
and similarly identities in $\Theta$ induce a monad unit for $Op(\Theta)$. This defines the cartesian operad associated with the Lawvere theory $\Theta$.
Let $C$ be a CMC category, and let $M: Set^{Fin/\Lambda} \to Set^{Fin/\Lambda}$ be a $\Lambda$-sorted cartesian operad. The monad induced by $M$ on $[\Lambda, C]$ is the monad $M_C$ obtained by transporting the monad
across the equivalence $\mathbf{CMC}(Set^{Fin/\Lambda}, C) \simeq [\Lambda, C]$.
Actually, it seems a good idea to overload the notation and use $M_C$ for any one of three monads induced by $M$:
since all three indicated categories are canonically equivalent – and let the choice be dictated by doctrinal needs.
In particular, to construct the free $\Theta$-model in $\mathbf{Prod}(\Theta, C)$ generated by a typing function $f: \Lambda \to C$, the obvious choice is the second. Here the monad
takes the product-preserving functor $f^-: (Fin/\Lambda)^{op} \to C$ to another product-preserving functor $(Fin/\Lambda)^{op} \to C$, which by following the formulas above is expressed by the coend
In essence this gives the free model generated by $f: \Lambda \to C$. More exactly, the free model (as a product-preserving functor $Free(f): \Theta \to C$) is just
This is manifestly a functor $\Theta \to C$.
$Free(f): \Theta \to C$ is product-preserving.
We already know that $Free(f) \circ k: (Fin/\Lambda)^{op} \to C$ is product-preserving, since that is exactly
and $Op(\Theta)_C$ was after all designed to land in product-preserving functors $\mathbf{Prod}((Fin/\Lambda)^{op}, C)$. But a functor $G: \Theta \to C$ is product-preserving iff $G \circ k$ is product-preserving: this is because product-preservation just comes down to preservation of projection and diagonal maps for all objects $x, y$ in $\Theta$, and all that projection and diagonal data is already contained in $(Fin/\Lambda)^{op}$ under the product-preserving “inclusion” $k: (Fin/\Lambda)^{op} \to \Theta$ (which we recall is the identity on objects).
$Free: [\Lambda, C] \to \mathbf{Prod}(\Theta, C)$ is left adjoint to $U: \mathbf{Prod}(\Theta, C) \to [\Lambda, C]$.
Suppose $M: \Theta \to C$ is product-preserving and that we have a natural transformation $Free(f) \to M$. We have natural bijections between families that are extranatural in the indicated arguments, as follows:
with both sides product-preserving in $x \in Ob((Fin/\Lambda)^{op})$. Under the equivalence $\mathbf{Prod}((Fin/\Lambda)^{op}, C) \simeq [\Lambda, C]$, the last is in natural bijection with maps
in $[\Lambda, C]$. This completes the proof, and thus also the proof of Theorem 1.
It goes without saying that if $C$ and therefore also $C^\Lambda$ is complete, then so is any monadic category over $C^\Lambda$ such as $Mod_C(\Theta)$. In general it is not true that a category that is monadic over a cocomplete category is itself cocomplete, but fortunately the following is true.
If $C$ is CMC, then the category of models $Mod_C(\Theta)$ is cocomplete for any $\Lambda$-sorted Lawvere theory $\Theta$.
It is an old result of Linton that if $B$ is cocomplete and $T$ is a monad on $B$, then the category of algebras $A = B^T$ is cocomplete if it has reflexive coequalizers. This applies here to give the desired conclusion, in view of Proposition 1, Theorem 1, and the fact that $C^\Lambda$ is cocomplete.
For convenience we reproduce a proof of Linton’s result here. Let $U: A \to B$ be monadic with left adjoint $F: B \to A$; let $T$ be the monad $U F$; let $\eta : 1_B \to U F$ be the unit and $\varepsilon: F U \to 1_A$ be the counit of the adjunction. First, a family of free $T$-algebras $\{F(c_i)\}_{i \in I}$ has a coproduct: it’s just $F(\sum_i c_i)$ since the left adjoint $F$ preserves coproducts.
Next, under our hypotheses, the category of $T$-algebras $A$ has arbitrary coproducts, because the coproduct of a family $\{a_i\}_{i \in I}$ of algebras can be exhibited as a coequalizer of a reflexive fork diagram consisting of coproducts of free algebras:
Finally, coequalizers (not just reflexive coequalizers) exist in $A$, because $A$ has binary coproducts, and the coequalizer of a general pair of arrows $a' \stackrel{\overset{f}{\to}}{\underset{g}{\to}} a$ can be computed as the coequalizer of the reflexive fork
As pointed out to me by Mike Shulman, the standard presentation of colimits in terms of coproducts and coequalizers is actually in terms of coproducts and reflexive coequalizers (being a truncation of a simplicial object, namely a two-sided bar construction). This observation can be used in lieu of the final paragraph of the proof above of Linton’s result.
Let $k: (Fin/\Lambda)^{op} \to \Theta$ and $k': (Fin/\Lambda)^{op} \to \Theta'$ be $\Lambda$-sorted Lawvere theories. A morphism of theories is a finite-product preserving functor $\Theta \to \Theta'$. This is the same as a functor $g: \Theta \to \Theta'$ such that $k' = g \circ k$ (since the projection and diagonal map data on objects of $\Theta$ are already in $(Fin/\Lambda)^{op}$, and $k, k'$ are product-preserving).
If $C$ is CMC and $g: \Theta \to \Theta'$ is a morphism of theories, then the functor
is monadic.
$g^\ast: \; \mathbf{Prod}(\Theta', C) \to \mathbf{Prod}(\Theta, C)$ preserves reflexive coequalizers and reflects isomorphisms (we already know $\mathbf{Prod}(\Theta', C)$ has reflexive coequalizers).
That $g^\ast$ reflects isomorphisms is easy: given that $g^\ast(f)$ is an iso, then also $k^\ast g^\ast(f) = (k')^\ast(f)$ is an iso, whence $f$ is an iso since $(k')^\ast$ reflects isos.
Similarly, suppose $i, j$ is a reflexive pair of maps $M \to N$ in $\mathbf{Prod}(\Theta', C)$, with coequalizer $p: N \to P$, and suppose the reflexive pair $g^\ast(i), g^\ast(j)$ in $\mathbf{Prod}(\Theta, C)$ has coequalizer $q: g^\ast(N) \to Q$. Then there is a unique map $r: Q \to g^\ast(P)$ such that $g^\ast(p) = r \circ q$; to show $g^\ast$ preserves reflexive coequalizers, we must show $r$ is an iso. Since $k^\ast$ preserves reflexive coequalizers, we see $k^\ast(q)$ is the coequalizer of
as is $(k')^\ast(p) = k^\ast g^\ast(p)$ since $(k')^\ast$ preserves reflexive coequalizers. This implies $k^\ast(r)$ is an iso, and so $r$ is an iso since $k^\ast$ reflects isos.
We invoke the crude monadicity theorem; in view of the preceding lemma, the only hypothesis left to verify is the existence of a left adjoint to $g^\ast$. But this clearly follows from the adjoint triangle theorem.
The consideration of CMC categories closely parallels the development of operad theory in terms of 2-rigs given here:
The preceding article was discussed further (with some errors corrected) in
Eugenia Cheng, The category of opetopes and the category of opetopic sets, Th. Appl. Cat. 11 (2003), 353–374. arXiv)
Tom Leinster, Structures in higher-dimensional category theory. (arXiv)
Also providing a template for the abstract consideration of cartesian monoidally cocomplete categories is the seminal article of Kelly: