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 be the inclusion of the category of finite sets into the category of all sets. Let be a set, and let , or just , be the comma category whose objects are pairs where is a finite set.
We can think of such a pair as a finite set fibered over , so that all but finitely many fibers are empty. The category has finite coproducts (they are just coproducts in each separate fiber).
A key fact we need is that is the free category with finite coproducts generated by . More formally: treat the set as a discrete category; there is an evident functor which takes to the evident fibered set .
Let be a category with finite coproducts, and let be a functor. There is (up to unique isomorphism) a unique coproduct-preserving functor that extends along . If has chosen coproducts, we can demand preservation on the nose.
The idea of proof is that takes a fibered set to the coproduct in .
Dually, the free category with finite products generated by is . For a category with finite products, the product-preserving extension of to will be denoted .
A -sorted Lawvere theory is a category with finite products equipped with a finite-product preserving functor that is the identity on objects. (Thus we can think of 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 is isomorphic to its square . Whereas it is convenient to think of them as distinct so that -ary operations in the theory are identified with morphisms , 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 in a category with finite products is a product-preserving functor . A homomorphism of models is a natural transformation between such functors. Thus we define the category of models,
and there is a forgetful functor obtained by an obvious composition:
We will prove
Let be a category that admits general colimits and finite products that distribute over colimits. Then the forgetful functor 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 immediate, by an old result of Linton.
Recall the crude monadicity theorem: a functor is monadic if
has a left adjoint ,
The category has reflexive coequalizers,
The functor preserves reflexive coequalizers and reflects isomorphisms.
In the case of the forgetful functor , 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.
reflects isomorphisms.
On account of , this is equivalent to saying the functor , induced from the product-preserving functor , reflects isomorphisms.
Suppose are product-preserving functors and is a natural transformation, such that the whiskering is invertible. But such a natural transformation is invertible iff all its components are invertible. Since is the identity on objects, this means each component is invertible, so itself is invertible, as was to be shown.
Suppose has finite products and reflexive coequalizers, and that products distribute over reflexive coequalizers. Then the product functor 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 is a sifted category , meaning precisely that the diagonal functor 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 given by two reflexive fork diagrams in our category . 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 . This shows the product applied to a reflexive coequalizer of is canonically isomorphic to the reflexive coequalizer of the product , as was to be shown.
If products distribute over reflexive coequalizers in , then admits reflexive coequalizers and preserves them.
Let denote the category of all functors ; this certainly has reflexive coequalizers if has them. For any category , let be the category of reflexive fork diagrams in . Let
be the full inclusion. We show is closed under reflexive coequalizers as computed in , i.e., that the composite (where “” means coequalizer)
factors through the full inclusion . This will mean both that has reflexive coequalizers and that preserves them, whence which is the composite
also preserves them.
But if are two objects of , and if is a reflexive fork, then preserves the product since
where the first and last isomorphisms hold since colimits in are computed pointwise, the second isomorphism holds by the lemma, and the third holds since each is product-preserving.
Now we show that has a left adjoint , under the following assumptions
has all colimits (we don’t actually need all, but that’s certainly the most natural assumption),
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 , 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 and suitable monads thereon as being “-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 be a category with finite products. For CMC categories , let denote the category of finite-product preserving, cocontinuous functors between them. Then, if is a category with finite products, then the Day convolution product on induced by the cartesian monoidal structure on is also cartesian, and is CMC. Furthermore, is the free CMC category generated by as a cartesian monoidal category, in the sense that for any CMC category there is an equivalence
which takes a finite-product preserving functor to the left Kan extension , of along the Yoneda embedding .
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 is a weight over .
is the free cartesian monoidally cocomplete category generated by the discrete category .
The point is that for a cartesian monoidally cocomplete , there are equivalences of categories
both of which have been described above. Putting them together: there is in the first place, for each typing an induced finite-product preserving map ; here we think of as being a fiberwise finite power of if is a finite set over , i.e.,
where denotes the fiber over . In the second place, we pass from to a CMC functor defined on weights by
Now for a key definition:
A -typed or -sorted cartesian operad is a monoid in the monoidal category (taking endofunctor composition as the monoidal product and the identity as monoidal unit).
A principal moral of our story is that a -typed cartesian operad is essentially the same thing as -sorted Lawvere theory. We need just a little from that story here.
Let be a -sorted Lawvere theory (with canonical product-preserving functor ; recall also our earlier notation for the canonical inclusion). The Lawvere theory gives rise to a product-preserving functor defined by
According to our development, this gives rise to a CMC endofunctor which we denote :
Composition in induces a monad multiplication for :
and similarly identities in induce a monad unit for . This defines the cartesian operad associated with the Lawvere theory .
Let be a CMC category, and let be a -sorted cartesian operad. The monad induced by on is the monad obtained by transporting the monad
across the equivalence .
Actually, it seems a good idea to overload the notation and use for any one of three monads induced by :
since all three indicated categories are canonically equivalent – and let the choice be dictated by doctrinal needs.
In particular, to construct the free -model in generated by a typing function , the obvious choice is the second. Here the monad
takes the product-preserving functor to another product-preserving functor , which by following the formulas above is expressed by the coend
In essence this gives the free model generated by . More exactly, the free model (as a product-preserving functor ) is just
This is manifestly a functor .
is product-preserving.
We already know that is product-preserving, since that is exactly
and was after all designed to land in product-preserving functors . But a functor is product-preserving iff is product-preserving: this is because product-preservation just comes down to preservation of projection and diagonal maps for all objects in , and all that projection and diagonal data is already contained in under the product-preserving “inclusion” (which we recall is the identity on objects).
is left adjoint to .
Suppose is product-preserving and that we have a natural transformation . We have natural bijections between families that are extranatural in the indicated arguments, as follows:
with both sides product-preserving in . Under the equivalence , the last is in natural bijection with maps
in . This completes the proof, and thus also the proof of Theorem 1.
It goes without saying that if and therefore also is complete, then so is any monadic category over such as . 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 is CMC, then the category of models is cocomplete for any -sorted Lawvere theory .
It is an old result of Linton that if is cocomplete and is a monad on , then the category of algebras 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 is cocomplete.
For convenience we reproduce a proof of Linton’s result here. Let be monadic with left adjoint ; let be the monad ; let be the unit and be the counit of the adjunction. First, a family of free -algebras has a coproduct: it’s just since the left adjoint preserves coproducts.
Next, under our hypotheses, the category of -algebras has arbitrary coproducts, because the coproduct of a family 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 , because has binary coproducts, and the coequalizer of a general pair of arrows 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 and be -sorted Lawvere theories. A morphism of theories is a finite-product preserving functor . This is the same as a functor such that (since the projection and diagonal map data on objects of are already in , and are product-preserving).
If is CMC and is a morphism of theories, then the functor
is monadic.
preserves reflexive coequalizers and reflects isomorphisms (we already know has reflexive coequalizers).
That reflects isomorphisms is easy: given that is an iso, then also is an iso, whence is an iso since reflects isos.
Similarly, suppose is a reflexive pair of maps in , with coequalizer , and suppose the reflexive pair in has coequalizer . Then there is a unique map such that ; to show preserves reflexive coequalizers, we must show is an iso. Since preserves reflexive coequalizers, we see is the coequalizer of
as is since preserves reflexive coequalizers. This implies is an iso, and so is an iso since 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 . 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: