[Math] Can we prove that the ring of formal power series over a noetherian ring is noetherian without axiom of choice

ac.commutative-algebraaxiom-of-choice

Let $A$ be a commutative ring with an identity.
Suppose that every non-empty set of ideals of $A$ has a maximal element.
Let $A[[x]]$ be the formal power series ring over $A$.
Can we prove that every non-empty set of ideals of $A[[x]]$ has a maximal element without Axiom of Choice?

Remark
The same question was asked in MSE.

Best Answer

I believe that the answer is yes.

Let $A$ be a commutative ring with $1$, such that any non-empty set of ideals has a maximal element. For each ideal $I\leq A[[x]]$, and each $n\in \mathbb{N}$, define $I^{(n)}$ to be the set

$$\{0\}\cup\{a\in A\ :\ a\text{ is the leading non-zero coefficient, in degree $n$, of some }f\in A[[x]]\}.$$

This is an ideal of $A$. Also define $I^{(\omega)}=\bigcup_{n\in \mathbb{N}}I^{(n)}$, which is also an ideal of $A$.

Now suppose $\{I_{\alpha}\}_{\alpha}$ is a set of ideals in $A[[x]]$. The set of ideals $\{I_{\alpha}^{(\omega)}\}_{\alpha}$ has a maximal element, say $I^{(\omega)}_{\beta}$. Further, it isn't hard to prove that the form of the noetherian hypothesis we are assuming implies finite generation of ideals (provable in ZF). Thus, we may fix a generating set $a_1,a_2,\ldots, a_k$ for $I^{(\omega)}_{\beta}$. This means that $I^{(\omega)}_{\beta}=I^{(n)}_{\beta}$ for some $n\in \mathbb{N}$, which we also fix. (For instance, we can take the integer $n$ to be the lowest degree where each of $a_1,a_2,\ldots, a_k$ occurs as a leading coefficient.)

Now, restrict the set of $\alpha$ to only those for which $I_{\alpha}^{(n)}=I_{\beta}^{(n)}$. (Note that if $I_{\alpha}^{(n)}\neq I_{\beta}^{(n)}$, then $I_{\alpha}$ does not contain $I_{\beta}$. So this restriction costs us nothing.) Next, we may as well also assume $\beta$ is chosen such that $I_{\beta}^{(n-1)}$ is a maximal element of $\{I_{\alpha}^{(n-1)}\}_{\alpha}$. We then may assume $I_{\beta}^{(n-2)}$ is maximal in $\{I_{\alpha}^{(n-2)}\}_{\alpha}$, after restricting $\alpha$ again. Recursively repeating this process (only finitely many times), the resulting $\beta$ is such that $I_{\beta}$ is maximal in $\{I_{\alpha}\}_{\alpha}$.