Finite-variable polynomial algebras over fields are Noetherian by finite generators

Every field $F$ is Noetherian. Let $I\subseteq F$ be an ideal of the commutative ring $F$; if $I$ contains some $a\mathrm{\ne }0$, then $1_F=a^{-1}a\in I$ by [L8] and [L4], so $I=F=(1_F)$; otherwise $I=\{0\}=(0_F)$, which is generated by the empty list. In both cases $I$ is finitely generated, so every submodule of the regular module ${}_{F}F$ is finitely generated by [L3], and [L1] and [L2] make $F$ Noetherian.

Let $C$ be a Noetherian commutative ring and let $I\subseteq C[x]$ be an ideal. Then $I$ is finitely generated. In this step, a polynomial is said to have support bounded by $n$ when all coefficients above index $n$ vanish; this includes the zero polynomial without assigning it a degree. For $n\in \mathbb{N}$ put $J_n:=\{a\in C:\text{the coefficient of }{x}^n\text{ in some }f\in I\text{ with support bounded by }n\text{ equals }a\}$, a nonempty set containing $0$. Each $J_n$ is an ideal of $C$: it is closed under addition because coefficients of $x^n$ add, and under multiplication by $r\in C$ because $rf\in I$ again has support bounded by $n$ with coefficient of $x^n$ equal to $ra$. By [L5] the coefficient of $x^{n+1}$ in $xf$ is the coefficient of $x^n$ in $f$, and $xf$ has support bounded by $n+1$ by [L5]; hence $J_n\subseteq J_{n+1}$. The union $J:={\bigcup }_n{J}_n$ is an ideal of $C$: for $a\in J_m$ and $b\in J_n$, both lie in $J_{\max (m,n)}$, which is an ideal, so $a+b\in J_{\max (m,n)}\subseteq J$; also $ra\in J_m\subseteq J$ for $r\in C$. Since $C$ is Noetherian, every ideal of $C$ is finitely generated by [L1], [L2] and [L3]; fix a finite generating list $J=(b_1,\dots ,b_r)$ as in [L4]. If $r=0$, then $J=0$, hence $I=0$ because the leading coefficient of any nonzero $f\in I$ would belong to $J_{\mathrm{deg}f}\subseteq J$; in this case the empty list generates $I$. Otherwise each $b_i$ lies in some $J_{N_i}$; put $N:={\max }_i{N}_i$, which exists because the list is finite and nonempty. Then $J_N$ is an ideal containing every $b_i$, so $J\subseteq J_N$ by [L4], and $J_N\subseteq J$ by definition of $J$; hence $J_n=J_N$ for every $n\ge N$. For each of the finitely many $n\le N$ the ideal $J_n$ has a finite generating list $J_n=(c_{n,1},\dots ,c_{n,s_n})$ by [L1], [L2] and [L3], and for each pair $(n,k)$ we choose $f_{n,k}\in I$ with support bounded by $n$ whose coefficient of $x^n$ is $c_{n,k}$, which exists by the definition of $J_n$ (take $f_{n,k}=0$ when $c_{n,k}=0$). We claim that the finite set $W:=\{f_{n,k}:0\le n\le N,1\le k\le s_n\}$ generates $I$; by [L4] this means $(W)=I$, and $(W)\subseteq I$ holds because $W\subseteq I$. The zero polynomial is already in $(W)$. Let $0\mathrm{\ne }f\in I$ have degree $d$, and put $n:=\min \{d,N\}$; the leading coefficient $\mathrm{lc}(f)$ is the coefficient of $x^d$ in $f$, so $\mathrm{lc}(f)\in J_d$ if $d\le N$ and $\mathrm{lc}(f)\in J_d=J_N$ if $d>N$, that is $\mathrm{lc}(f)\in J_n$ in both cases. By [L4] there are ${\mu }_1,\dots ,{\mu }_{s_n}\in C$ with $\mathrm{lc}(f)={\sum }_k{\mu }_k{c}_{n,k}$, and each $x^{d-n}{f}_{n,k}$ lies in $I$ and has support bounded by $d$ with coefficient of $x^d$ equal to $c_{n,k}$; therefore $g:=f-{\sum }_k{\mu }_k{x}^{d-n}{f}_{n,k}$ lies in $I$ and is either zero or has degree strictly smaller than $d$ by [L5] and [L6]. Induction on $d$, in the form of repeated descent of the degree, expresses every element of $I$ as a combination of elements of $W$ with coefficients in $C[x]$; hence $I=(W)$ is finitely generated.

We prove by induction on $d$ that $K[x_1,\dots ,x_d]$ is Noetherian. For $d=0$ the ring is $K$ by [L7], Noetherian by step 1.1. For the step, $K[x_1,\dots ,x_{d+1}]=K[x_1,\dots ,x_d][x_{d+1}]$ by [L7]; if $K[x_1,\dots ,x_d]$ is Noetherian, then every ideal of $K[x_1,\dots ,x_{d+1}]$ is finitely generated by step 1.2, so $K[x_1,\dots ,x_{d+1}]$ is Noetherian by [L1], [L2] and [L3].

Thus for every field $K$ and every $d\ge 0$ the ring $K[x_1,\dots ,x_d]$ is Noetherian, that is, each of its ideals has a finite generating list: by step 2.1 its regular module is Noetherian, and its ideals are exactly the submodules of that module by [L3]. Every selection made above was from a finite list — the generating lists of the finitely many ideals $J_n$ with $n\le N$, the finitely many witnesses $f_{n,k}$, and the finitely many indices $N_i$ — and the degree descent is an induction on $\mathbb{N}$, so no choice principle is used.