Mac Lane coherence theorem

In category theory, a branch of mathematics, Mac Lane's coherence theorem states, in the words of Saunders Mac Lane, “every diagram commutes”.^[1] This result was once thought to be the essence of the coherence theorem, but regarding a result about certain commutative diagrams, Kelly argued that, "no longer be seen as constituting the essence of a coherence theorem".^[2]^[3] More precisely (cf. #Counter-example), it states every formal diagram commutes, where "formal diagram" is an analog of well-formed formulae and terms in proof theory.

The theorem can be stated as a strictification result; namely, every monoidal category is monoidally equivalent to a strict monoidal category.^[4]

Counter-example

It is not reasonable to expect we can show literally every diagram commutes, due to the following example of Isbell.^[5]

Let ${\mathsf {Set}}_{0}\subset {\mathsf {Set}}$ be a skeleton of the category of sets and D a unique countable set in it; note $D\times D=D$ by uniqueness. Let $p:D=D\times D\to D$ be the projection onto the first factor. For any functions $f,g:D\to D$ , we have $f\circ p=p\circ (f\times g)$ . Now, suppose the natural isomorphisms $\alpha :X\times (Y\times Z)\simeq (X\times Y)\times Z$ are the identity; in particular, that is the case for $X=Y=Z=D$ . Then for any $f,g,h:D\to D$ , since $\alpha$ is the identity and is natural,

f\circ p=p\circ (f\times (g\times h))=p\circ \alpha \circ (f\times (g\times h))=p\circ ((f\times g)\times h)\circ \alpha =(f\times g)\circ p

.

Since $p$ is an epimorphism, this implies $f=f\times g$ . Similarly, using the projection onto the second factor, we get $g=f\times g$ and so $f=g$ , which is absurd.

Proof

Coherence condition (Monoidal category)

Let a bifunctor $\otimes \colon \mathbf {C} \times \mathbf {C} \to \mathbf {C}$ called the tensor product, a natural isomorphism $\alpha _{A,B,C}$ , called the associator:

\alpha _{A,B,C}\colon A\otimes (B\otimes C)\rightarrow (A\otimes B)\otimes C

Also, let $I$ an identity object and $I$ has a left identity, a natural isomorphism $\lambda _{A}$ called the left unitor:

\lambda _{A}:I\otimes A\rightarrow A

as well as, let

I

has a right identity, a natural isomorphism

\rho _{A}

called the right unitor:

\rho _{A}:A\otimes I\rightarrow A

.

Since there are many ways to construct an isomorphism using the above natural isomorphism, they impose a condition called the coherence condition on the above natural isomorphism. If the above isomorphism satisfies the following conditions, they are called coherence conditions: the arrows constructed by get tensor products and compositions from identity morphisms, natural isomorphisms, and their inverses are equal, if their domains and codomains of the arrows are same.^[6]^[7] If the coherence condition is satisfied, then no matter how they construct the isomorphism, they will always end up with the same isomorphism.

Pentagon and triangle identity (Coherence axiom)

To satisfy the coherence condition, it is enough to prove just the pentagon and triangle identity, which is essentially the same as what is stated in Kelly's (1964) paper.^[6]