Coefficient ideals of a polynomial ideal (source code)

= Coefficient ideals of a polynomial ideal
{title2=$A_n(K)$}

For an <ideal> $K\subseteq R[t]$, let $A_n(K)$ consist of the coefficients at $t^n$ of elements of $K$ of <polynomial degree> at most $n$, including the zero <polynomial>. Each $A_n(K)$ is an <ideal> of $R$, and multiplication of representing <polynomials> by $t$ shows that $A_n(K)\subseteq A_{n+1}(K)$.

If $R$ is a <Noetherian ring>, this chain stabilizes at some $N$. Choose finite <generating sets of an ideal> for $A_0(K),\ldots,A_N(K)$, and for each nonzero generator choose a representing <polynomial> $f_{nj}\in K$ with that <leading coefficient> and <polynomial degree> $n$. These finitely many <polynomials> generate $K$: for any nonzero $f\in K$ of <polynomial degree> $d$, use the chosen generators at level $\min(d,N)$, multiplied by suitable powers of $t$, to cancel its <leading coefficient>. Induction on <polynomial degree> finishes the argument. This proves the <Hilbert basis theorem> without assuming that $R$ is an <integral domain>.