The Stacks project

Proof. Set $\overline{M} = M/M[f^\infty ]$. Then $\mathop{\mathrm{Coker}}(M \to M_ f) \cong \mathop{\mathrm{Coker}}(\overline{M} \to \overline{M}_ f)$ hence we may and do assume that $f$ is a nonzerodivisor on $M$. In this case $M \subset M_ f$ and $M_ f/M = \mathop{\mathrm{colim}}\nolimits M/f^ nM$ where the transition maps are given by multiplication by $f$. Since formation of Tor groups commutes with colimits (Algebra, Lemma 10.76.2) it suffices to show that $\text{Tor}^ R_1(R', M/f^ n M) = 0$.

We first treat the case $M = R/R[f^\infty ]$. By Lemma 15.90.6 we have $M \otimes _ R R' = R'/R'[f^\infty ]$. From the short exact sequence $0 \to M \to M \to M/f^ nM \to 0$ we obtain the exact sequence

by Algebra, Lemma 10.75.2. Here the diagonal arrow is injective. Since the first group $\text{Tor}_1^ R(R', R/R[f^\infty ])$ is zero by Lemma 15.90.14, we deduce that $\text{Tor}_1^ R(R', M/f^ nM) = 0$ as desired.

To treat the general case, choose a surjection $F \to M$ with $F$ a free $R/R[f^\infty ]$-module, and form an exact sequence

By Lemma 15.88.8 this sequence remains unchanged, and hence exact, upon tensoring with $R'$. Since $\text{Tor}^ R_1(R', F/f^ n F) = 0$ by the previous paragraph, we deduce that $\text{Tor}^ R_1(R', M/f^ n M) = 0$ as desired. $\square$