The Stacks project

Proof. Let $A, f, J$ be as in Example 38.37.10. Since all our schemes are affine and since we have internal Hom in the category of vector bundles, the fully faithfulness of the functor follows if we can show that

for a finite projective $A$-module $P$. After writing $P$ as a summand of a finite free module, this follows from the case where $P$ is finite free. This case immediately reduces to the case $P = A$. The case $P = A$ follows from Lemma 38.38.2 (in fact we proved this case directly in the proof of this lemma).

Essential surjectivity. Here we obtain the following algebra problem. Suppose $P_1$ is a finite projective $A/J$-module, $P_2$ is a finite projective $A/fA$-module, and

is an isomorphism. Goal: show that there exists an $N$, a finite projective $A$-module $P$, an isomorphism $\varphi _1 : P \otimes _ A A/J \to P_1 \otimes _{A/J, F^ N} A/J$, and an isomorphism $\varphi _2 : P \otimes _ A A/fA \to P_2 \otimes _{A/fA, F^ N} A/fA$ compatible with $\varphi$ in an obvious manner. This can be seen as follows. First, observe that

Hence by More on Algebra, Lemma 15.6.9 there is a finite projective module $P'$ over $A/(J \cap fA)$ which comes with isomorphisms $\varphi '_1 : P' \otimes _ A A/J \to P_1$ and $\varphi _2 : P' \otimes _ A A/fA \to P_2$ compatible with $\varphi$. Since $J$ is a finitely generated ideal and $f$-power torsion we see that $J \cap fA$ is a nilpotent ideal. Hence for some $N$ there is a factorization

of $F^ N$. Setting $P = P' \otimes _{A/(J \cap fA), \beta } A$ we conclude. $\square$