Tensor product preserves quasi-coherence

The affine comparison morphism: let $U=\mathrm{Spec}A$ with $\mathcal{F}{\mathrm{\mid }}_U\cong \tilde{M}$ and $\mathcal{G}{\mathrm{\mid }}_U\cong \tilde{N}$. For $f\in A$ the universal property of the tensor product over the ring $A_f$ gives a well-defined $A_f$-linear map ${\delta }_f:\widetilde{(M{\otimes }_{A}N)}(D(f))=(M{\otimes }_{A}N{)}_f\cong M_f{\otimes }_{A_f}{N}_f⟶(\tilde{M}{\otimes }_{{\mathcal{O}}_U}\tilde{N})(D(f)),\frac{m}{f^k}\otimes \frac{n}{f^l}⟼\frac{m}{f^k}\otimes \frac{n}{f^l},$ from the localised tensor into the presheaf tensor of the sections, composed with the sheafification map; it is well defined because both sides are the localisations of the tensor product and of the section modules [F1, F5]. For $D(g)\subseteq D(f)$ the restriction maps of the two sheaves correspond under ${\delta }_g$ and ${\delta }_f$, since restriction in both is the canonical localisation (of $M{\otimes }_{A}N$, of $M$ and of $N$) and the tensor of the localisation maps is the localisation of the tensor [F3, F5]; hence the compatible maps ${\delta }_f$ on the basis of distinguished opens determine a morphism of ${\mathcal{O}}_U$-modules $\delta :\widetilde{(M{\otimes }_{A}N)}⟶\tilde{M}{\otimes }_{{\mathcal{O}}_U}\tilde{N}\mathrm{.}$

The morphism is an isomorphism on stalks: fix $\mathfrak{p}\in U$. By [F2] the stalk of the tensor product of the associated sheaves is $(\tilde{M}{\otimes }_{{\mathcal{O}}_U}\tilde{N}{)}_{\mathfrak{p}}\cong (\tilde{M}{)}_{\mathfrak{p}}{\otimes }_{A_{\mathfrak{p}}}(\tilde{N}{)}_{\mathfrak{p}}\cong M_{\mathfrak{p}}{\otimes }_{A_{\mathfrak{p}}}{N}_{\mathfrak{p}},$ while by [F2] and [F3] the stalk of the associated tensor is ${\widetilde{(M{\otimes }_{A}N)}}_{\mathfrak{p}}\cong (M{\otimes }_{A}N{)}_{\mathfrak{p}}\cong M_{\mathfrak{p}}{\otimes }_{A_{\mathfrak{p}}}{N}_{\mathfrak{p}}\mathrm{.}$ Under these identifications the map ${\delta }_{\mathfrak{p}}$ sends the class of $m\otimes n$ to the class of $m\otimes n$, and since the classes of the pure tensors generate both sides as $A_{\mathfrak{p}}$-modules, ${\delta }_{\mathfrak{p}}$ is the canonical isomorphism between the two copies of $M_{\mathfrak{p}}{\otimes }_{A_{\mathfrak{p}}}{N}_{\mathfrak{p}}$; in particular ${\delta }_{\mathfrak{p}}$ is bijective for every $\mathfrak{p}$.

The affine identification: a morphism of sheaves of modules is an isomorphism if and only if all of its stalk maps are isomorphisms, so step 2.1 shows that $\delta$ is an isomorphism of ${\mathcal{O}}_U$-modules; hence $(\mathcal{F}{\otimes }_{{\mathcal{O}}_X}\mathcal{G}){\mathrm{\mid }}_U\cong \tilde{M}{\otimes }_{{\mathcal{O}}_U}\tilde{N}\cong \widetilde{(M{\otimes }_{A}N)}$ by [F1], which is the displayed affine form.

Global quasi-coherence: let $x\in X$. Since $\mathcal{F}$ and $\mathcal{G}$ are quasi-coherent, choose affine opens $U_{\mathcal{F}}\ni x$ and $U_{\mathcal{G}}\ni x$ with $\mathcal{F}{\mathrm{\mid }}_{U_{\mathcal{F}}}\cong \tilde{M}$ and $\mathcal{G}{\mathrm{\mid }}_{U_{\mathcal{G}}}\cong \tilde{N}$; then $U_{\mathcal{F}}\cap U_{\mathcal{G}}$ is an open neighbourhood of $x$ in the affine scheme $U_{\mathcal{F}}$, so by [F5] it contains a distinguished open $D(f)$ with $x\in D(f)$, and $D(f)=\mathrm{Spec}{A}_f$ is affine with $\mathcal{F}{\mathrm{\mid }}_{D(f)}\cong \widetilde{(M_f)}$ and, writing $U_{\mathcal{G}}=\mathrm{Spec}B$, the affine-open restriction lemma in [F5] gives $\mathcal{G}{\mathrm{\mid }}_{D(f)}\cong \widetilde{(A_f{\otimes }_{B}N)}$, using the restriction map $B\to A_f$. Therefore the family of all affine opens $U\subseteq X$ on which both $\mathcal{F}$ and $\mathcal{G}$ are associated covers $X$, and for each member the restriction of $\mathcal{F}{\otimes }_{{\mathcal{O}}_X}\mathcal{G}$ is $\widetilde{(M{\otimes }_{A}N)}$ by step 3.1, in particular an associated sheaf; by the affine cover criterion [F4] the tensor product $\mathcal{F}{\otimes }_{{\mathcal{O}}_X}\mathcal{G}$ is quasi-coherent.

Choice accounting: the cover used in step 4.1 is the family of all affine opens on which both sheaves are associated, which is determined by the data, so no chart, module or isomorphism is selected; the comparison morphism $\delta$ of step 1.1 is built from the canonical localisation maps and the universal property of the tensor product, and the identifications of step 2.1 are the canonical stalk maps. Thus the only use of the Axiom of Choice is the inherited one recorded in the Statement through [F6].