Solution (source code)

= Solution

A <ring> is <Artinian> when its <ideals> satisfy the <descending chain condition>: every chain $I_1\supseteq I_2\supseteq\cdots$ eventually becomes constant. It is <Noetherian> when its <ideals> satisfy the <ascending chain condition>, equivalently when every <ideal> is finitely generated. We first prove <finite length of a commutative Artinian ring>; this gives the stronger structural reason for its <Noetherian> property.

If $\mathfrak p$ is a <prime ideal> of an <Artinian ring>, the quotient $R/\mathfrak p$ is an <Artinian> <integral domain>. For a nonzero element $x$ of that domain, the chain $(x)\supseteq(x^2)\supseteq\cdots$ stabilizes. Thus $x^n=bx^{n+1}$ for some $b$, and cancellation gives $bx=1$. The quotient is a <field>, so every <prime ideal> is a <maximal ideal>.

There are only finitely many <maximal ideals>. Otherwise, choose distinct ones $\mathfrak m_1,\mathfrak m_2,\ldots$. The intersections $\mathfrak m_1\cap\cdots\cap\mathfrak m_n$ form a strictly descending chain. To see strictness, for each $i\leq n$ choose $a_i\in\mathfrak m_i\setminus\mathfrak m_{n+1}$; their product belongs to the first $n$ <ideals> but not to the next one, since $\mathfrak m_{n+1}$ is prime. This contradicts the <descending chain condition>.

Put $J=\bigcap_i\mathfrak m_i$. This <Jacobson radical> is also the <nilradical>, since all primes are maximal. We need the stronger conclusion that \b[$J$ is nilpotent], without assuming <Noetherianity>. Its powers stabilize, say $K=J^n=J^{n+1}=JK$. Suppose $K\neq0$. By the <descending chain condition>, choose an <ideal> $L$ minimal subject to $KL\neq0$. Some $x\in L$ has $Kx\neq0$, so minimality gives $L=Rx$. Moreover $K(JL)=KL\neq0$, and minimality gives $JL=L$. Hence $x=jx$ for some $j\in J$. But $1-j$ is a unit: it cannot lie in any <maximal ideal>, because $j$ lies in all of them. Thus $x=0$, a contradiction. Therefore $J^n=0$.

The <Chinese remainder theorem> gives $R/J\cong\prod_iR/\mathfrak m_i$, a finite product of <fields>. Each quotient $J^i/J^{i+1}$ is an <Artinian module> over this product, and each <field> component must be a finite-dimensional <vector space>; an infinite-dimensional <vector space> admits a strictly descending chain of subspaces. Consequently every layer has finite <composition length>. The finite filtration
$$
R\supset J\supset\cdots\supset J^n=0
$$
shows that $R$ itself has finite <composition length>. A strict inclusion of submodules strictly increases length, so an ascending chain cannot continue indefinitely. \b[Every commutative <Artinian ring> is therefore <Noetherian>.] This is the <Artinian rings are Noetherian> result.

For the <formal power series ring>, let $B=R[[X]]$ with $R$ <Noetherian>, and let $H$ be any <ideal> of $B$. For $n\geq0$ define a coefficient <ideal>
$$
A_n=\{a\in R:\text{some }f\in H\cap X^nB\text{ has coefficient }a\text{ at }X^n\}.
$$
These <coefficient ideals of a formal power series ideal> satisfy $A_n\subseteq A_{n+1}$, by multiplication by $X$. The <ascending chain condition> gives $A_n=A_N$ for all $n\geq N$. For each $0\leq n\leq N$, choose finitely many series $f_{n,j}\in H\cap X^nB$ whose coefficients at $X^n$ generate $A_n$.

We claim that these finitely many series generate $H$ as an ordinary <ideal>. Given $f\in H$, cancel its coefficient at $X^k$ successively. After coefficients below $k$ have vanished, its coefficient at $X^k$ lies in $A_k$. If $k\leq N$, use an $R$-linear combination of the $f_{k,j}$. If $k>N$, use a combination of $X^{k-N}f_{N,j}$, since $A_k=A_N$. The remainder then belongs to $H\cap X^{k+1}B$.

Collect all the cancellations against each fixed generator. For $n<N$ its multiplier is a polynomial, while the multipliers of the $f_{N,j}$ are well-defined <formal power series>: at any fixed degree, only finitely many cancellation steps contribute. The remainder has every coefficient zero. Thus
$$
f=\sum_{n=0}^{N}\sum_j g_{n,j}(X)f_{n,j},\qquad g_{n,j}(X)\in R[[X]].
$$
This is a finite sum of <ideal> generators, rather than merely a topological closure assertion. Since $H$ was arbitrary,
$$
\boxed{R\text{ Noetherian}\ \Longrightarrow\ R[[X]]\text{ Noetherian}.}
$$
This coefficient-cancellation argument proves <Noetherianity of a formal power series ring>.

The corresponding <Artinian> assertion is \b[false]. For any nonzero <ring> $R$, the <ideals>
$$
(X)\supsetneq(X^2)\supsetneq(X^3)\supsetneq\cdots
$$
in $R[[X]]$ are strictly decreasing, since $X^n$ has a nonzero coefficient in degree $n$ and no multiple of $X^{n+1}$ does. In particular, a <field> $k$ is <Artinian>, but $k[[X]]$ is not. The zero <ring> is the harmless exception.