# Left adjoint to the forgetful functor from finite product categories to symmetric monoidal categories

I recall reading that the forgetful functor $FinProdCat \to SymMonCat$ from categories with finite products and product preserving functors to symmetric monoidal categories and tensor preserving functors has a left adjoint.

To make this precise one has to insert lax, weak or strict in several places -- I am interested in any combination of these (but most in a 2-adjunction between the categories with weakly product, resp. tensor, preserving functors).

Is something like this true at all? If so, can anyone give a true and precise statement and/or a reference? I wouldn't mind getting a concrete description of the left adjoint, but a confirmation of its existence would already be a treat.

Thanks!

(This is not a case of google laziness: I spent half a day looking for reference. I would imagine that the statement emerges after inserting the right things into long known results about enriched base change or 2-monads, but I wasn't able to find the right one)

EDIT: What would be nice would be an argument along these lines: Both Symmetric monoidal categories and finite product categories are algebras for certain pseudomonads. Algebras for pseudomonads are are finite copower preserving functors from Cat-enriched Lawvere theories, see Power's Enriched Lawvere Theories, Thm 3.4. There should be a map (sort of an inclusion, since we demand less structure for a symmetric monoidal category) from the Lawvere theory for symmetric monoidal categories to that for finite product categories and the forgetful functor should be precomposition with it. Now the left adjoint could be obtained by taking Cat-enriched left Kan extensions along this map.

One problem is that I only know that left Kan extensions of product preserving functors along product preserving functors are product preserving again, but I don't know the corresponding statement for copowers. This could either be true or for our special Lawvere theories it could be enough to ask for product preserving functors, then the above might have a chance to work.

-
By the way: I don't mean the right adjoint to the forgetful functor - for this see e.g. this article of Hyland and Power: Symmetric Monoidal Sketches dpmms.cam.ac.uk/~martin/Research/Oldpapers/hp00.pdf –  Peter Arndt Apr 2 '12 at 14:23
@Peter: Thank you very much for pointing me to this article; in the last days I wondered if there is a theory of "generators and relations" for symm. mon. cat.; see also mathoverflow.net/questions/92897. Sorry for this offtopic comment. But even in this case I would first observe that every symmetric monoidal category defined by generators and relations should be mapped to the corresponding finite product category with the same generators and relations. For example, the permutation groupoid gets mapped to the discrete category $\mathbb{N}$; both are free on one generator. –  Martin Brandenburg Apr 2 '12 at 14:34
If you add enough "niceness" conditions on a category, a fantastic way to improve a symmetric monoidal category to one where the tensor product is given by cartesian product is to consider the category of cocommutative coalgebras in your original category. But I think this construction is right-adjoint to forgetting from cartesian to symmetric monoidal. In order for a left adjoint to exist, it had better be true that any (2-)limit of finite product categories is also the limit of underlying symmetric monoidal categories. How confident are you in this? –  Theo Johnson-Freyd Apr 2 '12 at 16:23
@Martin: Good thought! The presentations and relations should help me compute the left adjoint in my cases. For the permutation groupoid it should give the opposite of the category of finite sets, though. –  Peter Arndt Apr 2 '12 at 17:52
@Theo: Yes, that is the - admittedly very neat - right adjoint. It seems to be true that the forgetful functor preserves limits, so I'm keeping my fingers crossed. –  Peter Arndt Apr 2 '12 at 17:53

The 2-categories of finite-product categories and symmetric-monoidal categories are both 2-monadic over $\mathrm{Cat}$, in all possible senses. That is, there are strict 2-monads $P$ and $S$ on $\mathrm{Cat}$ such that $P$-algebras and strict, pseudo, lax, and colax $P$-morphisms coincide with finite-product categories and their morphisms, and likewise for $S$-algebras and symmetric-monoidal categories. Moreover, both $P$ and $S$ are finitary, and we have a 2-monad morphism $S\to P$ which induces your forgetful functor(s) on categories of algebras.

First consider the strict case: (strict) limits of both $P$-algebras and $S$-algebras (and strict morphisms) are created in $\mathrm{Cat}$, so the forgetful functor preserves strict limits. Thus, since the 2-categories of $P$- and $S$-algebras and strict morphisms are locally presentable, this functor has a (strict) left adjoint.

The pseudo case requires some more work. One could in theory mimic the above argument entirely in the world of 2-categories, but I don't know if the machinery has been set up for that yet. Alternatively, one can use pseudo-morphism classifiers to reduce the problem to the strict case. This is done in the classic Blackwell-Kelly-Power paper "Two-dimensional monad theory", Theorem 5.12. (They state the strict case as Theorem 3.9.)

I have no idea whether the lax or colax cases are true; offhand I would say it seems unlikely.

-
Thank you! (I wrote the edit to my question before seeing your answer - I will look at Blackwell-Kelly-Power now) –  Peter Arndt Apr 2 '12 at 17:56
Everytime I encounter 2-monad theory (and various special cases thereof) I don't understand how one can make any of these general constructions explicit. Even for me, and I like category theory a lot, it is still impossible to understand any paper in this area. I wonder why. –  Martin Brandenburg Apr 2 '12 at 18:16
So let me pose this specific question: Even if there is some fancy theory which yields the existence of the left adjoint, how can we write it down? I mean something explicit which is not defined by generators and relations. For example, the right adjoint is explicit, it is just $C \mapsto \mathrm{CMon}(C)$. –  Martin Brandenburg Apr 2 '12 at 18:19
@Martin: Unfortunately, frequently adjoint functors don't have very nice descriptions. Look at a proof of the adjoint functor theorem; in many cases that's as explicit of a "construction" as you're going to get. In the locally presentable case, the adjoint can usually be defined as a certain transfinite colimit; maybe you'd like that better? –  Mike Shulman Apr 2 '12 at 19:29
Thm. 5.12 did it for me - thanks a lot. –  Peter Arndt Apr 2 '12 at 22:43