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 \dots$

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 = ⋃_{m = 0}^{n} T_{m}$ .

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

Proof that the construction works

Fill this in later