# Coherence theorem for symmetric lax monoidal functors

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$.

• I don't have this to hand to properly verify this would answer your question, but have you looked at: Geoffrey Lewis, Coherence for a closed functor, LNM 281 (Springer, 1972) 148-195? – Todd Trimble Jun 30 '16 at 12:57
• @ToddTrimble: thanks for the reference, I'm having a look. (It's a bit hard to read, though. I'd never heard of clubs). – Bruno Stonek Jun 30 '16 at 13:26
• The rough idea of club is that if you understand (for certain categorical doctrines) the free structure on one element, then the free structure on more general categories can be gotten by a wreath product construction. There was a lot of work on this in the early 70's, in the "Australian school" headed by Max Kelly. – Todd Trimble Jun 30 '16 at 13:31

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.