The Stacks project

Proof. Assume that $M \otimes _ R R'$ is a finite projective module over $R'$ and that $M_ f$ is a finite projective module over $R_ f$. Our task is to prove that $M$ is finite projective over $R$. We will use Algebra, Lemma 10.78.2 without further mention. By Lemma 15.90.18 we see that $M$ is flat. By Lemma 15.90.4 we see that $M$ is finite. Choose a short exact sequence $0 \to K \to R^{\oplus n} \to M \to 0$. Since a finite projective module is of finite presentation and since the sequence remains exact after tensoring with $R'$ (by Algebra, Lemma 10.39.12) and $R_ f$, we conclude that $K \otimes _ R R'$ and $K_ f$ are finite modules. Using the lemma above we conclude that $K$ is finitely generated. Hence $M$ is finitely presented and hence finite projective. $\square$