Coherence theorem for symmetric lax monoidal functors

Question

Let $V$ and $W$ be symmetric monoidal categories. Let $F:V\to W$ be a lax symmetric monoidal functor with multiplication $\nabla:FA\otimes FB \to F(A\otimes B)$. Consider the following statements:

1) There are lax symmetric monoidal functors $F(-)^{\otimes n}:V\to W$ and $F((-)^{\otimes n}):V\to W$ for each $n\geq 2$,

2) There is a lax monoidal transformation $F(-)^{\otimes n} \Rightarrow F((-)^{\otimes n})$.

They seems plausible to me. For example, if $n=2$ these things are a long but doable diagram chase. As $n$ gets bigger, it gets more and more unwieldy to actually verify it by hand.

It seems to me this is a sort of "coherence theorem". For example, consider the second statement for $n=3$. There are two reasonable natural transformations to define by suitably tensoring $\nabla$ with the identity, yet they are equal by associativity of $F$. As $n$ grows, the amount of "obvious but provably equal" options for defining the natural transformation grows.

Are these statements true, and how might one go about actually proving them?

Note: there is a hidden (iterated) diagonal which might be a red herring. We could be considering the functors in 1) to be $V^{\times n}\to W$.

Answer 1

I think they are true.

First of all, let's break out the diagonal as you suggested by writing $(-)^{\otimes n}:V\to V$ as the composite $V \xrightarrow{\Delta} V^n \xrightarrow{\otimes_n} V$. Since the 2-category of symmetric monoidal categories and lax symmetric monoidal functors has finite products, $F$ commutes with the $\Delta$'s (which are strict monoidal), so it suffices to show that $\otimes_n$ is monoidal and that we have a symmetric monoidal transformation (it doesn't make sense for a transformation to be "lax") $F \circ \otimes_n \to \otimes_n \circ F^n$.

Now, it's fairly straightforward to show that if $V$ is symmetric monoidal, then $\otimes : V\times V\to V$ is strong monoidal. By taking products with the identity and composing, we find that $\otimes_n : V^n \to V$ is also strong monoidal, and therefore $F\circ \otimes_n$ and $\otimes_n\circ F^n$ are lax monoidal.

More generally, if $X$ is a symmetric pseudomonoid in any 2-category with products, then $\otimes :X\times X\to X$ is strong monoidal, and hence so is $\otimes_n:X^n \to X$. But a lax symmetric monoidal functor can be identified with a symmetric pseudomonoid in the 2-category $\mathrm{Oplax}(\mathbf{2},\mathrm{Cat})$ whose objects are the arrows of Cat (functors) regarded as functors from the interval category $\mathbf{2}$ to Cat, and whose morphisms are oplax transformations (which here are just 2-cells fitting in a square). Similarly, a strong symmetric monoidal morphism in that 2-category can be identified with a symmetric monoidal transformation $G\circ F \to F'\circ H$ where $G$ and $H$ are strong symmetric monoidal and $F$ and $F'$ are lax symmetric monoidal. Thus, applying the general result about symmetric pseudomonoids to our $F$, we get the desired transformation.