6

The Yoneda lemma is sometimes claimed to simplify proofs. For instance, the associativity of binary products can be proved by considering $\hom(X, (A \times B) \times C)$, and by the bijection of sets $(U \times V) \times W \cong U \times (V \times W)$ we get the result.

However, this neglects the naturality of that family of bijection. Wouldn't it be just as tedious to verify naturality as doing the proof by diagram chasing? This seems to especially be the case when equalizers and exponentials etc. are involved, so the rearrangement is non-trivial. Ascending to 2-categories, this problem only gets worse.

Is there a nice trick that reduces the work, while staying completely rigorous?

Trebor
  • 3,480
  • 2
  • 8
  • 29
  • 1
    There’s no need to chase any diagrams. You just need to build up your toolbox of basic lemmas. For example, natural transformations compose to yield natural transformations. – Zhen Lin Mar 18 '23 at 04:54
  • @ZhenLin My example above doesn't seem to be decomposable. So what you are saying is "no, we can't do this quickly", right? Because these are exactly the tools you are referring that need to be built up by hand. – Trebor Mar 18 '23 at 05:41

1 Answers1

4

As with so many things, you proceed in small steps. I will not go into too many details because basic things like this depend on definitions and you have not provided any.

First: $$\textrm{Hom} (X, (A \times B) \times C) \cong \textrm{Hom} (X, A \times B) \times \textrm{Hom} (X, C)$$ This is natural in $X, A, B, C$ and is either by definition of $\times$ or a basic lemma you prove soon. Note that $\times$ of sets may have a different definition – it doesn't matter, as long as you are consistent. Then we repeat: $$\textrm{Hom} (X, A \times B) \times \textrm{Hom} (X, C) \cong (\textrm{Hom} (X, A) \times \textrm{Hom} (X, B)) \times \textrm{Hom} (X, C)$$ This too is natural in $X, A, B, C$, of course. Now, $$(\textrm{Hom} (X, A) \times \textrm{Hom} (X, B)) \times \textrm{Hom} (X, C) \cong \textrm{Hom} (X, A) \times (\textrm{Hom} (X, B) \times \textrm{Hom} (X, C))$$ naturally in $X, A, B, C$. This is supposed to be a lemma you already know – otherwise there is indeed no point using Yoneda for this. Now we basically reverse the earlier steps: $$\textrm{Hom} (X, A) \times (\textrm{Hom} (X, B) \times \textrm{Hom} (X, C)) \cong \textrm{Hom} (X, A) \times \textrm{Hom} (X, B \times C)$$ $$\textrm{Hom} (X, A) \times \textrm{Hom} (X, B \times C) \cong \textrm{Hom} (X, A \times (B \times C))$$ Compose all of these natural bijections to obtain: $$\textrm{Hom} (X, (A \times B) \times C) \cong \textrm{Hom} (X, A \times (B \times C))$$ Then finally use the fully-faithfulness of the Yoneda embedding to deduce: $$(A \times B) \times C \cong A \times (B \times C)$$ This is natural in $A, B, C$, of course.

Zhen Lin
  • 87,736
  • 11
  • 174
  • 320
  • 2
    My main concern is exactly the step in $\mathsf{Set}$. In the category $\mathsf{Set}$, writing (a) a proof of natural associativity abstractly by universal properties, and (b) using concrete elements, the length of (a) and (b) are actually similar. So the only thing Yoneda provides in this situation is the ability to reason with elements which is more intuitive, instead of really shortening the proof, right? – Trebor Mar 18 '23 at 09:41
  • 1
    I think most mathematicians would consider option (b) to be obvious and not require spelling out. – Zhen Lin Mar 18 '23 at 10:48
  • This is actually a real problem for formalization, because a proof assistant does not consider (b) as obvious, sadly :( But your answer is very helpful. – Trebor Mar 18 '23 at 10:49
  • 3
    If you spell everything out then it is unlikely to be much shorter. I believe in conservation of complexity. – Zhen Lin Mar 18 '23 at 10:53