Theorem: Power Series Ring over Noetherian Ring is Noetherian

Let $A$ be a Noetherian ring.
Let $A \sqbrk x$ be the formal power series ring over $A$ in the single indeterminate $x$.
Then $A \sqbrk x$ is also a Noetherian ring.

Proof:
Let $I$ be an ideal of $A \sqbrk x$.
We show that $I$ is finitely generated.
If $0 \ne g \in A \sqbrk x$, define $\order g$ as the largest non-negative integer $n$ such that $x^n$ divides $g$, and $\order 0 = \infty$.
{{explain|What does "divides" mean in this context? "Division" as such is defined on {{ProofWiki}} only for division rings.}}
For a non-negative integer $n$, define:
:$S_n = \set {a \in A: \exists f \in I: \order {f - a x^n} > n}$
Note:
:$S_n = \set {a \in A: \exists f \in I: \order f = n \text{ and } [x^n] f = a}$
where $[x^n] f$ denotes the $x^n$ term of $f$.
We first show $S_n$ is an ideal of $A$ for all $n$.
Note $0 \in S_n$ since $\order {x^{n + 1} - 0 x^n} = n + 1 > n$, so $S_n$ is nonempty.
Let $r,s\in S_n$ and $a\in A$.
Let $f,g\in I$ such that $\order {f - r x^n} > n$ and $\order {g - s x^n} > n$.
Then $\order {\paren {f - a g} - \paren {r - a s} x^n} > n$, so $r - a s \in S_n$.
Thus $S_n$ is an ideal of $A$.
Next, we show $S_n\subseteq S_{n+1}$ for all $n$.
Let $r \in S_n$ and $f \in I$ such that $\order {f - a x^n} > n$.
Then:
:$\order {x f - a x^{n + 1} } > n + 1$
so $r \in S_{n + 1}$.
Thus $S_0 \subseteq S_1 \subseteq \cdots$ is an ascending chain of ideals of $A$.
Since $A$ is Noetherian, there exists a non-negative integer $k$ such that $S_k = S_{k + i}$ for all non-negative integers $i$.
Since $A$ is Noetherian, for $n \le k$, let $r_{n, 1}, \ldots, r_{n, m_n}$ generate $S_n$ and for $1 \le i \le m_n$, let $f_{n,i}\in I$ such that $\order {f_{n, i} - r_{n, i} x^n} > n$.
Let $F = \ideal {f_{1, 1}, \ldots, f_{k, m_k} }$.
We will prove $I = F$.
Clearly, $F \subseteq I$ by definition of each $f_{i, j}$.
Let $g \in I$ and define $l = \order g$.
First, suppose $l \ge k$.
Define $g_0 = g$ and $g_j, \alpha_{i, j}$ inductively on $j$ as follows.
Let $s = [x^{k + j}] g_j$.
We have $s \in S_{k + j} = S_k$.
Hence there exist $\alpha_{1, j}, \ldots, \alpha_{m_k, j} \in A$ such that:
:$s = \ds \sum_{i \mathop = 1}^{m_k} \alpha_{i, j} r_{k, i}$
Define:
:$g_{j + 1} = g_j - \ds \sum_{i \mathop = 1}^{m_k} \alpha_{i, j} f_{k, i} x^J$
so that:
:$\order {g_{j + 1} } > j$
Define:
:$h_i = \ds\sum_{j \mathop = 0}^\infty \alpha_{i, j} x^j \in A \sqbrk x$
We show that:
:$g = \ds \sum_{i \mathop = 1}^{m_k} h_i f_{k, i}$
Let:
:$z := g - \ds \sum_{i \mathop = 1}^{m_k} h_i f_{k, i}$
Observe that:
:$z = g - \ds \sum_{i \mathop = 1}^{m_k} h_i f_{k, i} = g - \sum_{i \mathop = 1}^{m_k} \sum_{j \mathop = 0}^\infty \alpha_{i, j} x^j f_{k, i} = g - \sum_{j \mathop = 0}^\infty \sum_{i \mathop = 1}^{m_k} \alpha_{i, j} x^j f_{k, i}$
We show that:
:$z = g_J - \ds \sum_{j \mathop = J}^\infty \sum_{i \mathop = 1}^{m_k} \alpha_{i, j} x^j f_{k, i}$
for all non-negative integers $J$.
We induct on $J$.
The base case $J = 0$ is true as $g_0 = g$.
So suppose that:
:$z = g_K - \ds \sum_{j \mathop = K}^\infty \sum_{i \mathop = 1}^{m_k} \alpha_{i, j} x^j f_{k, i}$
for all $K \le J$.
Then:
:$z = g_J - \ds \sum_{j \mathop = J}^\infty \sum_{i \mathop = 1}^{m_k} \alpha_{i, j} x^j f_{k, i}$
by the inductive hypothesis.
By construction:
:$g_{J + 1} = g_J - \ds \sum_{i \mathop = 1}^{m_k} \alpha_{i, j} f_{k, i} x^J$
Thus:
:$z = g_J - \ds \sum_{j \mathop = J}^\infty \sum_{i \mathop = 1}^{m_k} \alpha_{i, j} x^j f_{k, i} = \paren {g_J - \sum_{i \mathop = 1}^{m_k} \alpha_{i, J} f_{k, i} } - \sum_{j \mathop = J + 1}^\infty \sum_{i \mathop = 1}^{m_k} \alpha_{i, j} x^j f_{k, i}$
Hence:
:$z = g_{J + 1} - \ds \sum_{j \mathop = J + 1}^\infty \sum_{i \mathop = 1}^{m_k} \alpha_{i, j} x^j f_{k, i}$
So now:
:$\order z = \order {g_J - \ds \sum_{j \mathop = J}^\infty \sum_{i \mathop = 1}^{m_k} \alpha_{i, j} x^j f_{k, i} }$
for all non-negative integers $J$.
So for all $J$:
:$\order {g_J} \ge J$
and:
:$\ds \sum_{j \mathop = J}^\infty \sum_{i \mathop = 1}^{m_k} \alpha_{i, j} x^j f_{k, i} \ge J$
Thus:
:$\order z = \order {g_J - \ds \sum_{j \mathop = J}^\infty \sum_{i \mathop = 1}^{m_k} \alpha_{i, j} x^j f_{k, i} }\ge J$
Hence:
:$\order z = \infty$
Then $z = 0$, which means:
:$g - \ds \sum_{i \mathop = 1}^{m_k} h_i f_{k, i} = 0$
Therefore:
:$g = \ds \sum_{i \mathop = 1}^{m_k} h_i f_{k, i}$
Therefore:
:$g \in F$
{{qed|lemma}}
Now, suppose $l < k$.
We induct on $k - l$.
The base case $k - l = 0$ is already done since we have $l \ge k$ here.
Suppose:
:$f \in I \implies f \in F$ whenever $k - \order f \le p$
and that:
:$k - l = p + 1$
We have:
:$[x^l] g \in S_l$
so there exist $\alpha_1, \ldots, \alpha_{m_l} \in A$ such that:
:$[x^l] g = \ds \sum_{i \mathop = 1}^{m_l} \alpha_i r_{l, i}$
Let:
:$h = g - \ds\sum_{i \mathop = 1}^{m_l} \alpha_i f_{l, i}$
Then:
:$\order h > \order g$
Also:
:$h \in I$
so $h \in F$ by the induction hypothesis.
Thus $g \in F$.
Thus $I = F$ and is finitely generated.
Since $I$ was arbitrary, we have $A \sqbrk x$ is Noetherian.
{{qed}}
Category:Noetherian Rings
Category:Formal Power Series
fq35vq0kic3hrodf31gxtpgbcm8oho9