Image under leading coefficient map is Noetherian implies finitely generated

Statement

Suppose $R$ is a commutative unital ring, and $I$ is an ideal in the polynomial ring $R[x]$. Let $l:R[x]\to R$ be the leading coefficient map. Suppose $l(I)$ is a Noetherian ideal. Then $I$ is also a finitely generated ideal.

Proof

Construction of a generating set

Let $l_{n}(I)$ be the subset of $l(I)$ comprising those elements of $R$ that occur as leading coefficients of polynomials of degree $n$. Then $l_{n}(I)$ is an ideal, and further:

$l_{0}(I)\leq l_{1}(I)\leq l_{2}(I)\leq \ldots$

And the ascending union is $l(I)$.

Since $l(I)$ is finitely generated, there exists a $n$ such that $l_{n}(I)=l(I)$ (to see this, take a generating set for $l(I)$, and consider a $n$ such that $l_{n}(I)$ contains all the generators. Now construct a subset of $I$ as follows:

• For each $0\leq m\leq n$, consider $l_{m}(I)$. This is a submodule of the Noetherian module $l(I)$, hence it is finitely generated. Pick a finite generating set for $l_{m}(I)$, and for each member of this generating set, pick a representative polynomial of degree $m$. Call the set of such representative polynomials $T_{m}$.
• Let $T=\bigcup _{m=0}^{n}T_{m}$.

Then $T$ is a generating set for $I$.

Proof that the construction works

Fill this in later