Pushforward of coherent sheaves in algebraic K-theory

Assume the Axiom of Choice and the Axiom of Dependent Choice, inherited from the coherence and finiteness suppliers below (The Axiom of Choice, The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$-indexed chain). Let $k$ be a field and let $f:X\to Y$ be a proper morphism of schemes of finite type over $k$ (Proper morphisms, Locally finite type and finite type morphisms); then $Y$ is locally Noetherian and for every coherent ${\mathcal{O}}_X$-module $\mathcal{F}$ all higher direct images $R^q{f}_{\ast }\mathcal{F}$ are coherent ${\mathcal{O}}_Y$-modules (Coherent higher direct images under proper morphisms, Higher direct image of a sheaf) and vanish for all sufficiently large $q$ (Dimension bound for quasi-coherent cohomology on a Noetherian scheme on the separated Noetherian preimage of each affine open of $Y$, giving the single global bound $q>\dim X$). Set $f_{!}[\mathcal{F}]:={\sum }_{q\ge 0}(-1{)}^q[R^q{f}_{\ast }\mathcal{F}]\in K_0(Y)$ (Grothendieck groups of coherent sheaves and of vector bundles on a scheme). Then:

1. $f_{!}$ is a well-defined homomorphism $K_0(X)\to K_0(Y)$ of abelian groups: a short exact sequence $0\to {\mathcal{F}}^{\mathrm{\prime }}\to \mathcal{F}\to {\mathcal{F}}^{\mathrm{\prime }\mathrm{\prime }}\to 0$ on $X$ induces the long exact sequence of higher direct images $0\to f_{\ast }{\mathcal{F}}^{\mathrm{\prime }}\to f_{\ast }\mathcal{F}\to f_{\ast }{\mathcal{F}}^{\mathrm{\prime }\mathrm{\prime }}\to R^1{f}_{\ast }{\mathcal{F}}^{\mathrm{\prime }}\to \cdots$ (Higher direct image of a sheaf, The derived long exact sequence), whose alternating sum is zero, giving $f_{!}[\mathcal{F}]=f_{!}[{\mathcal{F}}^{\mathrm{\prime }}]+f_{!}[{\mathcal{F}}^{\mathrm{\prime }\mathrm{\prime }}]$.
2. (Functoriality) ${\mathrm{id}}_{!}=\mathrm{id}$ and $(g\circ f{)}_{!}=g_{!}\circ f_{!}$ for composable proper morphisms: the bounded Leray spectral sequence for the composition preserves its total alternating class on every page; no degeneration or splitting is asserted (Leray spectral sequence for sheaf cohomology).
3. (Compatibility with the module structure) $f_{!}(f^{\ast }[\mathcal{E}]\cdot [\mathcal{F}])=[\mathcal{E}]\cdot f_{!}[\mathcal{F}]$ for $\mathcal{E}$ locally free on $Y$ and $\mathcal{F}$ coherent on $X$, i.e. the projection formula; this is proved in lem-projection-formula-in-algebraic-k-theory. For $Y=\mathrm{Spec}k$ and $X$ projective, $f_{!}[\mathcal{F}]=\chi (X,\mathcal{F})$ is the Euler characteristic (Euler characteristic of a coherent sheaf, Euler characteristic is additive in short exact sequences).

Well-definedness. The sum in the definition is finite because $R^q{f}_{\ast }\mathcal{F}=0$ for $q>\dim X$: for an affine open $U\subseteq Y$ the preimage $f^{-1}U$ is separated, Noetherian and of dimension at most $\dim X$, and Dimension bound for quasi-coherent cohomology on a Noetherian scheme bounds its quasi-coherent cohomology uniformly, the higher direct image being the sheafification of these local cohomology groups (Cech cohomology computes quasi-coherent cohomology on a separated scheme). Additivity in short exact sequences is the alternating-sum cancellation in the bounded long exact sequence of higher direct images, together with the coherence of every term (Coherent higher direct images under proper morphisms, Grothendieck groups of coherent sheaves and of vector bundles on a scheme). For the composition spectral sequence apply Grothendieck spectral sequence to $f_{\ast }$ and $g_{\ast }$ on module sheaves. Module-injective sheaves are flasque (Injective modules are flasque and Ext from the structure sheaf is cohomology), their direct images are flasque, and flasque sheaves are acyclic on every open (Flasque abelian sheaves are Γ-acyclic). As in the module/abelian comparison in Leray spectral sequence for sheaf cohomology, this makes them $g_{\ast }$-acyclic and supplies the required acyclicity hypothesis. Functoriality is then page-invariance of the total alternating class: for composable proper $f:X\to Y$, $g:Y\to Z$ the $E_2$ page $R^p{g}_{\ast }(R^q{f}_{\ast }\mathcal{F})$ is bounded in both directions by the uniform dimension bounds for $f$, $g$ and $gf$, each differential changes total degree by one so that the two kernel/image short exact sequences cancel every image class, and the finite abutment filtration identifies the invariant with the alternating class of $R^{\bullet }(g\circ f{)}_{\ast }\mathcal{F}$ (Leray spectral sequence for sheaf cohomology); no degeneration is used. The projection formula is proved separately in lem-projection-formula-in-algebraic-k-theory, and for $Y=\mathrm{Spec}k$ the definition reduces to the Euler characteristic.