Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedverified 2026-09-24 (gpt-6-sol)
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.

associated graded polynomial surjection

Statement

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]→gr⁡mR, determined by Xi↦xi+m2, with every variable of degree one.

Facts & Assumptions

Given: The objects and hypotheses in the statement.

[F2]

The associated graded ring and associated graded module of an ideal-adic filtration: Let R be a commutative ring, let I⊂R be an ideal, and let M be an R-module. The associated graded ring of the I-adic filtration is gr⁡I(R):=⨁n≥0In/In+1. Multiplication is induced by multiplication in R: (a+Im+1)(b+In+1)=ab+Im+n+1. The associated graded module is gr⁡I(M):=⨁n≥0InM/In+1M, viewed as a graded gr⁡I(R)-module by (a+Im+1)(x+In+1M)=ax+Im+n+1M.

Proof

1.1F2givenalgebra

The degree-zero part is R/m=k. On mn/mn+1 the action of R factors through k, since mmn⊆mn+1. The graded multiplication therefore defines the displayed polynomial map. Altering a representative by mn+1 changes a product of degrees n,j by mn+j+1, so multiplication and the map are well-defined.

2.1step 1.1givenalgebra∎

For n≥1, every element of mn/mn+1 is a sum of classes of products u1⋯un with each uj∈m. In m/m2, express the class of each uj as a k-linear combination of the given basis classes xi+m2. Replacing one factor uj by such a combination changes the product only by an element of mn+1. Expanding therefore expresses every degree-n class as a k-linear combination of monomials in the xi+m2, all in the image of ϕ. Degree zero is k by step 1.1. This argument also covers e=0: the empty degree-one basis makes every positive-degree quotient zero, so the map k→gr⁡mR is surjective.

Depends on

Used by

Dependency tree · two levels

2 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