# The Unapologetic Mathematician

## The “Strictification” Theorem

I want to get in another post in the current line before I head off to Portugal on Tuesday. This theorem is another heavy one to prove, so if the proof of the Coherence Theorem was overwhelming you might just want to skim this one and remember the result: Any monoidal category $\mathcal{M}$ is monoidally equivalent to a strict monoidal category $\mathcal{S}$ — one whose objects form an honest monoid without any “up to isomorphism” dodging about. This will justify the usual laxity with which we treat associativity and unit laws in monoidal categories, writing $A\otimes B\otimes C\otimes\cdots$ without regard to parentheses and such.

When we naively write down a monoidal product like this we’re treating it as a list of objects of $\mathcal{M}$, and we take the product of two lists just by concatenation. So let’s start by defining the collection of objects of $\mathcal{S}$ to be the free monoid on the objects of $\mathcal{M}$, which is exactly this collection of lists. We’ll write a typical list as $A=[A_1,A_2,...,A_m]$. Then we have the concatenation product $\left[A_1,...A_m\right]\cdot\left[B_1,...B_n\right]=\left[A_1,...A_m,B_1,...,B_n\right]$ and the empty list $\left[\right]$ for an identity object. All the monoid rules hold “on the nose” already, so we don’t need to worry about associators and all.

We don’t have any arrows in our category yet, but let’s press on a bit first to define a map $F:\mathcal{S}\rightarrow \mathcal{M}$. If this has any hope of being the object function of a monoidal functor we’ll need $F([])=\mathbf{1}$. We also need to figure out how $F$ should deal with a monoidal product. What we’re going to do is just choose to make the result have all its parentheses on the right. We define $F([A_1,A_2,...])=A_1\otimes F([A_2,...])$ to get (for example) $F([A_1,A_2,A_3,A_4])=A_1\otimes(A_2\otimes(A_3\otimes A_4))$.

Now we’ll go back and add arrows to $\mathcal{S}$ in just such a way as to make $F$ into a monoidal functor. Given two lists $A$ and $B$ in $\mathcal{S}$ I’ll define $\hom_\mathcal{S}(A,B)=\hom_\mathcal{M}(F(A),F(B))$. Notice that this makes the functor $F$ fully faithful by definition, and that every object $M$ in $\mathcal{M}$ is $F([M])$, so we’re well on our way to having an equivalence of categories!

What’s missing now? Well, we still don’t know quite how to take the monoidal product of arrows in $\mathcal{S}$, so it’s still not quite a monoidal category yet. We can use the isomorphisms of hom-sets we just set up to do this. Given $f:A\rightarrow C$ and $g:B\rightarrow D$ in $\mathcal{S}$ their monoidal product $f\cdot g:A\cdot B\rightarrow C\cdot D$ is an arrow in $\hom_\mathcal{M}(F(A\cdot B),F(C\cdot B))$. We define it to be the composite: $F(A\cdot B)\rightarrow F(A)\otimes F(B)\rightarrow F(C)\otimes F(D)\rightarrow F(C\cdot D)$
Here the middle arrow is the monoidal product of $f$ and $g$ in $\mathcal{M}$, and the outer two arrows are the (unique!) ways to change parentheses as needed. The uniqueness follows from the Coherence Theorem, so we have a well-defined monoidal product on $\mathcal{S}$.

So now $F$ is a monoidal functor. We take $F_*$ to be the identity $F([])=\mathbf{1}$, and we let $F_{(A,B)}:F(A)\otimes F(B)\rightarrow F(A\cdot B)$ be the (unique!) arrow moving all the parentheses to the right. The Coherence Theorem gives us this uniqueness, and also handles the diagrams required for a monoidal functor.

Now for the other direction we’ll just go ahead and define $G:\mathcal{M}\rightarrow\mathcal{S}$ by setting $G(A)=[A]$ and $G(f)=f$. We also define $G_*:[]\rightarrow[\mathbf{1}]$ by noticing that $G_*\in\hom_\mathcal{M}(\mathbf{1},\mathbf{1}$, so we can just use the identity. We define $G_{(A,B)}:[A,B]\rightarrow[A\otimes B]$ similarly.

I’ll leave the cleanup to you: $G$ does satisfy coherence conditions for a monoidal functor, $F\circ G:\mathcal{M}\rightarrow\mathcal{M}$ is the identity functor, and there is a monoidal natural isomorphism from $G\circ F$ to the identity functor on $\mathcal{S}$. It’s all pretty striaghtforward, though you’ll have to appeal to the Coherence Theorem a couple times like we have above.

July 1, 2007 - Posted by | Category theory

1. Thanks for this nice explanation. In a monoidal closed category, there’s the curry isomorphism between $A \otimes B \multimap C$ and $B \multimap A \multimap C$. Are all monoidal closed categories equivalent to strict ones where this isomorphism is the identity? Comment by Mike Stay | September 23, 2008 | Reply Comment by John Armstrong | September 23, 2008 | Reply Comment by Todd Trimble | December 17, 2008 | Reply