Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedverified 2026-09-26 (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.

one dimensional regular local rings are dvrs

Statement

Assume the Axiom of Choice (The Axiom of Choice). A nonzero Noetherian local ring of dimension one is regular if and only if it is a discrete valuation ring. Fields are excluded from the term DVR.

Facts & Assumptions

Given: The Axiom of Choice and a nonzero Noetherian local ring (R,m,k) of dimension one.

[F1]

embedding dimension and regular local ring: Regularity means dim⁡k(m/m2)=dim⁡R=1.

[F2]

Determinant trick for Nakayama: If a finite module M satisfies mM=M, some a∈m has (1−a)M=0. Under AC, In a nonzero commutative ring, every proper ideal is contained in a maximal ideal shows that every nonunit lies in a maximal ideal. In this local ring it must lie in m, so 1−a is a unit: otherwise 1−a,a∈m would force 1∈m.

[F3]

Equivalent characterizations of a DVR: Let R be a nonfield domain. The following are equivalent. 1. R is a discrete valuation ring. 2. R is a Noetherian valuation ring. 3. R is a one-dimensional Noetherian local integrally closed domain. 4. R is a local principal ideal domain with nonzero maximal ideal.

[F4]

The first clause of The Krull intersection is the (1−a)-torsion submodule, and it vanishes in the Jacobson-radical case identifies ⋂n≥0mn with the elements annihilated by 1−a for some a∈m. By [F2], each such 1−a is a unit under the stated AC premise, so this intersection is 0.

Proof

1.1F1F2given

Suppose R is regular. Lift a basis of the one-dimensional vector space m/m2 to t∈m. Then m=(t)+m2. The finite module Q=m/(t) satisfies mQ=Q, so [F2] gives Q=0 and m=(t). Since dim⁡R=1, m≠0 and t is a nonzero nonunit. Also t is not nilpotent: if tr=0, every prime contains t and hence m, making m the only prime and forcing dimension zero.

2.1step 1.1F3F4algebra

By [F4], ⋂n≥0(tn)=0. Thus for every nonzero a∈R there is a largest n with a∈(tn). Write a=tnu. If u∈m=(t) then a∈(tn+1), a contradiction; therefore u is a unit. Products of nonzero elements tnu and tmv are nonzero because t is not nilpotent, so R is a domain. In a nonzero ideal choose an element with least such exponent n; it generates the ideal. The zero ideal is principal too. Thus R is a local PID with nonzero maximal ideal, hence a DVR by [F3].

3.1F1F3algebra∎

Conversely, a DVR is a nonfield local PID of dimension one by [F3]. Its maximal ideal (t) is nonzero, and t∉(t2) by cancellation in a domain, so m/m2 has basis the class of t. Its embedding dimension is one, and it is regular by [F1].

Depends on

Used by

Dependency tree · two levels

33 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