Grothendieck groups of coherent sheaves and of vector bundles on a scheme

Assume the Axiom of Choice (The Axiom of Choice) inherited from the coherent-category and higher-direct-image suppliers. Let $X$ be a locally Noetherian scheme (Locally Noetherian and Noetherian schemes). Then the category of coherent ${\mathcal{O}}_X$-modules is abelian (Coherent sheaves on a locally Noetherian scheme, Coherent module sheaves), and the category of finite locally free ${\mathcal{O}}_X$-modules of locally constant rank is an exact category (Locally free sheaves of finite rank).

1. The Grothendieck group of coherent sheaves $K_0(X):=K_0(\mathrm{Coh}(X))$ is the abelian group with one generator $[\mathcal{F}]$ for each isomorphism class of coherent sheaves, subject to $[\mathcal{F}]=[{\mathcal{F}}^{\mathrm{\prime }}]+[{\mathcal{F}}^{\mathrm{\prime }\mathrm{\prime }}]$ for every short exact sequence $0\to {\mathcal{F}}^{\mathrm{\prime }}\to \mathcal{F}\to {\mathcal{F}}^{\mathrm{\prime }\mathrm{\prime }}\to 0$ (Grothendieck group of an essentially small abelian category); existence of the group is the group completion of the commutative monoid modulo the exact-sequence relations. These isomorphism classes form a set: on a fixed set-indexed affine cover, finite presentations give a set of local module models, and their overlap isomorphisms form sets; gluing those data gives a set of representatives. The same applies to vector bundles, using finite free local models.
2. The Grothendieck group of vector bundles $K^0(X)$ is the abelian group with one generator $[\mathcal{E}]$ for each isomorphism class of finite locally free sheaves of locally constant rank, subject to $[\mathcal{E}]=[{\mathcal{E}}^{\mathrm{\prime }}]+[{\mathcal{E}}^{\mathrm{\prime }\mathrm{\prime }}]$ for every exact sequence $0\to {\mathcal{E}}^{\mathrm{\prime }}\to \mathcal{E}\to {\mathcal{E}}^{\mathrm{\prime }\mathrm{\prime }}\to 0$ of such sheaves. Tensor product makes $K^0(X)$ a commutative ring with unit $[{\mathcal{O}}_X]$ (Tensor product of sheaves of modules, Tensor product preserves quasi-coherence), and makes $K_0(X)$ a $K^0(X)$-module via $[\mathcal{E}]\cdot [\mathcal{F}]:=[\mathcal{E}\otimes \mathcal{F}]$, using that tensoring with a locally free sheaf is exact.
3. Every morphism $f:X\to Y$ of locally Noetherian schemes induces $f^{\ast }:K^0(Y)\to K^0(X)$ by pullback of locally free sheaves (Scheme pullback preserves quasi-coherence, Dual and base change for finite locally free sheaves); flat $f$ also induces $f^{\ast }:K_0(Y)\to K_0(X)$.
4. Under the Axiom of Choice (The Axiom of Choice) inherited from the coherent-cohomology suppliers, if $f:X\to Y$ is proper between finite type schemes over a field, the higher direct images $R^q{f}_{\ast }\mathcal{F}$ are coherent (Coherent higher direct images under proper morphisms) and vanish for $q\gg 0$ over affine opens of $Y$ (Dimension bound for quasi-coherent cohomology on a Noetherian scheme, with the global bound $q>\dim X$); the resulting pushforward $f_{!}:K_0(X)\to K_0(Y)$ is defined in def-pushforward-in-algebraic-k-theory.
5. The natural map $K^0(X)\to K_0(X)$, $[\mathcal{E}]\mapsto [\mathcal{E}]$, is well defined and additive; under the same Axiom of Choice premise it is an isomorphism when $X$ is a regular quasi-projective scheme of finite type over a field (lem-k-zero-vector-bundles-versus-coherent-sheaves).