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 be a skeleton of the category of sets and D a unique countable set in it; note by uniqueness. Let be the projection onto the first factor. For any functions , we have . Now, suppose the natural isomorphisms are the identity; in particular, that is the case for . Then for any , since is the identity and is natural,
- .
Since is an epimorphism, this implies . Similarly, using the projection onto the second factor, we get and so , which is absurd.
Proof
Notes
- Mac Lane 1998, Ch VII, § 2.
- Mac Lane 1998, Ch VII. the end of § 1.
References
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/