Alphabeta Math
LemmaStatement: 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.

The symbolic-power step inside the principal ideal theorem

Statement

Let (R,m) be a Noetherian local domain, and let xm be nonzero. If m is minimal over (x), then every prime ideal strictly contained in m is zero. In particular ht(m)1.

Facts & Assumptions

Given: A Noetherian local domain (R,m) and a nonzero element xm such that m is minimal over (x).

[L3]

The nilradical of a Noetherian ring is nilpotent (The nilradical of a Noetherian ring is nilpotent).

[L4]

Prime ideals of a localization correspond to primes disjoint from its denominator set (Prime ideals of a localization are exactly the primes disjoint from the denominator set).

[L5]

If IM=M for a finitely generated module, then (1a)M=0 for some aI (Determinant trick for Nakayama).

[L6]

In a local ring, every element outside the unique maximal ideal is a unit; in particular 1a is a unit for a in the maximal ideal (Assuming the Axiom of Choice, a nonzero commutative ring is local exactly when its nonunits form an ideal, exactly when one of x and 1x is a unit for every x).

Proof

technique · direct
1.1

Since m is both maximal and minimal among primes containing (x), it is the only such prime. Hence the quotient R=R/(x) is Noetherian by [L2] and has the single prime m. Its nilradical is therefore m, so [L3] gives mN=0 for some N. Each layer mj/mj+1 is a finite-dimensional vector space over R/m: it is finitely generated by [L2] and is annihilated by m. A descending chain of ideals in R induces descending chains in these finitely many finite-dimensional layers, so all layers, and therefore the original chain, stabilize. Thus R is Artinian.

L2L3givenalgebra
2.1

Let pm be prime. Then xp. For r1, define the symbolic power p(r):=prRpR. These form a descending chain. By step 1.1, the ideals (p(r)+(x))/(x) in R stabilize, so for some r, p(r)+(x)=p(r+1)+(x). If ap(r), write a=b+xc with bp(r+1). In Rp the element x is a unit, while abprRp; hence cprRpR=p(r). Therefore p(r)=p(r+1)+xp(r).

L4step 1.1givenconstructalgebra
3.1

The quotient module M=p(r)/p(r+1) is finitely generated by [L2], and step 2.1 says M=xM. Apply [L5] with I=(x). It gives (1a)M=0 for some a(x)m. Fact [L6] makes 1a a unit, so M=0 and p(r)=p(r+1). Localizing this equality at p gives (pRp)r=(pRp)r+1.

L2L5L6step 2.1algebra
4.1

Apply [L5] in the local ring Rp to the finite module (pRp)r and the ideal pRp. Step 3.1 says that ideal times the module is the module, so [L6] gives (pRp)r=0. Because Rp is a domain, this forces pRp=0, and contraction through [L4] gives p=(0). Thus every prime strictly below m is zero, and [L1] yields ht(m)1.

L1L4L5L6step 3.1algebra

Depends on

Used by

Dependency tree · two levels

35 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