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](http://www.emis.de/journals/TAC/volumes/6/n7/6-07abs.html), 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.



Left adjoint to the forgetful functor from finite product categories to symmetric monoidal categories
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.


