## Coherence for pull-backs and push-forwards

Let $p:X \to S$ and $q:Y\to S$ be two objects in the category of ringed spaces over the ringed space $S$, and let $f:X \to Y$ be a morphism over $S$.

Given a sheaf $\mathcal{F}$ of $\mathcal{O}_Y$-modules, there are at least two different ways to produce a morphism $$q_*\mathcal{F} \to p_*f^*\mathcal{F}$$ of sheaves of $\mathcal{O}_S$-modules by just using canonical operations. We could for instance apply the adjunction unit for $(f^*, f_*)$ to $\mathcal{F}$, push the map forward to $S$ and then use the natural isomorphism $q_*f_* \simeq p_*$. That is $$\mathcal{F} \to f_*f^*\mathcal{F}$$ $$q_*\mathcal{F} \to q_*f_*f^*\mathcal{F}$$ $$q_*\mathcal{F} \to p_*f^*\mathcal{F}.$$ On the other hand, we could start by applying the adjunction co-unit for $(q^*, q_*)$, pull it back to $X$, use the natural isomorpism $f^*q^* \simeq p^*$ and finally use the adjuncton $(p^*, p_*)$ to produce a morphism of $\mathcal{O}_S$-modules. That is $$q^*q_*\mathcal{F} \to \mathcal{F}$$ $$f^*q^*q_*\mathcal{F} \to f^*\mathcal{F}$$ $$p^*q_*\mathcal{F} \to f^*\mathcal{F}$$ $$q_*\mathcal{F} \to p_*f^*\mathcal{F}.$$

In this case we get the same map (something which at least I find tedious to check; but I might be thinking of it in the wrong way).

My question is:

Is there a general coherence result which frees us from checking such equalities case by case, just as in the case of for instance symmetric monoidal categories. I'm thinking of something like: Start with a commutative diagram of ringed spaces and a map of sheaves of modules over one of the spaces. Is any map produced from this map, by just applying push-forwards and pull-backs and using adjunctions, uniquely determined by the strings of symbols in the domain and co-domain of the new map?

(One could probably state a similar question where we throw the tensor product into the mix of canonical operations.)

-

The isomorphism $f^* q^* \cong p^*$ induced by $q_* f_* \cong p_*$ is defined to be the composition

$f^* q^* \to f^* q^* p_* p^* \cong f^* q^* q_* f_* p^* \to f^* f_* p^* \to p^*$.

Now it is easily checked that the two definitions of the morphism agree. In fact, the first one is more natural, whereas the second one is somehow artificial since it coindices with the first one plus an expansion of the isomorphism $f^* q^* \cong p^*$, which is then removed again.

More generally, if $p: X \to S,~ p' : X' \to S,~ q' : X' \to X, ~q : S' \to S$ are morphisms (in your case $p=id$) such that the obvious diagram commutes, then there is a natural transformation $p'^* q_* \to q_* p'^*$. It is studied, for example, in EGA I, 9.3. Remark that we only use here that we have a weakly commutative diagramm of categories and functors such that the vertical functors $p_*,p'_*$ have left adjoints. See this paper by Calmes, Hornbostel (Lemma 1.2.6) for a generalization to categories.

-