Pullback of a pullback square along $f$ is again a pullback square

Question

Awodey's Category Theory is at it again, asking me to do things without fully explaining what any of it means. Part (b) of Problem 2 in Chapter 5 reads as follows:

Show that the pullback along an arrow $f:Y\to X$ of a pullback square over $X$, $\require{AMScd}$ \begin{CD} A\times_X B @>>> B\\ @VVV @VVV\\ A @>>> X \end{CD} is again a pullback square over $Y$.

---

So I started by doing the obvious thing and I drew a cube with the goal of eventually applying the two-pullbacks lemma.

(Original image here.)

The goal is to show that the back fact of the cube is a pullback square. The triples $(A', \alpha', f_\alpha)$ and $(B', \beta', f_\beta)$ are obtained as pullbacks of the diagrams $\require{AMScd}$ \begin{CD} A\\ @V\alpha VV\\ X @<f<< Y \end{CD} and $\require{AMScd}$ \begin{CD} B\\ @V\beta VV\\ X @<f<< Y \end{CD} This much seems pretty clearly the right way to do things, but then I run into a problem. There are two ways to induce each of the three arrows $P\to A'$, $P\to B'$, and $P\to A\times_X B$ as pullbacks. My thinking is that I probably don't want to induce $P\to A'$ or $P\to B'$ as the pullback of $\alpha'$ and $\beta',$ so I induce those maps as pullbacks $\require{AMScd}$ \begin{CD} P @>>> A\times_X B\\ @VVV @VV p_1 V\\ A' @>>f_\alpha > A \end{CD} and $\require{AMScd}$ \begin{CD} P @>>> A\times_X B\\ @VVV @VV p_2 V\\ B' @>>f_\beta > B \end{CD} The problem is that this induces two different maps $g_1:P\to A\times_X B$ and $g_2:P\to A\times_X B$. If I could show that these maps are the same, then I could apply two-pullbacks twice and be done. However, I have no idea how to do this. It seems that it should come from the uniqueness of maps to pullbacks, so I would try and show that $p_1g_1=p_1g_2$ and $p_2g_1=p_2g_2$. Uniqueness would then give $g_1=g_2$. Alas, I don't see why this would be true. Perhaps I need to pullback $\alpha'$ and $\beta'$ and show that those maps are the the same as the ones I have already induced. Any hint would be appreciated.

---

In truth, I am not exactly sure what the question is asking. For example, one lemma given in Awodey states that the pullback of a commutative triangle is a commutative triangle. He then clarifies to say that if I have a triangle $\gamma:A\to B$, $\beta:B\to C$, and $\alpha:A\to C$ with $\alpha=\beta\circ\gamma$ and a map $f:C'\to C$, and if one can form pullbacks $\alpha'$ and $\beta'$ of $\alpha$ and $\beta$ along $f$, then there is a pullback $\gamma'$ of $\gamma$ which satisfies $\alpha'=\beta'\circ\gamma'$. I'm not entirely sure how the first bolded statement translates to the second bolded statement. The only justification I have for it is that it makes the application of the two-pullbacks lemma possible. If someone could justify the precise lemma statement from the ambiguous one and make the problem statement precise in the same way, that would help just as much.

Answer 1

For anyone who cares, I have figured out the answer to the problem. If one labels the map $\alpha\circ p_1=\beta\circ p_2:A\times_X B\to X$ as $h$, then we have two commutative triangles making up the front face of the cube. Take the triangle $A\times_X B\to A\to X$. One forms pullbacks $h'$ and $\alpha'$ of $h$ and $\alpha$ respectively along $f$, and then two-pullbacks gives a map $q_1:P\to A'$ such that $\alpha'\circ q_1=h'$ and such that left side of the cube is a pullback. Do the same for the other triangle on the front face. Then one evidently gets commutativity of the entire cube, and every face save for the back face (the one we care about) is a pullback square. Now, by two-pullbacks, if we show that the rectangle formed by the back and bottom faces is a pullback, then since the bottom face is a pullback, the back face must be as well. But since the diagram commutes, this rectangle is the same as the rectangle formed by the top and front faces. Since these faces are each pullback squares, the rectangle is as well, and two-pullbacks gives that the back face is indeed a pullback.

Working through this problem has also made it evident to me why the commutative triangle lemma should be interpreted the way it is. In this problem, we assume that the category $\mathbf{C}$ has all pullbacks, but in this problem we are only pulling back along $f$. In order to get anywhere in this problem, i.e. show that a face which doesn't involve $f$ is a pullback, we need some way of concluding that some face which doesn't involve $f$ is a pullback. The commutative triangle lemma states that if one has a commutative triangle and pulls back the only two maps that one can pull back along $f$, then there is a map completing the triangle, that is, which makes a very much desired "commutative triangular prism" in which the faces are pullbacks.

If there are any flaws in my understanding someone should let me know, but as of now I feel that all of the gaps in my understanding have been filled.

Answer 2

Awodey's description of a pullback of a commutative triangle is different (and much clearer) than what you've said. For example, it doesn't make sense to talk about the pullback of $\alpha'$ along $f$ since the codomain of $\alpha'$ is not $C$. It would make sense to talk about the pullback along $\beta$ and $\gamma$ inducing a pullback square involving $\alpha$, and this is what Awodey says (though more clearly than this). Albeit, you've switch $\alpha$ and $\gamma$ from his presentation (which is probably part of the confusion).

Nevertheless, there is an easier/better way of thinking about what is going on which is touched at in multiple points later in the book. Awodey mentioned the slice category $\mathcal C/C$ early on as an example of a category. This is the category whose objects are arrows of $\mathcal C$ with codomain $C$. Given two objects of $\mathcal C/C$, i.e. two arrows $k:A\to C$ and $g:B\to C$, an arrow from $k \to g$ is an arrow $f:A\to B$ such that $k=g\circ f$. This is sometimes expressed by saying that the arrows are commutative triangles.

Now, assuming $\mathcal C$ has pullbacks, an arrow $h: C'\to C$ of $\mathcal C$ induces a functor $h^*:\mathcal C/C\to\mathcal C/C'$ via pullback called the pullback or reindexing functor or change of base. This works as follows: $$\require{AMScd} \begin{CD} B\times_C C' @>h^*(g)>> C' \\ @VpVV @VVhV \\ B @>>g>C \end{CD}$$ In other words, the object $h^*(g)$ (viewing $g$ as an object of $\mathcal C/C$) is the projection of the pullback of $h$ and $g$ into $C'$ (which is an object of $\mathcal C/C'$). Now given $f:A\to B$ such that $k = g \circ f$, i.e. an arrow of $\mathcal C/C$ from $k$ to $g$, we can take the pullback of $f$ along $p$ (i.e. the other projection of the pullback $h^*(g)$) which will give us an arrow into $B\times_C C'$. Alas, we have no guarantee that the domain of the resulting arrow (of $\mathcal C$) will equal the domain of $h^*(k)$ (and whose projection will match the other projection in the pullback diagram defining $h^*(k)$). The two pullbacks lemma, though, states that we can always find such a pullback. The pullback diagram for $h^*(k)=h^*(g\circ f)$ is the "outer rectangle" while $h^*(g)$ is the "right square" and the pullback we need is the "left square". The form in the corollary is even more direct. We want to turn arrows of $\mathcal C/C$, i.e. commutative triangles, into arrows of $\mathcal C/C'$ (more commutative triangles) by pulling back along $h$. In other words, the commutative triangle form is simply the statement that $h^*$ has a well-defined action on arrows. (Another perspective on the "two pullbacks" lemma is that $(g\circ f)^*\cong f^*\circ g^*$.)

Now for your pullback of a pullback square, you just note that pullbacks (aka fibered products) are products in the slice category. That is, given $k:A\to C$ and $g:B\to C$, the product $k\times g$ in $\mathcal C/C$ is (the diagonal arrow of the) pullback of $k$ and $g$. So your "pullbacks of pullback squares is a pullback" theorem is simply stating that $h^*$ preserves products, i.e. that $h^*(k\times g)\cong h^*(k)\times h^*(g)$ and $h^*(\pi_i)=\pi'_i$. (The terminal object of any slice category is the identity arrow [viewed as an object]. It's straightforward to show $h^*(id_C)\cong id_{C'}$.) In fact, using slightly more advanced category theory, we can finesse the whole problem. $h^*$ (as with any pullback functor) has a left adjoint just via post-composition, so $h^*$, like any right adjoint, preserves all limits including finite products.