Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-31
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.

Local DVRs at the nonzero primes force dimension one

Statement

Assume the Axiom of Choice. Let R be a domain such that Rp is a discrete valuation ring for every nonzero prime ideal p of R. Then every nonzero prime ideal of R is maximal. Consequently, if R is not a field, then dimR=1.

Facts & Assumptions

Given: A domain R such that Rp is a discrete valuation ring for every nonzero prime ideal p.

[L1]

Localising at a prime ideal produces a local ring with maximal ideal pRp (Rp is local with unique maximal ideal pRp).

[L2]

Prime ideals of a localisation correspond exactly to primes of the original ring that avoid the denominator set (Prime ideals of a localization are exactly the primes disjoint from the denominator set).

[L3]

A discrete valuation ring has exactly two prime ideals, namely (0) and its maximal ideal, and hence has dimension 1 (Prime ideals and dimension of a DVR).

[L4]

Every proper ideal of a nonzero commutative ring is contained in a maximal ideal (In a nonzero commutative ring, every proper ideal is contained in a maximal ideal).

Proof

technique · direct
1.1

Let pq be prime ideals of R with p(0). By hypothesis, Rq is a discrete valuation ring. Because R is a domain, any nonzero element of p remains nonzero in Rq, so pRq is a nonzero prime ideal of Rq. Its contraction is p, so pRqqRq. This contradicts [L3], which allows only (0) and qRq as primes in a DVR. Therefore no nonzero prime ideal of R is properly contained in another prime ideal.

L1L2L3givenalgebra
2.1

Let p be a nonzero prime ideal of R. By [L4], choose a maximal ideal m containing p. Since p is nonzero, step 1.1 forbids a strict inclusion pm. Hence p=m, so every nonzero prime ideal of R is maximal.

L4step 1.1givenchoose
3.1

Assume now that R is not a field. Choose a nonzero nonunit xR. Then (x) is a proper ideal, so [L4] gives a maximal ideal m containing it. The ideal m is nonzero because it contains x, and step 2.1 shows that every nonzero prime ideal is maximal. Thus every strict prime chain has length at most 1, while (0)m has length 1. Hence dimR=1.

L4step 2.1givenchoose

Depends on

Used by

Dependency tree · two levels

20 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