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.
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.
Best Answer
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.