Mac Lane coherence theorem

In category theory, a branch of mathematics, Mac Lane coherence theorem states, in the words of Saunders Mac Lane, “every diagram commutes”.^[1] 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.

Counter-example

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

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

${\displaystyle 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 ${\displaystyle p}$  is an epimorphism, this implies ${\displaystyle f=f\times g}$ . Similarly, using the projection onto the second factor, we get ${\displaystyle g=f\times g}$  and so ${\displaystyle f=g}$ , which is absurd.

Proof

Notes

1. Mac Lane 1998, Ch VII, § 2.
2. Mac Lane 1998, Ch VII. the end of § 1.

References

• Mac Lane, Saunders (1998). Categories for the working mathematician. New York: Springer. ISBN 0-387-98403-8. OCLC 37928530.
• Section 5 of Saunders Mac Lane, Topology and Logic as a Source of Algebra (Retiring Presidential Address), Bulletin of the AMS 82:1, January 1976.

External links

• https://ncatlab.org/nlab/show/coherence+theorem+for+monoidal+categories
• https://ncatlab.org/nlab/show/Mac+Lane%27s+proof+of+the+coherence+theorem+for+monoidal+categories
• https://unapologetic.wordpress.com/2007/06/29/mac-lanes-coherence-theorem/