Mac Lane's coherence theorem

In category theory in mathematics, Mac Lane's coherence theorem states that in any monoidal category, every well-formed diagram built from the associativity and unit isomorphisms commutes.^[1] The theorem can be stated as a strictification result, namely that every monoidal category is monoidally equivalent to a strict monoidal category.^[2]

Overview

In a monoidal category, the tensor product is associative and unital only up to the natural isomorphisms given by the associator and the left and right unitors. Because these isomorphisms can be composed in many different ways, there are in principle many different arrows between the same tensor expressions. The central question is whether all these “canonical” arrows agree with one another.

Mac Lane's coherence theorem gives a positive answer. It states that every diagram that can be built from the associativity and unit constraints necessarily commutes. This means that any two canonical morphisms obtained by rebracketing tensor products (using the associator and its inverse) or by inserting and removing the unit object (using the unitors and their inverses) are equal whenever they have the same source and target. As a result, the associator and unitors behave coherently, and no further identities beyond the pentagon and triangle need to be imposed.

One important consequence is that every monoidal category is equivalent, in a sense appropriate to monoidal structure, to a strict monoidal category in which the associativity and unital laws hold on the nose. This “strictification” property explains why monoidal categories can often be treated as though they were strictly associative without loss of generality.

Background

A monoidal category ${\displaystyle ({\mathcal {C}},\otimes ,I)}$ is a category equipped with a tensor product functor ${\displaystyle \otimes$ :{\mathcal {C}}\times {\mathcal {C}}\to {\mathcal {C}}} and a unit object ${\displaystyle I}$, together with natural isomorphisms that express how the tensor product behaves. The tensor product is not strictly associative or strictly unital; instead, the structure includes three canonical natural isomorphisms:

• the associator

 ${\displaystyle \alpha _{A,B,C}:(A\otimes B)\otimes C\to A\otimes (B\otimes C)}$,

• the left unitor

 ${\displaystyle \lambda _{A}:I\otimes A\to A}$, and

• the right unitor

 ${\displaystyle \rho _{A}:A\otimes I\to A}$.

These isomorphisms witness associativity and unitality “up to isomorphism”. Because different sequences of rebracketing and unit insertions can connect the same tensor expressions, there may be many canonical morphisms between the same source and target object. A central question is whether all such canonical morphisms agree with one another.

To control this ambiguity, monoidal categories are required to satisfy two compatibility conditions, the pentagon and triangle identities, which relate the associator and unitors. These conditions are the starting point for Mac Lane’s coherence theorem.

Statement

Let ${\displaystyle ({\mathcal {C}},\otimes ,I,\alpha ,\lambda ,\rho )}$ be a monoidal category whose structural natural isomorphisms satisfy the pentagon and triangle identities. A formal tensor expression is any expression obtained from objects of ${\displaystyle {\mathcal {C}}}$ using ${\displaystyle \otimes }$ and ${\displaystyle I}$. A formal composite is any morphism obtained by finite compositions and tensor products of the morphisms

${\displaystyle \alpha _{A,B,C},\qquad \alpha _{A,B,C}^{-1},\qquad \lambda _{A},\qquad \lambda _{A}^{-1},\qquad \rho _{A},\qquad \rho _{A}^{-1},}$

tensored with identity morphisms, whenever the source and target are well-defined.

A formal diagram in ${\displaystyle {\mathcal {C}}}$ is a commutative diagram whose vertices are formal tensor expressions and whose edges are formal composites.

Mac Lane's coherence theorem. In any monoidal category, every formal diagram commutes. Equivalently, if ${\displaystyle f,g:X\to Y}$ are formal composites with the same domain and codomain, then ${\displaystyle f=g}$.^[3][4]

Proof sketch

Mac Lane’s original proof proceeds by reducing all formal composites to canonical representatives inside a strict monoidal category. The idea is to construct a strict monoidal category ${\displaystyle {\mathcal {C}}_{\mathrm {str} }}$ together with a strong monoidal functor ${\displaystyle F:{\mathcal {C}}_{\mathrm {str} }\to {\mathcal {C}}}$ that is essentially surjective on objects. The pentagon and triangle identities ensure that any two formal composites in ${\displaystyle {\mathcal {C}}}$ with the same source and target correspond to the same strict morphism in ${\displaystyle {\mathcal {C}}_{\mathrm {str} }}$, which implies the desired equality in ${\displaystyle {\mathcal {C}}}$.^[5]

A modern approach, due to Max Kelly, views the proof in terms of free monoidal categories. Let ${\displaystyle {\mathsf {FreeMon}}({\mathcal {C}})}$ be the free monoidal category generated by ${\displaystyle {\mathcal {C}}}$, and let ${\displaystyle {\mathsf {FreeStrict}}({\mathcal {C}})}$ be the free strict monoidal category on the same data. The universal property of these constructions gives a canonical strong monoidal functor ${\displaystyle J:{\mathsf {FreeStrict}}({\mathcal {C}})\to {\mathsf {FreeMon}}({\mathcal {C}}),}$ and the pentagon and triangle identities imply that ${\displaystyle J}$ is fully faithful. Full faithfulness of ${\displaystyle J}$ is exactly the content of coherence: it means that there is at most one canonical morphism between any two tensor expressions.^[6][7]

Schauenburg later gave a shorter proof using the formalism of 2-categories: a monoidal category is the same data as a pseudomonoid in the 2-category of categories. Coherence for pseudomonoids follows from general coherence results for bicategories, yielding coherence for monoidal categories as a special case.^[8]

Although the details vary among approaches, all proofs rely on the fact that once the pentagon and triangle identities hold, every composite built from the associator and unitors has a unique normal form. This uniqueness is equivalent to the commutativity of all formal diagrams.

Counter-example

Mac Lane’s coherence theorem asserts that all formal diagrams commute, that is, diagrams whose edges are built only from the structural isomorphisms of a monoidal category. Isbell’s example shows that this result cannot be strengthened to arbitrary diagrams involving the monoidal product: if one were to require all such diagrams to commute, the category would collapse in an impossible way. ^[9]

Let ${\displaystyle {\mathsf {Set}}_{0}\subset {\mathsf {Set}}}$ be a skeleton of the category of sets, and let ${\displaystyle D}$ be its unique countably infinite object. Since ${\displaystyle D\times D}$ is also a countably infinite set, the skeleton identifies it with ${\displaystyle D}$. Let ${\displaystyle p:D=D\times D\to D}$ denote the projection onto the first factor. For any functions ${\displaystyle f,g:D\to D}$, one has the identity ${\displaystyle f\circ p\;=\;p\circ (f\times g).}$

Now suppose, contrary to the usual definition, that the associators ${\displaystyle \alpha _{X,Y,Z}:X\times (Y\times Z)\to (X\times Y)\times Z}$ are literally the identity maps; in particular, this holds for ${\displaystyle X=Y=Z=D}$. Then for any ${\displaystyle f,g,h:D\to D}$, ${\displaystyle f\circ p=p\circ (f\times (g\times h))=p\circ ((f\times g)\times h),}$ where the second equality uses naturality of ${\displaystyle \alpha }$. Hence ${\displaystyle f\circ p=(f\times g)\circ p.}$ Since ${\displaystyle p}$ is an epimorphism, it follows that ${\displaystyle f=f\times g}$. A symmetric argument using the second projection shows ${\displaystyle g=f\times g}$, and therefore ${\displaystyle f=g}$. Because ${\displaystyle f}$ and ${\displaystyle g}$ were arbitrary endomorphisms of ${\displaystyle D}$, this is a contradiction.

See also

• Braided monoidal category
• Coherency (homotopy theory)
• Monoidal category
• Symmetric monoidal category
• 2-category#Coherence theorem
• 3-category