Could not include quasi-category theory - contents
A homotopy exact square is the analogue of an exact square which applies to homotopy Kan extensions, or equivalently to (∞,1)-Kan extensions. It is especially important in the theory of derivators, which provide a calculus for computing with homotopy Kan extensions whose primary tool is the use of homotopy exact squares.
We write , , etc. for the model categories, simplicial categories, -categories, or homotopy categories of diagrams in of whatever shape. We write , , and so on for precomposition functors, which are always homotopically meaningful, and we write , and so on for the homotopically meaningful notions of pointwise left Kan extension. Specifically:
Assume that is such that the relevant extensions and exist. Then there is a canonical Beck-Chevalley transformation
defined as the composite
and we say that the given square is -exact if this transformation is an equivalence. If the square is -exact for all , we say it is homotopy exact. Note that by the general calculus of mates, this is equivalent to requiring that the dual transformation
is an equivalence, where and denote the analogous sort of right Kan extension.
Of course when we say “for all ” we need to specify what sorts of we consider. However, we actually get the same definition regardless of whether we mean “for all model categories ” or “for all simplicially enriched categories ” or “for all -categories ” or “for all derivators ”. This is a nontrivial theorem, especially in the case of derivators.
Since any 1-category is a degenerate sort of -category, any homotopy exact square is exact in the usual 1-categorical sense, but the converse is not true. This also implies that a square can be -exact for some particular without being homotopy exact. However, there exists a “universal” such that -exactness is equivalent to homotopy exactness, namely .
Of course, the above definition is “functional”, while in practice we want some more combinatorial characterization which is easier to check. This can be done completely analogously to the characterization of ordinary exact squares using comma objects, except that at the last step we need to consider a more restricted notion of “equivalence” (i.e. a more restricted basic localizer).
The characterization is the following. Given and and , let denote the category whose objects are triples with and such that , and whose morphisms are morphisms making two triangles commute.
Any comma square is homotopy exact. In other words, if is the comma category with and the canonical projections, then the square is homotopy exact. If in addition is the terminal category, then just picks out an object and is the comma category ; thus this says that (pointwise) homotopy Kan extensions can be computed pointwise as homotopy limits over such comma categories.
If is a fully faithful functor, then the square
is homotopy exact. This just says that the unit is an isomorphism, i.e. that left (and equivalently right) homotopy Kan extensions along are “honest” extensions.
A functor is a homotopy final functor if and only if the square
is homotopy exact. Homotopy exactness of this square says that for , the canonical map is an isomorphism, which is one equivalent definition of when is homotopy final. In this case, the characterization theorem reduces to saying that is homotopy final if and only if each comma category has a contractible nerve, which is a known characterization of homotopy final functors.
For a proof, suppose given and and a morphism , and let be the category whose contractibility we must check. By definition, since , an object of consists of objects and such that , and morphisms and such that .
Let be the full subcategory of consisting of those objects with and the identity, so that an object of is an object such that together with a morphism such that . Then the inclusion has a left adjoint, which sends to , where is an opcartesian arrow over . Therefore, the nerves of and are homotopy equivalent.
But has an initial object, namely , where is an opcartesian arrow over . Thus the nerve of is contractible, and thus so is the nerve of .
Groth has also proved that homotopy-exactness of such squares can be used to replace that of comma squares in the definition of a derivator.