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”. 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.

Let $\mathsf_0 \subset \mathsf$ 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

Notes

References

*Saunders Mac Lane, ''Categories for the Working Mathematician,'' 2nd edition, Springer GTM, 1998.
*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/

{{categorytheory-stub

Category theory