It is well know that the triple $(Sp,\wedge,\mathbb{S} )$ composed by the $\infty$-category of spectra, the smash product and sphere spectrum is a monoidal $\infty$-category. In particular, this implies that there exists the free-forgetfull adjunction equivalence of $\infty$-categories $F:Sp\cong Mod_{\mathbb{S}}(Sp):U$ where, for $m\in Sp$, $F(m)=(m,\alpha_{m}:\mathbb{S}\wedge m\cong m)$ is the pair composed by the starting $m$ and $\alpha$ is unit-isomorphism in $Sp$.
It is also well know that the triple $(Mod_{\mathbb{S}}(Sp), \otimes, \mathbb{S})$ whose second componet is the relative tensor product between modules (i.e. for each $A,B\in Mod_{\mathbb{S}}(Sp)$ the relative tensor product is $B\otimes A = |Bar(A,B)_*|$) is a monoidal $\infty$-category.
My question is the following: are $F$ and $U$ two strong monoidal funtors? Or in other words, $F$ (or equivalently $U$) is an monoidal equivalence?
My guest is yes and now I explain why. We denote with a pair $(X,\alpha_{X})$ an object of $Mod_{\mathbb{S}}(Sp)$ where the first component is an objects of $Sp$ and the second one is the action. Since $F\dashv U$ is an equivalence every action, i.e. $m_{X}$, is trivial and then two objects (X,\alpha_{X}) (Y,\alpha_{Y}) of $Mod_{\mathbb{S}}(Sp)$ are equivalent iff their first components are equivalent: i.e. if they are equivalent in $Sp$ $X\cong U((X,\alpha_{X}))\cong U((Y,\alpha_{Y}))\cong Y$
Let $m,n\in Sp$, we know that the first component of $F(m)\otimes F(n)\in Mod_{\mathbb{S}}(Sp)$ is $|Bar(F(m),F(n))_{*}|$ which is a colimits in $Sp$. All the component of the simplicial object $Bar(F(m),F(n))_{*}$ are equivalent to $m\wedge n$ and all the face and degeneracy arrows are isomorphisms, hence this colimits is exactly $m\wedge n$. In particular, this means that $F(m)\otimes F(n)\cong F(m\wedge n)\cong (m\wedge n,\alpha_{m\wedge n}:m\wedge n\wedge \mathbb{S}\cong m\wedge n )$.
Yes, this is true. Your bar construction argument shows (observing naturality in both arguments) that the diagram $$ \require{AMScd} \begin{CD} \mathrm{LMod}_\mathbb{S}\times\mathrm{LMod}_\mathbb{S} @>{-\otimes-}>>\mathrm{LMod}_\mathbb{S}\\ @V{U}VV @VV{U}V\\ \mathsf{Sp}\times\mathsf{Sp}@>{-\otimes-}>>\mathsf{Sp} \end{CD} $$ commutes, so in particular $U$ is a strongly monoidal functor. The functor $F$ is the inverse of a functor $U$ that admits a strongly monoidal refinement, and therefore also admits a strongly monoidal refinement by formal reasons (namely by flipping the vertical arrows in the above diagram).