Productive Homotopy Pullbacks
Posted by Mike Shulman
The last time I talked about derivators, we ended up making an interesting comparison between derivator techniques and quasicategory techniques. In particular, we looked at a proof of the pasting law for homotopy pullbacks using derivators (presented in that post) and the analogous proof for quasicategories from Higher Topos Theory (partially described here). We thought at the time it would be nice to continue with further comparisons, but got sidetracked.
Along those lines, here’s another little fact that was easy for me to prove with derivators. Anyone care to try their hand at a proof using quasicategories, so we can compare them?
Here’s the setup. In my last post I mentioned that there are some squares built out of cartesian products which are always pullback squares. Todd Trimble has a nice discussion of these here; he calls them productive pullbacks. I also mentioned that some, but not all, of these squares are actually always homotopy pullbacks. Let’s prove that.
The first one is For this, it suffices to prove that
- The pointwise product of pullback squares is a pullback square;
- For any , the square is a pullback; and
- The transpose of a pullback square is a pullback square.
I’m going to say “pullback” instead of “homotopy pullback” from now on. Also, in case you’ve forgotten, this page contains the characterization of homotopy exact squares, the main tool we use for computing in a derivator, as well as some important examples.
Let denote the free-living commutative square, and its lower-right corner (the free-living cospan), with inclusion functor . In a derivator, a pullback square is a -diagram which is isomorphic to of something.
Now since commutes with the “transpose” automorphisms of and , the third point above follows immediately. For the first, we observe that the following square of functors commutes: where the rightward-pointing arrows are the fold maps. But right Kan extension along a fold map is precisely how we calculate products of diagrams (using the fact that a derivator takes coproducts to products). Thus, it suffices to observe that right Kan extension along , when restricted to each factor, computes the right Kan extension along . This is because the following square is homotopy exact: Finally, for the second point above, consider the following square, where is the interval category: The downward-pointing arrows and project a commutative square to one of its axes (say, the horizontal one). This square is homotopy exact, so . But takes an arrow to the cospan while takes it to the square so this says that the latter is the pullback of the former, which is what we want.
The second productive homotopy pullback is To show that this is a pullback, consider the following functor . The function takes 5 to 1 and takes 6 and 7 to 2. The function takes 5 and 6 to 3 and takes 7 to 4. Let be the discrete fibration corresponding to this presheaf, and let be a pullback. Thus, .
Now since and are fibrations, right Kan extension along them is computed by taking limits over the fibers. This is because pullback squares such as are homotopy exact when is a fibration. Therefore, if is an -shaped diagram in a derivator, then looks like The morphisms, of course, are induced from those in , which contains maps , , , , , and . Therefore, the square we want to show to be a pullback is of the constant diagram on , which is to say (where is the restriction along ).
Since , it will therefore suffice to show that is of the form applied to something, and the obvious choice for that something is . Thus, we need to show the following square is homotopy exact: The nontrivial bit of proving this is essentially the statement that has a contractible nerve. But the geometric realization of the nerve of is homeomorphic to the interval, since looks like This completes the proof.
The final productive homotopy pullback square is I’ll leave that one as an exercise for the reader.
Anyone care to try a quasicategorical proof?
Re: Productive homotopy pullbacks
I am still trying to grasp derivators but I think I am making a little bit of progress :)
Thanks to the n-Category Cafe I’m making it there!