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. The theorem can be stated as a strictification result, namely that every monoidal category is monoidally equivalent to a strict monoidal category.
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” arrowsagree 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 or by inserting and removing the unit object 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 is a category equipped with atensor product functor and a unit object,
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
- the left unitor
- the right unitor
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 be a monoidal category whosestructural natural isomorphisms satisfy the pentagon and triangle identities.
A formal tensor expression is any expression obtained from objects of
using and.
A formal composite is any morphism obtained by finite compositions and
tensor products of the morphisms
tensored with identity morphisms, whenever the source and target are well-defined.
A formal diagram in 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 are formal composites with the same domain and
codomain, then.
Proof sketch
Mac Lane’s original proof proceeds by reducing all formal composites tocanonical representatives inside a strict monoidal category. The idea is to
construct a strict monoidal category together with a
strong monoidal functor
that is essentially surjective on
objects. The pentagon and triangle identities ensure that any two formal
composites in with the same source and target correspond to the same
strict morphism in, which implies the desired equality in
A modern approach, due to Max Kelly, views the proof in terms of free monoidal
categories. Let be the free monoidal category
generated by, and let be the free strict
monoidal category on the same data. The universal property of these
constructions gives a canonical strong monoidal functor
and the pentagon and triangle identities imply that is fully
faithful. Full faithfulness of is exactly the content of coherence:
it means that there is at most one canonical morphism between any two tensor
expressions.
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.
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.
Let be a skeleton of the category of sets, and let
be its unique countably infinite object. Since is also a
countably infinite set, the skeleton identifies it with. Let
denote the projection onto the first factor. For any
functions, one has the identity
Now suppose, contrary to the usual definition, that the associators
are literally the identity maps; in particular, this holds for
. Then for any,
where the second equality uses naturality of. Hence
Since is an epimorphism, it follows that. A symmetric
argument using the second projection shows, and therefore
. Because and were arbitrary endomorphisms of,
this is a contradiction.