The six functor formalism in a given cohomology theory consists of for each space a derived category of sheaves and six different ways to construct functors between those categories (four involving a morphism and two only a single space). It then consists of many coherences – these are isomorphisms between certain compositions of these functors and, in modern formulations, homotopies between certain combinations of these isomorphisms, 2-homotopies between certain compositions of these homotopies, and so on.
In Peter Scholze's notes on six functor formalisms he gives a precise definition, attributed to Lukas Mann, and closes it by saying:
We note that no further coherences are necessary here: Adjoints automatically acquire all
relevant coherences.
What mathematical claim is being made here? How do we know the coherences acquired are all the relevant ones? Does that knowledge give us an algorithm to prove a desired coherence results?
In the case of a three-functor formalism, including only $\otimes, f^*, f_!$ (i.e. ignoring the adjoints mentioned in the quoted passage), I know basically how to answer all these questions. The three-functor formalism is a functor from a certain infinity-category of correspondences to the infinity-category of all infinity-categories. Each functor arises from a correspondence, so a composition of functors arises from a composition of correspondences. Checking two functors are isomorphic means computing the relevant correspondences and checking they're isomorphic, and this works for all the classical isomorphisms of the six functors formalism that involve only those functors (Leray spectral sequence with compact supports, symmetry and associativity of tensor product, functoriality of pullback, Künneth formula, proper base change, projection formula, tensor products are compatible with pullbacks). Checking two such isomorphisms are the same means evaluating two isomorphisms of correspondences, which ultimately give isomorphisms of schemes, and checking they're the same.
But when adjoints appear I no longer no how to do this. Am I supposed to draw some diagrams in which correspondences are connected with strings?
Best Answer
When defining a homotopy-coherent structure, you have to strike the correct balance between supplying enough data (so that all isomorphisms (between isomorphisms, ...) that you need later are actually defined), and not supplying "too much" data (because if you include two isomorphisms between $A$ and $B$, you might later have to say that after all these two should be same, coherently...).
Generally, if you have some ($\infty$-)category $I$ and a functor towards $\mathrm{Cat}_\infty$, such that all arrows go to left adjoint functors, then you also get a second functor from $I^{\mathrm{op}}$ towards $\mathrm{Cat}_\infty$ giving the diagram of the right adjoints functors; and this procedure can be reversed, giving equivalences of $\infty$-category of such data. Informally, the formation of adjoints is unique (up to contractible choice) and functorial. Thus, one can hope that all the relevant coherence isomorphisms involving adjoint functors can be deduced from the data that is already present.
In the case of $6$-functor formalisms, it seems to me to indeed be the case that all the expected maps and isomorphisms that involve the right adjoint functors (internal Hom, $f_\ast$, $f^!$) do indeed follow automatically. As an example, the base change formula involving $\ast$-pushforward and $!$-pullback is just the adjoint of the base change for $\ast$-pullback and $!$-pushforward. Or the formula $\mathrm{Hom}(f^\ast A,f^! B)=f^!\mathrm{Hom}(A,B)$ follows by passing to taking a partial right adjoint in the projection formula. In general, however, this is a heuristic statement; it is slightly difficult to justify by a theorem because the classical encodings of $6$-functor formalisms consists of some (slightly random) collection of functors, maps, and isomorphisms.
Let me note that there are some maps where I thought for a while that they would not be captured by this abstract notion, but only later realized that actually they are. This the equivalence between $f^\ast$ and $f^!$ for "etale" maps $f$, and between $f_\ast$ and $f_!$ for "proper" maps $f$. More generally, for "separated" maps $f$, one expects a natural transformation $f_!\to f_\ast$ that should be an isomorphism for proper $f$. In Gaitsgory-Rozenblyum's approach to $6$ functors, they make such transformations part of the datum by working with a more subtle $(\infty,2)$-categorical version of correspondences that allows proper maps of correspondences. There seemed to be a general sentiment that this is really necessary: In fact, Gaitsgory-Rozenblyum explicitly say in their work that they think that $(\infty,2)$-categories are critical to define and construct $6$-functor formalisms. This was, to me, a major psychological roadblock, as my knowledge of $(\infty,2)$-categories lacks far behind that of $(\infty,1)$-categories.
But in fact $(\infty,1)$-categories are enough! And you can automatically deduce the expected isomorphisms $f^\ast=f^!$ for etale $f$ and $f_!=f_\ast$ for proper $f$ (and $f_!\to f_\ast$ for separated $f$), as in Lecture 6 of my notes. (Really what happens is that there are inductively defined comparison maps, and they may or may not be isomorphisms; but in any case one does not have to supply further data.) So if one would have incorporated such maps $f_!\to f_\ast$ as part of the data of $6$-functor formalism, one should also ask that these maps are in fact the same as the automatic maps (together with all coherence isomorphisms involving them...). This is probably true in the Gaitsgory-Rozenblyum encoding, but I really haven't tried to check this.
As a final note, it would be really really nice if one could find a nice algorithm or graphical calculus or such that would help one verify expected commutative diagrams involving all $6$ functors. I'm not aware of any work in this direction. But let me note that (as I was made aware of by my student Adam Dauser) the passage from a $6$-functor formalism towards a symmetric monoidal $(\infty,2)$-category where morphisms are given by "Fourier-Mukai kernels" is an instance of something that Lurie has written down in his notes on the cobordism hypothesis (see for instance Corollary 3.3.35 for $n=2$), which is an area that very much uses such graphical calculus...