Suppose $F: \mathcal{O}^\otimes \to \mathcal{P}^\otimes$ is a map of $\infty$-operads, and $\mathcal{C}$ is a symmetric monoidal $\infty$-category that admits small colimits, such that the tensor product preserves small colimits in both variables separately. Corollary 3.1.3.5 in Lurie's "Higher Algebra" shows that the forgetful functor $\operatorname{Alg}_{\mathcal{P}}(\mathcal{C}) \to \operatorname{Alg}_{\mathcal{O}}(\mathcal{C})$ induced by precomposition with $F$ admits a left adjoint $$ \operatorname{Free}: \operatorname{Alg}_{\mathcal{O}}(\mathcal{C}) \to \operatorname{Alg}_{\mathcal{P}}(\mathcal{C}) $$ sending a $\mathcal{O}$-algebra to the free $\mathcal{P}$ algebra generated by it. Both $\operatorname{Alg}_{\mathcal{O}}(\mathcal{C})$ and $\operatorname{Alg}_{\mathcal{P}}(\mathcal{C})$ admit canonical symmetric monoidal structures via the tensor product of algebras in HA Example 3.2.4.4. My question is the following: Is the free algebra functor $\operatorname{Free}$ symmetric monoidal?
My issue in showing this is mostly that the definition of the tensor product of algebras above is done via a simplicial construction, and Lurie doesn't seem to give any universal property that characterizes it. Therefore, before I delve too deep into a simplicial calculation that indicates to become pretty hard, I wanted to ask whether anyone has a different idea about how to show this statement, or knows about such a universal property that might help me.
Edit: Let me sketch a first attempt at a partial answer. For $K \to \operatorname{Fin}$ any simplicial set over the category of finite pointed sets, write $K^\flat$ for the associated preoperad where only identity morphisms are marked. Also, write $\operatorname{Op}(L)^\otimes$ for the fibrant replacement of a preoperad, i.e., the associated $\infty$-operad.
To obtain a map of simplicial sets over $\operatorname{Fin}$, by the definition of the symmetric monoidal structure on $\operatorname{Alg}_{\mathcal{O}}(\mathcal{C})$ we can equivalently give a natural map in $K$ $$ \operatorname{Hom}^{\natural}_{\operatorname{sSet}_{/\operatorname{Fin}}}(K^\flat \odot\mathcal{O}^\natural, \mathcal{C}^\natural) \to \operatorname{Hom}^{\natural}_{\operatorname{sSet}_{/\operatorname{Fin}}}(K^\flat \odot\mathcal{P}^\natural, \mathcal{C}^\natural)$$ where $\mathcal{O}^\natural$ denotes the inert marking, and $\odot$ is the tensor product from HA Notation 2.2.5.5. Such a map exists, namely since fibrant replacement is left adjoint to the inclusion of operads into preoperads, one can use the free algebra functor for the map of operads $$\operatorname{Op}(K^\flat \odot\mathcal{O}^\natural)^\otimes = \operatorname{Op}(K^\flat)^\otimes \otimes \mathcal{O}^\otimes \to \operatorname{Op}(K^\flat \odot\mathcal{P}^\natural)^\otimes$$ for this purpose, which on $K = \operatorname{Fin}$ recovers the free algebra functor we are looking for.
It is however not clear that this map sends coCartesian morphisms to coCartesian morphisms. As a reminder, a morphism $\alpha$ in $\operatorname{Alg}_{\mathcal{O}}(\mathcal{C})$ is coCartesian iff for all $O$ in the underlying category of $\mathcal{O}$, the induced morphism $\alpha(O)$ in $\mathcal{C}^\otimes$ is coCartesian, by HA 3.2.4.3.