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.

Modulo a parameter preserves the top Hilbert-Samuel multiplicity up to the finite-annihilator correction

Statement

Assume the Axiom of Choice.

Let $(R, m)$ be a Noetherian local ring, let $M \neq 0$ be a finite $R$ -module, and put $d = \dim Supp (M)$ . Assume $d \geq 1$ and let $x, x_{2}, \dots, x_{d}$ be a system of parameters for $M$ . Put $Q = (x, x_{2}, \dots, x_{d})$ and $Q^{'} = (x_{2}, \dots, x_{d})$ . For a finite module $N$ on which $J$ is an ideal of definition, and for an integer $r \geq 0$ with either $N = 0$ or $r \geq \deg P_{J, N}$ , write $e_{J}^{[r]} (N) : = r! [n^{r}] P_{J, N} (n),$ with value $0$ when $N = 0$ or $\deg P_{J, N} < r$ . Then

e_{Q}^{[d]} (M) = e_{Q^{'}}^{[d - 1]} (M / x M) - e_{Q^{'}}^{[d - 1]} (0 :_{M} x) .

In particular, if $x$ is $M$ -regular, then

e_{Q} (M) = e_{Q^{'}} (M / x M) .

Facts & Assumptions

Given: The Axiom of Choice, a Noetherian local ring $(R, m)$ , a nonzero finite $R$ -module $M$ of support dimension $d \geq 1$ , and a system of parameters $x, x_{2}, \dots, x_{d}$ as above.

[L1]

The support dimension is the least number of generators of an ideal of definition (For a finite module, the dimension is the least size of an ideal of definition, and such tuples are systems of parameters).

[L2]

The degree of a nonzero finite module's Hilbert-Samuel polynomial equals its support dimension (The degree of the Hilbert-Samuel polynomial equals the dimension of the support).

[F1]

For an ideal of definition generated by $r$ elements, its dimension- $r$ multiplicity is the Euler characteristic of the corresponding Koszul complex (Stacks Project, Theorem 43.15.5).

[F2]

The Koszul complex on $(x, x_{2}, \dots, x_{d})$ is the tensor product of the two-term complex on $x$ with the Koszul complex on $Q^{'}$ . The two-term complex has homology $M / x M$ in degree $0$ and $(0 :_{M} x)$ in degree $1$ .

[F3]

For a finite module $T$ , the quotient $T / J T$ has finite length exactly when its support is contained in the closed point (Stacks Project, Remark 43.15.6).

Proof

technique · direct

1.1

Put $K = (0 :_{M} x)$ and $C = M / x M$ . Multiplication by $x$ gives the exact complex $0 \to K \to M \overset{x}{\to} M \to C \to 0.$ One has $C / Q^{'} C = M / Q M,$ so $Q^{'}$ is an ideal of definition for $C$ . Also $x K = 0$ , hence $Q^{'} K = Q K$ . Every prime in $Supp (K / Q^{'} K)$ lies in $Supp (M) \cap V (Q) = {m}$ , so [F3] makes $K / Q^{'} K$ finite length and $Q^{'}$ an ideal of definition for $K$ . By [L1], each nonzero one of $C$ and $K$ has support dimension at most $d - 1$ , and [L2] therefore gives $\deg P_{Q^{'}, C}, \deg P_{Q^{'}, K} \leq d - 1$ whenever the polynomial is nonzero.

L1L2F3givenalgebra

2.1

By [L2] and [F1], $e_{Q}^{[d]} (M)$ is the Euler characteristic of the Koszul complex on $(x, x_{2}, \dots, x_{d})$ . Using the tensor decomposition in [F2] and taking homology first in the two-term $x$ direction gives the $Q^{'}$ -Koszul complex on $C$ in homological degree $0$ and that on $K$ in degree $1$ . Euler characteristic is unchanged by this finite spectral sequence, so step 1.1 and [F1] give $e_{Q}^{[d]} (M) = e_{Q^{'}}^{[d - 1]} (C) - e_{Q^{'}}^{[d - 1]} (K) .$

L2F1F2step 1.1algebra

3.1

If $x$ is $M$ -regular, then $K = 0$ . By [L2], $\deg P_{Q, M} = d$ , so $e_{Q}^{[d]} (M) = e_{Q} (M) \neq 0$ . Step 2.1 therefore makes $e_{Q^{'}}^{[d - 1]} (C)$ nonzero. The degree bound in step 1.1 forces $\deg P_{Q^{'}, C} = d - 1$ , and hence $e_{Q^{'}}^{[d - 1]} (C) = e_{Q^{'}} (C)$ . This proves $e_{Q} (M) = e_{Q^{'}} (M / x M) .$

L2step 1.1step 2.1algebra

4.1

Therefore the parameter-reduction formula holds.

step 2.1step 3.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

11 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, Lemmas 10.60.13 and 10.60.14 (standard reference, not scraped)
Stacks Project, Theorem 43.15.5: multiplicity as Koszul Euler characteristic (standard reference, not scraped)
Allen B. Altman and Steven L. Kleiman, A Term of Commutative Algebra, §21 (standard reference, not scraped)