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 [math]\displaystyle{ \mathsf{Set}_0 \subset \mathsf{Set} }[/math] be a skeleton of the category of sets and D a unique countable set in it; note [math]\displaystyle{ D \times D = D }[/math] by uniqueness. Let [math]\displaystyle{ p : D = D \times D \to D }[/math] be the projection onto the first factor. For any functions [math]\displaystyle{ f, g: D \to D }[/math], we have [math]\displaystyle{ f \circ p = p \circ (f \times g) }[/math]. Now, suppose the natural isomorphisms [math]\displaystyle{ \alpha: X \times (Y \times Z) \simeq (X \times Y) \times Z }[/math] are the identity; in particular, that is the case for [math]\displaystyle{ X = Y = Z = D }[/math]. Then for any [math]\displaystyle{ f, g, h: D \to D }[/math], since [math]\displaystyle{ \alpha }[/math] is the identity and is natural,
- [math]\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 }[/math].
Since [math]\displaystyle{ p }[/math] is an epimorphism, this implies [math]\displaystyle{ f = f \times g }[/math]. Similarly, using the projection onto the second factor, we get [math]\displaystyle{ g = f \times g }[/math] and so [math]\displaystyle{ f = g }[/math], which is absurd.
Proof
![[icon]](/wiki/File:Wiki_letter_w_cropped.svg){kind=small} | This section needs expansion. You can help by adding to it. (February 2022) |
Notes
- ↑ Mac Lane 1998, Ch VII, § 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/
 |  |
