Add a proof to morphisms

Thanks to  Elías Guisado who submitted this + edits from me

morphisms.tex

@@ -1809,6 +1809,54 @@ \section{Affine morphisms}
 Constructions, Lemma \ref{constructions-lemma-spec-properties} part (2).
 \end{proof}
 
+\begin{lemma}
+\label{lemma-quasi-coherence-scalar-restriction}
+Let $S$ be a scheme and let $\mathcal{A}$ be a quasi-coherent
+$\mathcal{O}_S$-algebra. An $\mathcal{A}$-module is
+quasi-coherent as an $\mathcal{O}_S$-module if and only if
+it is quasi-coherent as an $\mathcal{A}$-module.
+\end{lemma}
+
+\begin{proof}
+Let $\mathcal{F}$ be an $\mathcal{A}$-module.
+If $\mathcal{F}$ is quasi-coherent as an $\mathcal{A}$-module, then
+for every $s \in S$ there exists an open neighbourhood $U$ of $s$
+and an exact sequence
+$$
+\bigoplus\nolimits_J\mathcal{A}|_U\to
+\bigoplus\nolimits_I\mathcal{A}|_U\to
+\mathcal{F}|_U
+$$
+of $\mathcal{A}|_U$-modules.
+Then this is also an exact sequence of $\mathcal{O}_U$-modules.
+Hence $\mathcal{F}|_U$ is quasi-coherent as the cokernel of a morphism
+of quasi-coherent $\mathcal{O}_U$-modules on a scheme. It follows
+that $\mathcal{F}$ is quasi-coherent as an $\mathcal{O}_X$-module.
+
+\medskip\noindent
+Conversely, assume $\mathcal{F}$ is quasi-coherent as an $\mathcal{O}_X$-module.
+Pick an open affine $\Spec(R) = U \subset S$. We have isomorphisms of
+$\mathcal{O}_U$-modules $\mathcal{A}|_U \cong \widetilde{A}$ and
+$\mathcal{F}|_U \cong \widetilde{M}$, for some $R$-algebra $A$
+and some $R$-module $M$. The $\mathcal{A}$-module structure on $\mathcal{F}$
+translates into an $A$-module structure on $M$ compatible with the
+given $R$-module structure (details omitted). Choose an exact sequence
+$$
+\bigoplus\nolimits_J A \to
+\bigoplus\nolimits_I A \to
+M \to 0
+$$
+of $A$-modules. Since the functor $\widetilde{\ }$ is exact, this
+produces an exact sequence
+$$
+\bigoplus\nolimits_J \widetilde{A}\to
+\bigoplus\nolimits_I \widetilde{A}\to
+\widetilde{M} \to 0
+$$
+of $\widetilde{A}$-modules. This means that
+$\mathcal{F}$ is quasi-coherent as an $\mathcal{A}$-module.
+\end{proof}
+
 \begin{lemma}
 \label{lemma-affine-equivalence-modules}
 Let $f : X \to S$ be an affine morphism of schemes.
@@ -1836,7 +1884,51 @@ \section{Affine morphisms}
 \end{lemma}
 
 \begin{proof}
-Omitted.
+The final statement is Lemma \ref{lemma-quasi-coherence-scalar-restriction}.
+By Lemma \ref{lemma-affine-separated} and
+Schemes, Lemma \ref{schemes-lemma-push-forward-quasi-coherent}
+the pushforward $f_*\mathcal{F}$ of a quasi-coherent $\mathcal{O}_X$-module
+$\mathcal{F}$
+is a quasi-coherent $\mathcal{O}_S$-module. Hence a functor as in
+the statement of the lemma.
+
+\medskip\noindent
+We will construct an quasi-inverse $h$ to this functor. Let $\mathcal{G}$
+be a quasi-coherent $\mathcal{A}$-module. Then we set
+$$
+h(\mathcal{G}) = f^*\mathcal{G} \otimes_{f^*\mathcal{A}} \mathcal{O}_X =
+f^*\mathcal{G} \otimes_{f^*f_*\mathcal{O}_X} \mathcal{O}_X
+$$
+Elucidation: the pullback $f^*\mathcal{A} = f^*f_*\mathcal{O}_X$
+is an $\mathcal{O}_X$-algebra, the adjunction map
+$f^*f_*\mathcal{O}_X \to \mathcal{O}_X$ is an algebra homomorphism, and
+the pullback $f^*\mathcal{G}$ is an $f^*\mathcal{A}$-module. Observe that
+$h(\mathcal{G})$ is quasi-coherent as quasi-coherence is preserved by
+pullbacks and change of rings. Observe that there is a functorial map
+$$
+h(f_*\mathcal{F}) =
+f^*f_*\mathcal{F} \otimes_{f^*f_*\mathcal{O}_X} \mathcal{O}_X \to \mathcal{F}
+$$
+coming from the adjunction map $f^*f_*\mathcal{F} \to \mathcal{F}$ and
+a functorial map
+$$
+\mathcal{G} \to f_*h(\mathcal{G}) \quad\text{adjoint to the map}\quad
+f^*\mathcal{G} \to f^*\mathcal{G} \otimes_{f^*f_*\mathcal{O}_X} \mathcal{O}_X
+$$
+which sends a local section $s$ of $f^*\mathcal{F}$ to $s \otimes 1$.
+To finish the proof it suffices to show that these maps are isomorphisms
+for $\mathcal{F}$ and $\mathcal{G}$ as above. This may be checked on the
+members of an affine covering, i.e., when $X$ and $S$ are affine.
+
+\medskip\noindent
+The key algebra observation which makes this work is the
+following: Let $R \to A$ be a ring map. Let $N$ be an $A$-module. Then
+$$
+(N \otimes_R A) \otimes_{(A \otimes_R A)} A = N
+$$
+Namely, the left hand side of this equality is the effect of applying
+$h$ to the quasi-coherent $\widetilde{A}$-module $\widetilde{N}$ on $\Spec(R)$.
+We omit the details.
 \end{proof}
 
 \begin{lemma}