MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

Often when computing in category theory, one has to show that some square is cartesian. Depending on the number of maps involved, and their arrangement, it's somewhat difficult to write down exactly all of the relationships between the various squares.

Take for instance the following problem (please don't answer it, I've already proven it):

We have a commutative diagram

$$\begin{matrix}C_3 &\to& C_2 &\to& C_1\\ \downarrow&&\downarrow&&\downarrow\\ D_3&\to &D_2&\to& D_1 \end{matrix}$$

Label the right vertical map $p$, and assume we further have a commutative diagram

$$\begin{matrix}\ast &\to& C_1\\ \downarrow&&\downarrow\\ D_3&\to& D_1 \end{matrix}$$

Where map on the top of the square is called $x$ (it classifies a point $x$, and the left vertical map is called $\sigma$. The bottom map and right map are the same maps from the first diagram $D_3\to D_1$ is simply the composite of the two bottom maps in the first diagram.

We would like to show that the canonical map between fibers $$C_3\times_{D_3\times_{D_1} C_1} \{\sigma,x\}\to C_2\times_{C_1} \{x\}\times_{D_2\times_{D_1} \{px\}}\{e\}$$ is a pullback of the canonical map $C_3\to C_2\times_{D_2} D_3$ (if you really care to know, this is to show that the first map is a trivial fibration, since we knew at the time that the second map was a trivial fibration).

Note: The vertex $\{e\}$ is the image of $\sigma$ in $D_2$.

The diagram I drew to realize this was a sheet of four cartesian squares with a cartesian cube attached at the top left square. This is before even taking fibers.

Another example: If anyone's following Ravi Vakil's notes for his schemes course, there is a similar, albeit substantially less complicated problem to prove that the "magic square" is cartesian. I did a similar computation, which ended again with the surprising cartesianness ultimately arising from a cartesian cube attached to a cartesian sheet.

Then the question: Is there a more efficient way to verify claims like this (i.e. without drawing out "every single possible pullback"?

share|cite|improve this question
When I was writing up my thesis I had to think a lot about moduli problems in algebraic geometry and I ended up with questions like this, and once or twice an even simpler sort of question: I had some crazy commutative diagram and I wanted to use some universal property of some subset of it (e.g. "this bit is a pullback of this bit so there's a map from here to here that makes this triangle commute") to draw in another arrow, and I wanted to verify that the new diagram was a commutative diagram! The first time I ran into this issue I had to think hard about what the correct definition... – Kevin Buzzard Sep 18 '10 at 9:55
...of "commutative diagram" was, and then I had to think about what one actually needed to check in order to verify that adding an arrow to a commutative diagram made a new commutative diagram: "I know this new triangle commutes, but do I also have to check that this pentagon does or is it a formal consequence? Do I even have to check that every closed loop mentioning the new arrow commutes? No hang on, that doesn't always make" sort of thing. So I agree that it can get very confusing! There's nothing deep though, it's just a matter of practice (in my experience). – Kevin Buzzard Sep 18 '10 at 9:57
up vote 5 down vote accepted

Try doing it in sets; then you can usually write it out "syntactically". It looks like you've got a map $$ \{c_3\in C_3|p(c_3)=\sigma, fg(c_3)=x\} \to \{c_2 \in C_2| f(c_2)=x \}$$ sending $c_3\mapsto g(c_3)$ and you want to know it's the pullback of the map $$ \{c_3\in C_3\} \to \{(c_2,d_3)| p(c_2)=g(d_3)\}$$ sending $c_3\mapsto (g(c_3),p(c_3))$. I'm writing "$p$" for all vertical maps, "$g$" for $C_3\to C_2$ and $D_3\to D_2$, and "$f$" for $C_2\to C_1$ and $D_2\to D_1$.

Having done this, your claim looks false: it looks like the pullback set is just $\{c_3\in C_3|gf(c_3)=x\}$. But quite possibly I've misinterpreted your diagrams.

The point of this exercise is that, if the set theoretic argument holds, then you can prove the version in the category $C$ using the Yoneda lemma; apply $\mathrm{Hom}_{\mathcal{C}}(T,{-})$ to everything, for arbitrary objects $T$, and observe you get a pullback of sets, therefore you must have a pullback in $\mathcal{C}$.

share|cite|improve this answer
I changed the square brackets to curly braces, as you mentioned. – Tom Church Sep 18 '10 at 2:37
The claim I'm referencing is correct (it's from a book, and I verified it by hand), but I may not have included all of the necessary information. I think that you misunderstood precisely what we wanted prove, namely that one map is the pullback of another map by a third map (To see the claim in its full glory, look at the discussion before Proposition (about the existence of the fibre sequence)). Anyway, your idea is really good! – Harry Gindi Sep 18 '10 at 10:19
Tom's solution is the one that I was going to suggest as well. He beat me to it :-) – Tim Porter Sep 18 '10 at 14:17
Yes, but it was Charles's solution! – Harry Gindi Sep 18 '10 at 15:46
This answer is lovely, and also generalises well. In logical terms, it shows that you can use algebraic equational logic with equality to reason in categories with finite limits; in the jargon, this logic is a sound internal language for such categories. If the category has more structure, then you can do this with a more powerful logic: e.g. if the category has well-behaved images (i.e. is regular), you can use existential quantifiers as well in your reasoning. The beginning of the chapter on Logic in the Elephant has an excellent survey of these techniques. – Peter LeFanu Lumsdaine Sep 18 '10 at 20:56

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.