I am trying to find a reference for the following well-known result on the functoriality of the Leray spectral sequence:


Let $\pi:X\to Y$ and $\pi':X'\to Y'$ be morphisms of schemes and denote by $E\_2^{p,q}(\mathcal{F})=\mathrm{H}^q(Y,R^q\pi\_\*\mathcal{F})\implies \mathrm{H}^{p+q}(X,\mathcal{F})$ and $(E')\_2^{p,q}(\mathcal{G})\implies \mathrm{H}^{p+q}(X',\mathcal{G})$ their associated Leray spectral sequences (in étale cohomology for some étale sheafs $\mathcal{F},\mathcal{G}$). Assume that there are $f:X'\to X$ and $g:Y'\to Y$ such that the obvious square commutes. Then there is a morphism of spectral sequences $E\_r^{p,q}(\mathcal{F})\to (E')^{p,q}\_r(g^{-1}\mathcal{F})$ induced by the natural pullback maps on cohomology $E\_2^{p,q}(\mathcal{F})\to (E')\_2^{p,q}(g^{-1}\mathcal{F})$ such that the map on the infinity-pages agrees with the canonical pullback morphism $\mathrm{H}^n(X,\mathcal{F})\to \mathrm{H}^n(X',f^{-1}\mathcal{F})$.


It would be amazing if someone knows a reliable source for this frequently used result. Thanks in advance!



Leray spectral sequence and pullbacks
I apologize for the self promotion, but page 570 of my article *The Leray spectral sequence is motivic* has a very brief discussion of the functoriality of Leray.


**Added** In a bit more detail, here are the key points:


* To every object $(C, F)$ in the (bounded below, biregularly filtered) filtered derived category, one has a spectral sequence
with $E\_1^{pq}= H^{p+q}(Gr^p\_FC)$. This construction is functorial. See Deligne, Théorie de Hodge II, sect. 1; III, sect. 7.
* With your notation, the spectral sequence associated to
$(\mathbb{R} \pi\_\* \mathcal{F},\tau)$ becomes the Leray spectral sequence after reindexing to transform $E\_1$ to $E\_2$ [loc. cit.]. Here $\tau$ is the canonical filtration, given by truncations.
* Let $\mathcal{F}'= f^{-1}\mathcal{F}$. Then
we have a morphism in the filtered derived category
$$ (\mathbb{R} \pi\_\* \mathcal{F},\tau)\to \mathbb{R}g\_\*(\mathbb{R} \pi'\_\* \mathcal{F}',\tau)$$
This will induce a morphism of Leray spectral sequences.


