A pullback in a derivator is the generalization to the context of a derivator of the notion of pullback in ordinary category theory. Viewing a derivator as the “shadow” of an (∞,1)-category, the notion of pullback therein coincides with the notion of homotopy pullback in an -category.
Let denote the category
that is the “free-living commutative square”, and let be the full subcategory of on , with inclusion .
Let be a derivator and let be a commutative square in . We say that is a pullback square, or is cartesian, if the unit of the adjunction is an isomorphism. Since is fully faithful, so is , so this is equivalent to saying that there exists some such that .
If is merely a prederivator, then we can phrase the same definition by saying that has the universal property that would, if the whole functor existed.
The dual notion, of course, is a pushout or cocartesian square.
Using properties of homotopy exact squares, we can prove the “pasting law” for pullback squares in a derivator:
Given a diagram
in which the right-hand square is a pullback, then the left-hand square is a pullback if and only if the outer rectangle is a pullback.
The following proof should be compared and contrasted with the standard proof for pullbacks in 1-categories, and the quasi-categorical proof for pullbacks in -categories. In particular, note that the statement for derivators is a generalization of both, since both 1-categories and -categories give rise to derivators.
First of all, by “a diagram” in a derivator, we mean an object of for some suitable category . In the above case, is the category consisting of two commutative squares, as pictured above. We’ll write for this , and similarly for its lower-right L-shaped subcategory, and so on. We leave the verification of homotopy exactness of all squares to the reader.
Firstly, since the squares
are exact, if we start from a -diagram and right Kan extend it to a full -diagram, then the right-hand square and outer rectangle must be pullback squares. Moreover, by composition of adjoints, right Kan extension from to is equivalent to first extending to and then to , and since the square
is exact, the left-hand square in such an extension must also be a pullback.
Now if we start with an -diagram, say , we can restrict it to a -diagram and then right Kan-extend it to a new -diagram. If is the inclusion, then this results in , and we have a canonical natural transformation (the unit of the adjunction ). Since the square
is exact, the counit is an isomorphism for any , and in particular for , from which it follows by the triangle identities that is also an isomorphism — i.e. the components of at , , , and are isomorphisms. Now if the right-hand square of is a pullback, then the restrictions of and to are both pullback squares; hence since the -components of are isomorphisms, so is the -component. And if the left-hand square of is a pullback, then we can play the same game with to show that the -component of is an isomorphism, while if the outer rectangle is a pullback, we can play it with . Hence in both of these cases, itself is an isomorphism, since all of its components are — and thus the remaining square in is also a pullback, since we have shown that it is so in .
Let be any functor and let be injective on objects, with lower vertex . Suppose that is not in the image of , and that the induced functor is a nerve equivalence (such as if it has an adjoint). Then for any derivator and any , the square is cocartesian.
Since where is induced by and is the inclusion, it suffices to suppose that . Now what we want is to prove that the following square is homotopy exact:
Exactness is trivial at all objects of except . In that case, we paste with another square:
The left-hand square is a comma square, hence homotopy exact, so it suffices to show that the composite square is homotopy exact. But the comma object associated to the cospan is , and of course this comma square is also exact. And the composite square factors through this comma square by the functor which is assumed a nerve equivalence; hence it is also homotopy exact.
See all references at derivator. Referred to particularly above are: