Lemma 10.31.2. If $R$ is a Noetherian ring, then so is the formal power series ring $R[[x_1, \ldots , x_ n]]$.

Proof. Since $R[[x_1, \ldots , x_{n + 1}]] \cong R[[x_1, \ldots , x_ n]][[x_{n + 1}]]$ it suffices to prove the statement that $R[[x]]$ is Noetherian if $R$ is Noetherian. Let $I \subset R[[x]]$ be a ideal. We have to show that $I$ is a finitely generated ideal. For each integer $d$ denote $I_ d = \{ a \in R \mid ax^ d + \text{h.o.t.} \in I\}$. Then we see that $I_0 \subset I_1 \subset \ldots$ stabilizes as $R$ is Noetherian. Choose $d_0$ such that $I_{d_0} = I_{d_0 + 1} = \ldots$. For each $d \leq d_0$ choose elements $f_{d, j} \in I \cap (x^ d)$, $j = 1, \ldots , n_ d$ such that if we write $f_{d, j} = a_{d, j}x^ d + \text{h.o.t}$ then $I_ d = (a_{d, j})$. Denote $I' = (\{ f_{d, j}\} _{d = 0, \ldots , d_0, j = 1, \ldots , n_ d})$. Then it is clear that $I' \subset I$. Pick $f \in I$. First we may choose $c_{d, i} \in R$ such that

$f - \sum c_{d, i} f_{d, i} \in (x^{d_0 + 1}) \cap I.$

Next, we can choose $c_{i, 1} \in R$, $i = 1, \ldots , n_{d_0}$ such that

$f - \sum c_{d, i} f_{d, i} - \sum c_{i, 1}xf_{d_0, i} \in (x^{d_0 + 2}) \cap I.$

Next, we can choose $c_{i, 2} \in R$, $i = 1, \ldots , n_{d_0}$ such that

$f - \sum c_{d, i} f_{d, i} - \sum c_{i, 1}xf_{d_0, i} - \sum c_{i, 2}x^2f_{d_0, i} \in (x^{d_0 + 3}) \cap I.$

And so on. In the end we see that

$f = \sum c_{d, i} f_{d, i} + \sum \nolimits _ i (\sum \nolimits _ e c_{i, e} x^ e)f_{d_0, i}$

is contained in $I'$ as desired. $\square$

Comment #343 by Fred on

I guess in the fourth line, ''... then $I_d=(a_{d,j})$'' means ''... then $I_d=(a_{d,1},a_{d,2},\dots,a_{d,n_d})$''? That notation is confusing imo.

Comment #352 by on

Yes. I am not sure what would be a better notation. Any suggestions?

In your comment you can use Markdown and LaTeX style mathematics (enclose it like $\pi$). A preview option is available if you wish to see how it works out (just click on the eye in the toolbar).