LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Over a Noetherian ring, an ideal of $R [x]$ is generated by finitely many polynomials realising generators of its stages up to the stabilisation degree

Statement

Let $R$ be a Noetherian commutative ring and let $a$ be an ideal of $R [x]$ . Let $a_{0} \subseteq a_{1} \subseteq \dots$ be the stage ideals of The leading coefficients of the degree- $n$ elements of an ideal of $R [x]$ , together with $0$ , form an ideal of $R$ , and these ideals ascend with $n$ and let $N \in N$ be an index at which that chain stabilises, so $a_{n} = a_{N}$ for every $n \geq N$ . For each $n \leq N$ choose finitely many nonzero elements $c_{n, 1}, \dots, c_{n, m_{n}}$ of $a_{n}$ generating it, and for each of them a polynomial $g_{n, j} \in a$ , nonzero of degree $n$ , with $lc (g_{n, j}) = c_{n, j}$ .

Then the finitely many polynomials $g_{n, j}$ , for $n \leq N$ and $1 \leq j \leq m_{n}$ , generate $a$ as an ideal of $R [x]$ . In particular every ideal of $R [x]$ is finitely generated.

The selections are possible: each $a_{n}$ is an ideal of the Noetherian ring $R$ , hence has a finite generating set, from which the zero element may be discarded without loss, and every nonzero element of $a_{n}$ is by definition the leading coefficient of some nonzero degree- $n$ element of $a$ . Only finitely many selections are made, so no choice axiom is used.

Facts & Assumptions

Given: A Noetherian commutative ring $R$ , an ideal $a$ of $R [x]$ , and the stage ideals $a_{n}$ for $n \in N$ .

[L1]

For a commutative ring, being Noetherian is equivalent to every ideal being finitely generated, and to every ascending chain of ideals indexed by $N$ stabilising (A commutative ring is Noetherian exactly when every ideal is finitely generated, exactly when its ideals satisfy the ascending chain condition, and exactly when every nonempty set of ideals has a maximal member).

[L2]

For an ideal $a$ of $R [x]$ and $n \in N$ , the set $a_{n}$ of leading coefficients of the nonzero degree- $n$ elements of $a$ , together with $0$ , is an ideal of $R$ , and $a_{n} \subseteq a_{n + 1}$ (The leading coefficients of the degree- $n$ elements of an ideal of $R [x]$ , together with $0$ , form an ideal of $R$ , and these ideals ascend with $n$ ).

[L3]

In a commutative ring, $(S)$ consists of finite sums $\sum r_{i} s_{i}$ , and $(a) = R a$ ; the empty sum is included and equals $0$ (In a commutative ring, $(S)$ consists of finite sums $\sum r_{i} s_{i}$ , and $(a) = R a$ ).

[L4]

With $a_{n} = (c_{1}, \dots, c_{m})$ realised at stage $n$ by $g_{1}, \dots, g_{m} \in a$ , every nonzero $f \in a$ of degree $d \geq n$ with $lc (f) \in a_{n}$ admits an $h$ in the ideal generated by $g_{1}, \dots, g_{m}$ with $f - h = 0$ or $\deg (f - h) < d$ (A single cancellation step lowers the degree of a polynomial in an ideal once its leading coefficient lies in a realised stage).

[L5]

For $0 \neq f \in R [x]$ the degree is the largest index carrying a nonzero coefficient and the leading coefficient is the coefficient there; the zero polynomial has no degree (Degree, leading coefficient and monic polynomial, with the zero polynomial having no degree).

[L6]

Every nonempty subset $S \subseteq N$ has a least element: there is $ℓ \in S$ with $ℓ \leq s$ for all $s \in S$ (The well-ordering principle).

Proof

technique · contradiction

1.1

The stage ideals form an ascending chain of ideals of $R$ indexed by $N$ , and $R$ is Noetherian, so that chain stabilises: fix $N \in N$ with $a_{n} = a_{N}$ for every $n \geq N$ .

L1L2given

2.1

For each $n \leq N$ the ideal $a_{n}$ of $R$ is finitely generated; discard the zero element from a finite generating set, which changes nothing it generates, and realise each remaining generator $c_{n, j}$ by a nonzero $g_{n, j} \in a$ of degree $n$ . This is a selection over the finitely many pairs $(n, j)$ with $n \leq N$ , so it is a finite selection. Let $b$ be the ideal of $R [x]$ generated by all the $g_{n, j}$ ; since every $g_{n, j}$ lies in $a$ , we have $b \subseteq a$ .

L1L2L3step 1.1

3.1

Suppose $b \neq a$ , so that $a ∖ b$ is nonempty. The zero polynomial lies in $b$ , so every element of $a ∖ b$ is nonzero and therefore has a degree; the set of those degrees is a nonempty subset of $N$ and so has a least element $d$ . Fix $f \in a ∖ b$ with $\deg f = d$ .

assume-contraL3L5L6step 2.1

4.1

Put $n = \min (d, N)$ , so $n \leq N$ and $d \geq n$ . If $d \leq N$ then $n = d$ and $lc (f)$ lies in $a_{d} = a_{n}$ by the definition of the stage; if $d > N$ then $n = N$ and $lc (f) \in a_{d} = a_{N} = a_{n}$ by the stabilisation of step 1.1. The polynomials $g_{n, 1}, \dots, g_{n, m_{n}}$ realise generators of $a_{n}$ at stage $n$ , so the cancellation lemma applies and yields $h$ in the ideal generated by them, hence $h \in b$ , with $f - h = 0$ or $\deg (f - h) < d$ .

L2L4L5step 2.1step 3.1

5.1

Both alternatives are impossible. If $f - h = 0$ then $f = h \in b$ , contradicting $f \in a ∖ b$ . If $f - h \neq 0$ with $\deg (f - h) < d$ , then $f - h$ lies in $a$ and not in $b$ , since $h \in b$ and $f \notin b$ , so its degree belongs to the set whose least element is $d$ , contradicting $\deg (f - h) < d$ . Therefore $a = b$ , and $a$ is generated by the finitely many $g_{n, j}$ .

step 3.1step 4.1discharge-contradiction∎

Remarks

The generating list is not canonical. It depends on the stabilisation index $N$ , on the finite generating sets chosen for the stages, and on the realisers; a larger $N$ or a larger generating set produces a longer list that generates the same ideal. Nothing above claims minimality.
Where the Noetherian hypothesis is used, and where it is not. It is used twice, in step 1.1 for the stabilisation of the chain and in step 2.1 for finite generation of each stage. The leading coefficients of the degree- $n$ elements of an ideal of $R [x]$ , together with $0$ , form an ideal of $R$ , and these ideals ascend with $n$ and A single cancellation step lowers the degree of a polynomial in an ideal once its leading coefficient lies in a realised stage hold over any commutative ring; only the passage from "one cancellation step" to "a finite generating list" needs the chain condition.
The minimal-degree argument replaces an induction that would not terminate on its own. A single cancellation step lowers the degree, but iterating it from an arbitrary element gives no bound; choosing a counterexample of least degree turns one step into a contradiction.

Depends on

Used by

Dependency tree · two levels

26 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

M. Hochster, Introduction to Commutative Algebra, Math 614, Theorem 5.6 (standard reference, not scraped)
B. Totaro, Commutative Algebra (Michaelmas 2011), notes by Z. Norwood, §8 Theorem 8.3 (standard reference, not scraped)

Over a Noetherian ring, an ideal of R[x]R[x] is generated by finitely many polynomials realising generators of its stages up to the stabilisation degree