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.

depth two excludes finite punctured extension

Statement

Let (R,m) be reduced Noetherian local with depthR2. If RBQ(R) is a finite intermediate ring and SuppR(B/R){m}, then B=R.

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]

total ring of fractions: For a nonzero commutative ring R, let S be the set of its nonzerodivisors, meaning elements whose multiplication maps on R are injective. Its total ring of fractions is Q(R)=S1R. The set S is multiplicative since composites of injective multiplication maps are injective. The natural map RQ(R) is injective: a/1=0 implies sa=0 for some sS, hence a=0. Set Q(0)=0. For a domain this recovers the fraction field; for a ring with zero divisors it need not be a field.

[F2]

The three Depth Lemma inequalities: Let (R,m) be a Noetherian local ring and 0ABC0 a short exact sequence of finite R-modules. With a=depthR(A), b=depthR(B), and c=depthR(C), bmin{a,c},amin{b,c+1},cmin{a1,b}. The last inequality is vacuous when a=0.

[F3]

The local depth-zero associated-prime criterion: Let (R,m) be a Noetherian local ring and let M0 be a finite R-module. Then depth(M)=0mAssR(M).

[F4]

For a finite module, support is the set of primes containing the annihilator: If M is a finitely generated left R-module, then SuppR(M)={p:AnnR(M)p}.

[F5]

Assuming the Axiom of Choice, Nakayama's lemma: Assume the Axiom of Choice. Let R be a commutative ring, let IR satisfy IJ(R), and let M be a finitely generated left R-module. If IM=M, then M=0.

Proof

1.1

Choose the first element xm of an R-regular sequence of length two. It is a unit in Q(R), so it acts injectively on B. Since B is nonzero finite and xm, Nakayama gives B/xB0, hence depthRB1. Applied to 0RBC0, the depth lemma gives depthCmin(depthR1,depthB)1 if C0.

F1F2F5
2.1

If C0 and its support is contained in the closed point, the support-annihilator theorem gives AnnC=m. Finitely many generators of m each have a power in the annihilator; expanding monomials gives mNC=0 for some N. A last nonzero power mjC contains a nonzero element killed by m, making m associated and depthC=0. This contradicts the preceding bound. Thus C=0 and B=R, including the case of empty support.

F4F3step 1.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