The Stacks project

Proof. Set $J = (f_1, \ldots , f_ r)$, $J' = JR'$ and $M' = M \otimes _ R R'$. We have to show the canonical map $\mu : R'/J'[X_1, \ldots X_ r] \otimes _{R'/J'} M'/J'M' \to \bigoplus (J')^ nM'/(J')^{n + 1}M'$ is an isomorphism. Because $R \to R'$ is flat the sequences $0 \to J^ nM \to M$ and $0 \to J^{n + 1}M \to J^ nM \to J^ nM/J^{n + 1}M \to 0$ remain exact on tensoring with $R'$. This first implies that $J^ nM \otimes _ R R' = (J')^ nM'$ and then that $(J')^ nM'/(J')^{n + 1}M' = J^ nM/J^{n + 1}M \otimes _ R R'$. Thus $\mu $ is the tensor product of (10.69.0.1), which is an isomorphism by assumption, with $\text{id}_{R'}$ and we conclude. $\square$