The Pullback Lemma in Gory Detail (Redux)

January 15, 2024 01:33 UTC (Last updated on August 2, 2024 02:45 UTC)

Tags: math, category theory

Introduction

Andrej Bauer has a paper titled The pullback lemma in gory detail that goes over the proof of the pullback lemma in full detail. This is a basic result of category theory and most introductions leave it as an exercise. It is a good exercise, and you should prove it yourself before reading this article or Andrej Bauer’s.

Andrej Bauer’s proof is what most introductions are expecting you to produce. I very much like the representability perspective on category theory and like to see what proofs look like using this perspective.

So this is a proof of the pullback lemma from the perspective of representability.

Preliminaries

The key thing we need here is a characterization of pullbacks in terms of representability. To just jump to the end, we have for $$ and $$, $$ is the pullback of $$ and $$ if and only if it represents the functor $$

That is to say we have the natural isomorphism $$

We’ll write the left to right direction of the isomorphism as $$ where $$ and $$ and they satisfy $$. Applying the isomorphism right to left on the identity arrow gives us two arrows $$ and $$ satisfying $$ and $$. (Exercise: Show that this follows from being a natural isomorphism.)

One nice thing about representability is that it reduces categorical reasoning to set-theoretic reasoning that you are probably already used to, as we’ll see. You can connect this definition to a typical universal property based definition used in Andrej Bauer’s article. Here we’re taking it as the definition of the pullback.

Proof

The claim to be proven is if the right square in the below diagram is a pullback square, then the left square is a pullback square if and only if the whole rectangle is a pullback square. $$

Rewriting the diagram as equations, we have:

Theorem: If $$, $$, and $$ is a pullback of $$ and $$, then $$ is a pullback of $$ and $$ if and only if $$ is a pullback of $$ and $$.

Proof: If $$ was a pullback of $$ and $$ then we’d have the following.

$$

The second isomorphism is $$ being a pullback and $$ is an arrow into $$ so it’s necessarily of the form $$. The first equality is just $$ mentioned earlier. The second equality merely eliminates the use of $$ using the equation $$.

This overall natural isomorphism, however, is exactly what it means for $$ to be a pullback of $$ and $$. We verify the projections are what we expect by pushing $$ through the isomorphism. By assumption, $$ and $$ will be $$ and $$ respectively in the first isomorphism. We see that $$.

We simply run the isomorphism backwards to get the other direction of the if and only if. $$

The simplicity and compactness of this proof demonstrates why I like representability.