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.

A single cancellation step lowers the degree of a polynomial in an ideal once its leading coefficient lies in a realised stage

Statement

Let $R$ be a commutative ring, let $a$ be an ideal of $R [x]$ , let $n \in N$ , and let $a_{n}$ be the stage ideal 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$ . Suppose $m \in N$ and $g_{1}, \dots, g_{m} \in a$ are nonzero polynomials of degree $n$ whose leading coefficients $c_{j} = lc (g_{j})$ generate $a_{n}$ , so that $a_{n} = (c_{1}, \dots, c_{m})$ .

Let $f \in a$ be nonzero of degree $d$ with $d \geq n$ and $lc (f) \in a_{n}$ . Then there is a polynomial $h$ in the ideal of $R [x]$ generated by $g_{1}, \dots, g_{m}$ such that

$f - h = 0 or f - h \neq 0 and \deg (f - h) < d .$

At $d = 0$ the second alternative is impossible, so there $f = h$ . At $m = 0$ the hypothesis on $f$ cannot be met: $a_{n}$ is then the zero ideal while a leading coefficient is nonzero, so the statement is not vacuously producing a degree drop out of nothing.

Facts & Assumptions

Given: A commutative ring $R$ , an ideal $a$ of $R [x]$ , an index $n \in N$ , polynomials $g_{1}, \dots, g_{m} \in a$ nonzero of degree $n$ with leading coefficients $c_{1}, \dots, c_{m}$ generating $a_{n}$ , and a nonzero $f \in a$ of degree $d \geq n$ with $lc (f) \in a_{n}$ .

[L1]

$R [x]$ is the set of finitely supported functions $a ⁣ : N \to R$ , with $(a + b)_{i} = a_{i} + b_{i}$ and $(a b)_{i} = \sum_{j + k = i} a_{j} b_{k}$ ; $x$ is the sequence with coefficient $1_{R}$ at index $1$ and zero elsewhere (The polynomial ring over a commutative ring as finitely supported coefficient sequences with convolution).

[L2]

For $0 \neq f = \sum_{i} a_{i} x^{i} \in R [x]$ the degree is $\deg f = \max {i \in N : a_{i} \neq 0}$ and the leading coefficient is $lc (f) = a_{\deg f}$ ; the zero polynomial has no degree and no leading coefficient (Degree, leading coefficient and monic polynomial, with the zero polynomial having no degree).

[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]

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$ ).

Proof

technique · direct

1.1

Fix the data of the Given line and write $c = lc (f)$ , a nonzero element of $R$ lying in $a_{n}$ ; the exponent $d - n$ is a natural number because $d \geq n$ .

L1L2given

2.1

Since $a_{n}$ is the ideal generated by $c_{1}, \dots, c_{m}$ and $c$ lies in it, the finite-sum description gives $r_{1}, \dots, r_{m} \in R$ with $c = \sum_{j = 1}^{m} r_{j} c_{j}$ . Any one such list may be taken; the construction below uses no property of it beyond this equation.

L3L4step 1.1

3.1

Put $h : = \sum_{j = 1}^{m} r_{j} x^{d - n} g_{j}$ , which lies in the ideal of $R [x]$ generated by $g_{1}, \dots, g_{m}$ because each coefficient $r_{j} x^{d - n}$ is an element of $R [x]$ . By the convolution rule the coefficient of $x^{i}$ in $r_{j} x^{d - n} g_{j}$ is $r_{j}$ times the coefficient of $x^{i - (d - n)}$ in $g_{j}$ , read as $0$ when $i < d - n$ . For $i > d$ that index exceeds $n$ , so the coefficient vanishes; at $i = d$ that index is exactly $n$ , so the coefficient is $r_{j} c_{j}$ . Summing over $j$ , the polynomial $h$ has zero coefficients at every index above $d$ and coefficient $\sum_{j = 1}^{m} r_{j} c_{j} = c$ at index $d$ .

L1L2L3step 2.1

4.1

The polynomial $f - h$ lies in $a$ and has zero coefficient at every index $i \geq d$ : above $d$ both $f$ and $h$ vanish, and at $d$ the two coefficients are $c$ and $c$ . So either $f - h = 0$ , or $f - h$ is nonzero and every index carrying a nonzero coefficient is below $d$ , which by the definition of degree means $\deg (f - h) < d$ .

L2step 3.1

5.1

Two extreme cases are worth recording. When $d = n$ the exponent $d - n$ is $0$ and $x^{0} = 1$ , so $h = \sum_{j} r_{j} g_{j}$ and no shift occurs. When $d = 0$ there is no natural number below $d$ , so the second alternative of step 4.1 cannot occur and the conclusion is the equality $f = h$ . When $m = 0$ the sum defining $a_{n}$ is empty, $a_{n} = 0$ , and no nonzero leading coefficient lies in it, so no $f$ satisfies the hypothesis.

L2L3step 3.1step 4.1∎

Remarks

Nothing is divided and no leading coefficient is inverted. The correction $h$ is built by multiplying the given $g_{j}$ by ring elements and a power of $x$ , so the argument runs over an arbitrary commutative ring rather than only over a field or a domain. That is exactly why the stage ideals are needed: over a field one generator per stage would do.
The $g_{j}$ must have degree exactly $n$ . If some $g_{j}$ had degree below $n$ the coefficient computation in step 3.1 would place $r_{j} c_{j}$ at an index below $d$ and the cancellation at $x^{d}$ would fail. This is what makes the exact-degree definition of the stage ideal the usable one.
The lemma produces one step, not a terminating procedure. Iterating it requires knowing that the leading coefficient of $f - h$ again lies in a realised stage, which is what the ascending chain condition supplies in the finite-generation lemma that uses this one.

Depends on

Used by

Dependency tree · two levels

10 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)