In some modern textbooks (e.g., Tensor Categories by Etingof et al. and Brandenburg's textbook on category theory which is in German), Mac Lane's coherence theorem is deduced from Mac Lane's strictness theorem.

Strictness theorem. Every monoidal category is monoidally equivalent to a strict monoidal category.

Coherence theorem. Let $\mathsf{C}$ be a monoidal category and let $X_1,...,X_n \in \mathsf{C}$. Let $P_1,P_2$ be any two parenthesized products of $X_1,...,X_n$ with arbitrary insertions of the unit object $1$. Let $f,g\colon P_1\to P_2$ be two isomorphisms, obtained by composing $\alpha, \alpha^{-1}, l, l^{-1}, r, r^{-1}$, possibly tensored with identity morphisms. Then $f = g$.

The idea seems simple: to prove that if the induced morphisms in a strict monoidal category $\mathsf{C}_s$ (together with a monoidal equivalence $F\colon\mathsf{C}\to\mathsf{C}_s, J$) coincide, then so do $F(f)$ and $F(g)$, from which it will follow that $f = g$ by faithfulness of $F$. However, I'm having trouble building an isomorphism between $F(f), F(g)$ and their respective analogs in $\mathsf{C}_s$. What give me trouble are if unit isomorphisms tensored (possible multiple times) by identities are inserted between associativity in $f$ or $g$. Nontrivial examples would be apprecited for aforementioned books do not give them, they only refer to monoidal conditions.

I assume that a monoidal equivalence comes with a canonical isomorphism $F(1) \cong 1$ which satisfy approprite conditions relating $l_{F(X)}$ and $F(l_X)$ (resp., $r_{F(X)}$ and $F(r_X)$).

  • $\begingroup$ A very interesting question! Why didn't you ask about the other direction? Is it because it is obvious (or just by lack of interest)? $\endgroup$
    – Bob
    May 3, 2020 at 18:21
  • $\begingroup$ @Jxt921 Do you remember the details of the proof? I'm reading the same proof and I'm not satisfied by the explanation in Etingof's book, and your question strikes me as exactly what I'm looking for. Would you be interested in a bounty of 500rep (maximum bounty possible to give) if you give the complete rigorous proof? $\endgroup$ Dec 3, 2021 at 22:21

1 Answer 1


The proof should go as follows.

In the strict monoidal category, we have that the corresponding compositions of $\alpha'$, $\alpha^{\prime -1}$, $l'$, $l^{\prime-1}$, $r'$, $r^{\prime -1}$ are all the identity.

Let $P_{Fi}$ be the corresponding parenthesization of $FX_1,\ldots,FX_n$ and $1'$s to $P_i$. Monoidality of the equivalence gives natural isomorphisms $\alpha_i : FP_i \to P_{Fi}$ such that $$ \require{AMScd} \begin{CD} FP_1 @>F f>> FP_2\\ @V\alpha_1 VV @V\alpha_2 VV \\ P_{F1} @> \mathrm{id} >> P_{F2}. \end{CD} $$ The same diagram commutes for $g$, so $Ff=Fg$. Then by faithfulness of $F$, $f=g$.

Constructing $\alpha_i$

It sounds like you're having trouble with constructing the $\alpha_i$, so I'll expand on this a bit. This goes inductively, so we just need to deal with the outermost layer of $P_1$ or $P_2$. We'll just look at $P_1$.

If $P_1 = X\otimes Y$, then $FP_1 = F(X\otimes Y)$ and $P_{F1} = X_F \otimes Y_F$, where the $F$ subscript refers to the appropriate product of $F$ applied to the atoms. Then we have the monoidal structure isomorphism $J : F(X\otimes Y) \to F(X)\otimes F(Y)$, and then we inductively construct $\alpha_X : F(X)\to X_F$ and $\alpha_Y : F(Y)\to Y_F$. The composite $(\alpha_X \otimes \alpha_Y) \circ J$ gives the desired isomorphism $FP_1\to P_{F1}$.

On the other hand, if $P_1 = I\otimes X$, then $P_{F1} = I'\otimes X_F$. This time, if $\iota : F(I)\to I'$ is the natural isomorphism, we take the composite $$F(I\otimes X)\overset{J}{\to} F(I)\otimes FX \overset{\iota\otimes \alpha_X}{\to} I'\otimes X_F= P_{F1}$$

For $P_1 = X\otimes I$ we do the same thing but modified for symmetry.

Hopefully this helps. I can expand on this if needed.

Edit, an expansion on why the diagram commutes.

This is also proved inductively.

Suppose the outermost function in $f$ is an associator, which I'll denote by $a$ and $a'$ in the two categories in the equivalence in $C_s$, $a'=\mathrm{id}$, since I used $\alpha$ for the natural isomorphisms.

Then $f=a\circ f_0$ and $f'=a'\circ f_0'$, with $f:P_1\to P_2$ and $P_2 : X\otimes (Y \otimes Z$ for some products $X$, $Y$, and $Z$, so $f_0 : P_1\to (X\otimes Y)\otimes Z$. Then we have the commutative diagram $$ \newcommand\id{\mathrm{id}} \begin{CD} FP_1 @>f_0>> F((X\otimes Y) \otimes Z) @>Fa>> F(X \otimes (Y\otimes Z)) \\ @VVV @VJVV @VJVV \\ @. F(X\otimes Y) \otimes FZ @. FX\otimes F(Y\otimes Z) \\ @V\alpha_1 VV @VJ\otimes \id VV @V\id \otimes J VV \\ @. (FX\otimes FY)\otimes FZ @>a'>> FX\otimes (FY\otimes FZ)\\ @VVV @V(\alpha_X\otimes \alpha_Y)\otimes \alpha_Z VV @V\alpha_X \otimes (\alpha_Y\otimes \alpha_Z)VV \\ P_{F1} @>f'_0>> (X_F\otimes Y_F)\otimes Z_F @>a'>> X_F \otimes (Y_F\otimes Z_F) \\ \end{CD} $$ The left rectangle commutes by the inductive hypothesis applied to $f_0$, since the middle vertical composite is the definition of the $\alpha$ map for $(X\otimes Y)\otimes Z$. The top right rectangle commutes by the compatibility condition for $J$. The bottom right square commutes by naturality of the associator. By symmetry, the same argument applies to $a^{-1}$.

Now we need to do the same thing for the left and right units and their inverses. By symmetry, it suffices to prove commutativity when the outermost map in $f$ is $l$.

Then $f = l\circ f_0$, with $f_0 : P_1\to I\otimes P_2$. This time, we get the diagram $$ \begin{CD} FP_1 @>f_0>> F(I\otimes P_2) @>Fl>> FP_2 \\ @VVV @VJVV @V\id VV \\ @. FI\otimes FP_2 @. FP_2 \\ @V\alpha_1 VV @V \iota \otimes \id VV @V\id VV \\ @. I'\otimes FP_2 @>l'>> FP_2 \\ @VVV @V\id \otimes \alpha_2 VV @V\alpha_2VV \\ P_{F1} @>f'_0>> I'\otimes P_{F2} @>l'>> P_{F2} \\ \end{CD} $$ Again, the left rectangle commutes by the inductive hypothesis, the top right rectangle is the coherence condition for $\iota$, and the bottom right square is naturality of $l'$.

This completes the proof.

  • $\begingroup$ Thank you a lot for your attention! However, one thing remains - to prove that the diagram you have written commutes. I would greatly appreciate if you could expand on that, for I have no idea how to do it. $\endgroup$
    – Jxt921
    Dec 21, 2019 at 18:48
  • $\begingroup$ @Jxt921 Updated my answer. Hopefully this addresses your comment. $\endgroup$
    – jgon
    Dec 22, 2019 at 22:22
  • $\begingroup$ This seems to be in the right direction, but you probably need to accound to $a,l,r$ being tensored by identity morphisms (possibly multiple times). This I assume warrants another induction on the length of $\beta$ in $1_X\otimes \beta$ (or $\beta\otimes 1_X$). I tried to do it myself, but it seems this requires to modify the definition of your $\alpha_i$ $\endgroup$
    – Jxt921
    Dec 23, 2019 at 8:33
  • $\begingroup$ Or maybe not... Would, for example, $1_{F(X)}\otimes\beta$ already by covered for your definition? $\endgroup$
    – Jxt921
    Dec 23, 2019 at 8:35
  • $\begingroup$ @Jxt921 oh sorry, I forgot about that, but everything should still commute by just tensoring the diagrams with the identity maps. I'll have to check on that, but it should work properly. $\endgroup$
    – jgon
    Dec 23, 2019 at 14:26

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.