MacLane’s coherence theorem and free monoidal categories

adjoint-functorscategory-theoryfunctorsmonoidal-categories

Original question
The nLab gives one formulation of the coherence theorem for monoidal categories:

Every diagram in a free monoidal category made up of associators and unitors commutes.

It seems to me in practice this coherence theorem is often used as follows:
One has a diagram on a set of objects $S$ of a specific monoidal category $(C,\otimes,I)$ made up from the associators and unitors of $C$. One then considers this diagram "in the free monoidal category on $S$." Subsequently, one argues that since the diagram in the free monoidal category commutes, so does the original diagram.

How do you make this sketch of an argument precise? I tried using the universal property of „the free monoidal category“ – to no avail.

Edit:
In his answer Jonas suggested that any monoidal category is the quotient of a free monoidal category. Is this true? In the context of group theory this is easily proved using the universal property of the free group and the first isomorphism theorem for groups. Does an analogue of the isomorphism theorem hold for (monoidal) categories?

Best Answer

The free monoidal category $\mathbb M A$ on a set $A$ has the following universal property. For every monoidal category $\mathbf C$ and function $f \colon A \to |\mathbf C|$, there is a unique monoidal functor $\tilde f \colon \mathbb M A \to \mathbf C$ such that $\tilde f \circ \eta_A = f$, where $\eta_A \colon A \to \mathbb M A$ is the inclusion (concretely, $\mathbb M A$ has as its objects lists of objects in $A$, and $\eta_A$ sends $a \mapsto [a]$).

A diagram in the free monoidal category on $A$ is simply a pair of morphisms $\ell, r \colon x \to y$ in $\mathbb M A$. Conceptually, these are built inductively from the structural isomorphisms $\alpha$, $\lambda$, and $\rho$.

A formal diagram in a monoidal category $\mathbf A$ is simply a diagram in $\mathbb M(|\mathbf A|)$. We have a canonical functor $\mathbb M(|\mathbf A|) \to \mathbf A$ given by the universal property of the free monoidal category. Therefore, a formal diagram in $\mathbf A$ is sent to a pair of morphisms in $\mathbf A$. Since the morphisms in the free monoidal category were constructed inductively from structural isomorphisms, so will be the morphisms in $\mathbf A$ in the image of the functor.

However, the coherence theorem says that necessarily that for any diagram $\ell, r$ in the free monoidal category, we have $\ell = r$. Since functors preserve equality of morphisms, the functor $\mathbb M(|\mathbf A|) \to \mathbf A$ sends any diagram to an equal pair of morphisms in $\mathbf A$. Therefore any formal diagram in $\mathbf A$ commutes.

Related Question