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.