TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-01

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 finite graded module over a standard graded algebra has rational Hilbert series and eventual polynomial growth

Statement

Let $A$ be an Artinian commutative ring, let

S = A [x_{1}, \dots, x_{r}] / J

be a standard graded $A$ -algebra with $\deg x_{i} = 1$ , and let $M = ⨁_{n \in Z} M_{n}$ be a finite graded $S$ -module. Then:

the Hilbert series ${HS}_{M} (t)$ is a rational function of the form ${HS}_{M} (t) = \frac{p (t)}{(1 - t)^{r}}$ for some Laurent polynomial $p (t) \in Z [t, t^{- 1}]$ ;
the Hilbert function $n \mapsto ℓ_{A} (M_{n})$ agrees for all sufficiently large $n$ with a polynomial in $n$ with rational coefficients.

Facts & Assumptions

Given: An Artinian ring $A$ , a standard graded $A$ -algebra $S = A [x_{1}, \dots, x_{r}] / J$ with $\deg x_{i} = 1$ , and a finite graded $S$ -module $M = ⨁ M_{n}$ .

[L1]

A twist satisfies $M (- 1)_{n} = M_{n - 1}$ , hence

{HS}_{M (- 1)} (t) = t {HS}_{M} (t)

(Nonnegatively graded rings and modules, homogeneous elements, and twists, The Hilbert function and formal Hilbert series of a graded module with finite-length pieces).

[L2]

Length is additive in short exact sequences of finite-length modules (Module length is additive in short exact sequences).

Proof

technique · direct

1.1

If $r = 0$ , then $S = A$ and the finite graded $A$ -module $M$ has only finitely many nonzero homogeneous pieces. Hence ${HS}_{M} (t)$ is a Laurent polynomial, so both conclusions hold.

givenalgebra

1.2

Assume $r > 0$ and write $S^{'} = A [x_{1}, \dots, x_{r - 1}] / (J \cap A [x_{1}, \dots, x_{r - 1}])$ . Multiplication by the degree-one class of $x_{r}$ gives an exact sequence of graded $S$ -modules $0 \to K \to M (- 1) \overset{x_{r}}{\to} M \to C \to 0,$ where $K$ and $C$ are annihilated by $x_{r}$ and therefore are finite graded $S^{'}$ -modules.

givenconstruct

1.3

Taking degree- $n$ pieces in algebra and using [L2] yields $ℓ_{A} (C_{n}) - ℓ_{A} (K_{n}) = ℓ_{A} (M_{n}) - ℓ_{A} (M_{n - 1})$ for every $n$ . In Hilbert-series form this is $(1 - t) {HS}_{M} (t) = {HS}_{C} (t) - {HS}_{K} (t)$ by [L1].

L1L2algebra

1.4

By the algebra hypothesis applied to the finite graded $S^{'}$ -modules $K$ and $C$ , the two series on the right side of algebra have denominator dividing $(1 - t)^{r - 1}$ . Therefore ${HS}_{M} (t)$ has denominator dividing $(1 - t)^{r}$ .

algebra

1.5

Any rational function with denominator a power of $(1 - t)$ expands for large $n$ as a finite $Z$ -linear combination of binomial coefficients $(\binom{n + d}{d})$ , hence its coefficients agree eventually with a polynomial. Applying this to algebra proves the eventual polynomial behaviour of $H_{M} (n) = ℓ_{A} (M_{n})$ .

algebra

2.1

Steps 1.1 through 1.5 prove both claims.

algebra∎

Depends on

Used by

Dependency tree · two levels

6 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 (standard reference, not scraped)
Allen B. Altman and Steven L. Kleiman, A Term of Commutative Algebra, Corollary (20.8) (standard reference, not scraped)