The Stacks project

Proof. Set $J = (f_1, \ldots , f_ c)$. We prove the first assertion by induction on $c$. We have to show that given any relation $\sum _{|I| = n} a_ I f^ I \in J^{n + 1}$ with $a_ I \in R$ we actually have $a_ I \in J$ for all multi-indices $I$. Since any element of $J^{n + 1}$ is of the form $\sum _{|I| = n} b_ I f^ I$ with $b_ I \in J$ we may assume, after replacing $a_ I$ by $a_ I - b_ I$, the relation reads $\sum _{|I| = n} a_ I f^ I = 0$. We can rewrite this as

Here and below the “primed” multi-indices $I'$ are required to be of the form $I' = (i_1, \ldots , i_{c - 1}, 0)$. We will show by descending induction on $l \in \{ 0, \ldots , n\}$ that if we have a relation

then $a_{I', e} \in J$ for all $I', e$. Namely, set $J' = (f_1, \ldots , f_{c-1})$. Observe that $\sum \nolimits _{|I'| = n - l} a_{I', l} f^{I'}$ is mapped into $(J')^{n - l + 1}$ by $f_ c^{l}$. By induction hypothesis (for the induction on $c$) we see that $f_ c^ l a_{I', l} \in J'$. Because $f_ c$ is not a zerodivisor on $R/J'$ (as $f_1, \ldots , f_ c$ is a regular sequence) we conclude that $a_{I', l} \in J'$. This allows us to rewrite the term $(\sum \nolimits _{|I'| = n - l} a_{I', l} f^{I'})f_ c^ l$ in the form $(\sum \nolimits _{|I'| = n - l + 1} f_ c b_{I', l - 1} f^{I'})f_ c^{l-1}$. This gives a new relation of the form

Now by the induction hypothesis (on $l$ this time) we see that all $a_{I', l-1} + f_ c b_{I', l - 1} \in J$ and all $a_{I', e} \in J$ for $e \leq l - 2$. This, combined with $a_{I', l} \in J' \subset J$ seen above, finishes the proof of the induction step.

The second assertion means that given any formal expression $F = \sum _{|I| = n} m_ I X^ I$, $m_ I \in M$ with $\sum m_ I f^ I \in J^{n + 1}M$, then all the coefficients $m_ I$ are in $J$. This is proved in exactly the same way as we prove the corresponding result for the first assertion above. $\square$

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$

Proof. Consider the kernel $K$ of the map (10.69.0.1). As $M/JM \otimes _{R/J} R/J[X_1, \ldots , X_ c]$ is a finite $R/J[X_1, \ldots , X_ c]$-module and as $R/J[X_1, \ldots , X_ c]$ is Noetherian, we see that $K$ is also a finite $R/J[X_1, \ldots , X_ c]$-module. Pick homogeneous generators $k_1, \ldots , k_ t \in K$. By assumption for each $i = 1, \ldots , t$ there exists a $g_ i \in R$, $g_ i \not\in \mathfrak p$ such that $g_ i k_ i = 0$. Hence $g = g_1 \ldots g_ t$ works. $\square$

Proof. It suffices to prove this for $i = 1$. Set $\overline{J} = (\overline{f}_2, \ldots , \overline{f}_ c) \subset \overline{R}$. Then

Thus, in order to prove the lemma it suffices to show that $J^{n + 1}M + J^ nM \cap f_1M = J^{n + 1}M + f_1J^{n - 1}M$ because that will show that $\bigoplus _{n \geq 0} \overline{J}^ n\overline{M}/\overline{J}^{n + 1}\overline{M}$ is the quotient of $\bigoplus _{n \geq 0} J^ nM/J^{n + 1}M \cong M/JM[X_1, \ldots , X_ c]$ by $X_1$. Actually, we have $J^ nM \cap f_1M = f_1J^{n - 1}M$. Namely, if $m \not\in J^{n - 1}M$, then $f_1m \not\in J^ nM$ because $\bigoplus J^ nM/J^{n + 1}M$ is the polynomial algebra $M/J[X_1, \ldots , X_ c]$ by assumption. $\square$

Proof. Set $J = (f_1, \ldots , f_ c)$. Let us show that $f_1$ is a nonzerodivisor on $M$. Suppose $x \in M$ is not zero. By Krull's intersection theorem there exists an integer $r$ such that $x \in J^ rM$ but $x \not\in J^{r + 1}M$, see Lemma 10.51.4. Then $f_1 x \in J^{r + 1}M$ is an element whose class in $J^{r + 1}M/J^{r + 2}M$ is nonzero by the assumed structure of $\bigoplus J^ nM/J^{n + 1}M$. Whence $f_1x \not= 0$.

Now we can finish the proof by induction on $c$ using Lemma 10.69.5. $\square$

Proof. This is true because $J^ nM/J^{n + 1}M \cong \overline{J}^ n\overline{M}/\overline{J}^{n + 1}\overline{M}$. $\square$