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.
The module-relative Hilbert–Samuel polynomial exists without a dimension theorem
Statement
Let be a commutative Noetherian local ring, a finitely generated -module, and an ideal such that . For every integer , has finite length. There is a unique with for all sufficiently large integers . If or , then . No degree/dimension assertion is part of this lemma.
Facts & Assumptions
Given: A commutative Noetherian local ring , a finite module , and an ideal with .
Associated graded pieces and their multiplication are defined in The associated graded ring and associated graded module of an ideal-adic filtration.
Length counts simple factors, including length zero for the zero module: Composition series and length of a module.
Finite length passes to submodules and quotients and is additive in short exact sequences: Module length is additive in short exact sequences.
Polynomial extension preserves Noetherianity: Hilbert basis theorem: if is Noetherian then is Noetherian.
A finite module over a Noetherian ring is Noetherian (every submodule is finite): Finitely generated modules over a left Noetherian ring are Noetherian.
Quotients of Noetherian rings are Noetherian: Every quotient and every localisation of a Noetherian ring is Noetherian.
The local ring has unique maximal ideal and residue field : A local ring is a nonzero commutative ring with a unique maximal ideal.
Every ideal of a Noetherian ring is finitely generated, using only the choice-free equivalence of conditions 1 and 2 in 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.
Proof
If or , every quotient in the statement is zero, giving the polynomial zero. More generally put . If , then implies by repeated multiplication for every , so again all quotients are zero. Uniqueness in these cases follows from the polynomial argument at the end. Henceforth and .
For a simple -module and , ; the map taking to is onto and its kernel is maximal, since a nontrivial intermediate ideal would give a nontrivial submodule. Thus the kernel is and . A composition series therefore satisfies . Iteration gives .
Set , a Noetherian ring. Each for is generated by finitely many elements and killed by , hence is a finite-dimensional -space. Indeed a finite spanning list can be reduced, by deleting any member in the span of the others, to a basis; the flag of initial basis spans has simple factors . Its -length is its dimension. Applying length additivity to the finite -adic filtration gives .
Choose generators of . For each , multiplication by the finitely many monomials with gives a surjection from copies of onto : coefficients modulo suffice because . In particular every has finite length and is killed by . The actions commute, and define as a finite graded module over , generated by a finite generating list of in degree zero.
For any finite graded -module , replacing a finite generating list by all its homogeneous components gives homogeneous generators. Their degrees have a lower bound. Each is a quotient of finitely many copies of , indexed by monomials of the required degree times these generators. Thus is a well-defined formal Laurent series. When , only the finitely many generator degrees can occur, so is a Laurent polynomial.
Suppose and rationality with denominator has been proved for every finite graded module over . Put , and . Iterating polynomial extension from the Noetherian ring makes Noetherian. Consequently is finite as a submodule of finite ; is finite as a quotient. Both are killed by , so their same finite generators generate them over the ring with variables.
In degree , the exact sequence , split at its image, yields . Hence . The induction hypothesis gives a Laurent polynomial numerator divided by . Together with the base case this proves that form for all .
The filtration of has successive factors , so its length is . Its generating series is for a Laurent polynomial . The geometric series and repeated convolution give the coefficient of in when . One can count the convolution terms as nonnegative -tuples with sum , separated by dividers. Thus for beyond the finite set of exponents of , , a rational polynomial in . For the binomial is , as required for .
If two rational polynomials eventually equal , their difference vanishes at infinitely many distinct integers. Division by at a root lowers the degree by one, so a nonzero polynomial of degree has at most distinct roots. The difference is therefore zero. This also proves the uniqueness left open in the zero cases.
Remarks
Source locators: Stacks Project, Section 10.58, Lemmas 10.58.5–6 and Proposition 10.58.7; Section 10.59, opening Hilbert functions and Proposition 10.59.5. The proof gives its own kernel/cokernel induction and extends the proper ring-ideal convention to module-relative finite colength. Only choice-free clauses of the Noetherian interfaces are used.
Depends on
- The associated graded ring and associated graded module of an ideal-adic filtration
- Composition series and length of a module
- Module length is additive in short exact sequences
- Hilbert basis theorem: if $R$ is Noetherian then $R[x]$ is Noetherian
- Finitely generated modules over a left Noetherian ring are Noetherian
- Every quotient and every localisation of a Noetherian ring is Noetherian
- A local ring is a nonzero commutative ring with a unique maximal ideal
- 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
Used by
Dependency tree · two levels
39 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
- Stacks Project, Proposition 10.58.7 and its finite-difference induction (standard reference, not scraped)
- Stacks Project, Proposition 10.59.5 (associated graded reduction) (standard reference, not scraped)