Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10
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.

degree-r Hilbert–Samuel coefficient as Koszul Euler characteristic

Statement

Assume AC. Let (R,m) be a commutative Noetherian local ring, M a finite R-module and I=(f1,…,fr) with ℓR(M/IM)<∞. Use P(n)=ℓR(M/In+1M) for all sufficiently large n. Then P=0 or deg⁡(P)≤r, and er(I,M)=r![Tr]P(T)=χ(K(f1,…,fr;M)). The degree-r coefficient may vanish. This includes M=0, I=R and r=0.

Facts & Assumptions

Given: AC, a commutative Noetherian local ring (R,m), a finite R-module M, and I=(f1,…,fr) with ℓR(M/IM)<∞.

[A1]
[F1]

Euler characteristic and every coefficient ej use the fixed n+1 convention: koszul euler characteristic and degree indexed multiplicity.

[F2]

All the Koszul homology modules here have finite length: koszul homology finite length for an ideal of definition.

[F3]

Euler characteristic equals the alternating sum of finite-length terms: bounded finite length complex euler identities.

[F4]

A sufficiently deep shifted-adic quotient has the homology of K and finite-length terms; for a unit ideal K is acyclic: shifted adic koszul filtration euler comparison.

[F5]

The module-relative eventual rational polynomial exists uniquely: The module-relative Hilbert–Samuel polynomial exists without a dimension theorem.

[F6]

Finite length is additive and passes to quotients: Module length is additive in short exact sequences.

Proof

technique · direct
1.1F1F4F5given

If M=0, both sides are zero. If I=R, the polynomial is zero and the Koszul complex is acyclic. If r=0, then I=0 and M has finite length; the complex is M[0], its Euler characteristic is ℓR(M) and P is that constant, so e0=ℓR(M). The remaining argument concerns r≥1 and a proper ideal.

1.2F6givenalgebra

Put c=ℓR(M/IM). For j≥0, degree-j monomials in the r generators give a surjection (M/IM)aj→IjM/Ij+1M, where aj is the number of tuples (α1,…,αr) of nonnegative integers summing to j. Encode a tuple by j marks with r−1 separators, including adjacent separators for zero entries. This is a bijection with choices of separator positions, giving aj=(j+r−1r−1). Consequently ℓR(IjM/Ij+1M)≤c(j+r−1r−1).

1.3A1F2F3F4F5

Choose p>r deep enough for the shifted-adic comparison and for P(p−i−1)=ℓR(M/Ip−iM) for every 0≤i≤r. This is possible since only finitely many inequalities are required. The term in cochain degree −i of K/FpK is (M/Ip−iM)(ri). Homology comparison and term cancellation therefore give χ(K)=∑i=0r(−1)i(ri)P(p−i−1). The AC hypothesis supplies that in the finite-length and tail lemmas.

1.4algebra

Define ΔQ(t)=Q(t)−Q(t−1). For k=0 the identity ΔkQ(t)=∑i=0k(−1)i(ki)Q(t−i) is the single term Q(t). If it holds at k, subtract its value at t−1 from its value at t. The coefficient of Q(t−i) becomes (−1)i((ki)+(ki−1))=(−1)i(k+1i), with out-of-range binomials zero; the two endpoint coefficients are 1 and (−1)k+1. This proves the identity for every k by induction.

2.1F6step 1.2

Summing along the I-adic filtration gives 0≤ℓR(M/In+1M)≤c∑j=0n(j+r−1r−1)=c(n+rr). For the last identity, tuples in r variables of total at most n correspond bijectively to tuples in r+1 variables of total exactly n, by adjoining the slack n−j; the same separator count applies. This holds for every n≥0.

3.1F5step 2.1algebra

The eventual polynomial is nonnegative at all sufficiently large integers. If it is nonzero, its leading coefficient is positive: division by its highest power of n makes the lower terms tend to zero, so the sign is eventually the leading sign. If its degree exceeded r, that same division would make the upper bound from the preceding step tend to zero while the polynomial tends to a positive leading coefficient. This is impossible. Hence P=0 or deg⁡(P)≤r.

4.1F1step 1.1step 3.1step 1.3step 1.4algebra∎

For d≥1, the binomial expansion gives td−(t−1)d=dtd−1 plus terms of degree at most d−2; a constant has difference zero. By linearity, r differences annihilate every monomial of degree less than r and take tr to r!. The degree bound thus gives ΔrP=r![Tr]P(T), including the zero polynomial. At t=p−1 the preceding finite-difference identity is precisely the Euler sum, so it equals er(I,M). Together with the initial cases this proves the theorem.

Remarks

Source locators: Stacks 43.15.4 (finite differences), Theorem 43.15.5 and Remark 43.15.6; Hochster printed pp.106–108. In the present convention the quotient by Ip−i contributes P(p−i−1), not P(p−i). The monomial count proves the degree bound independently of a dimension theorem. No parameter-reduction result is a premise.

Depends on

Used by

Dependency tree · two levels

27 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