Cohomology comparison when higher direct images vanish

Apply the Godement construction to the underlying abelian sheaf of $\mathcal{F}$, retaining its module structure. For a module $G$, the first term on an open $U$ is ${\prod }_{x\in U}{G}_x$, with $a\in {\mathcal{O}}_X(U)$ acting through its germ on each factor. The germ map is module-linear; take its module cokernel and repeat. Since these cokernels have the same underlying abelian sheaves, this yields an exact functorial module resolution $\mathcal{F}\to G^{\bullet }$ whose terms are flasque and whose section complex computes $H^n(X,\mathcal{F})$. All modules and syzygies lie in the supplied datum's domain, and Choice supplies the required Dependent Choice.

Every flasque module $G$ is $f_{\ast }$-acyclic: on every open $V\subset Y$, flasque acyclicity gives $H^q(f^{-1}V,G)=0$ for $q>0$, and the local-section formula gives $R^q{f}_{\ast }G=0$. Moreover $f_{\ast }G$ is flasque, since its restrictions are the restrictions of $G$ along inverse-image opens. These facts hold for arbitrary $f$.

Apply the acyclic-resolution theorem to $f_{\ast }$ and $G^{\bullet }$. It identifies the cohomology sheaves of $f_{\ast }{G}^{\bullet }$ with $R^q{f}_{\ast }\mathcal{F}$. The hypothesis makes this an exact coaugmented resolution of $f_{\ast }\mathcal{F}$, and its terms are flasque by step 1.2. Forget the ${\mathcal{O}}_Y$-module structure, preserving exactness by [F2]. All terms and syzygies are then in $\mathrm{A}\mathrm{b}(Y)$, the full domain of the supplied cohomology datum. Apply the acyclic-resolution theorem to $\mathrm{\Gamma }(Y,-)$ on that category; this resolution computes $H^n(Y,f_{\ast }\mathcal{F})$. Its global section complex equals $\mathrm{\Gamma }(X,G^{\bullet })$ term by term, so step 1.1 gives the claimed comparison isomorphism.

Functoriality of Godement and of the acyclic-resolution comparisons makes these identifications natural and independent of presentations. In degree zero they are exactly the equality of direct-image global sections. Restricting over an open of $Y$ repeats the same proof. Empty schemes and the zero module give zero complexes, and for the identity morphism the comparison is the identity.