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

regular local graded surjection has zero kernel

Statement

For the graded map ϕ:k[X1,,Xe]grmR defined by a cotangent basis in a nonzero Noetherian local ring, if e=dimR, then kerϕ=0.

Facts & Assumptions

Given: The objects and hypotheses in the statement. We work with the Axiom of Choice; cited dependent-choice and resolution-existence hypotheses are retained.

[F1]

associated graded polynomial surjection: Let (R,m,k) be nonzero Noetherian local and let x1,,xe lift a basis of m/m2. There is a surjective graded k-algebra map ϕ:k[X1,,Xe]grmR, determined by Xixi+m2, with every variable of degree one.

[F2]

The degree of the Hilbert-Samuel polynomial equals the dimension of the support: Assume the Axiom of Choice. Let (R,m) be a Noetherian local ring, let M0 be a finite R-module, and let I be an ideal of definition for M. Then the Hilbert-Samuel polynomial PI,M has degree degPI,M=dimSupp(M).

[F3]

A polynomial ring in finitely many indeterminates over an integral domain is an integral domain: If R is an integral domain, then R[x1,,xn] is an integral domain for every nN, including n=0.

Proof

1.1

If e=0, the map is the identity of k. Suppose e1. If the homogeneous kernel were nonzero, it would contain a nonzero homogeneous polynomial f of degree a1, because the degree-zero map is injective.

F1given
2.1

Put P=k[X1,,Xe]. Since P is a domain, multiplication by f injects P(a) into P. Counting monomials of total degree at most n, for na, gives j=0ndimk(P/(f))j=(n+ee)(na+ee). This polynomial has degree e1: the terms of degree e cancel.

F3step 1.1algebra
3.1

The surjection P/(f)grmR bounds R(R/mn+1) by that count, because its filtration factors are precisely the graded pieces. But its eventual Hilbert–Samuel polynomial has degree dimR=e and positive leading coefficient (it is eventually positive). A polynomial of degree e cannot be bounded by one of degree e1 for all large n. Thus no such f exists.

F2step 2.1algebra

Depends on

Used by

Dependency tree · two levels

16 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