Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 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.

Height-one localizations of normal Noetherian domains are DVRs

Statement

Let R be a Noetherian integrally closed domain, and let p be a prime ideal of height 1. Then the localisation Rp is a discrete valuation ring.

Facts & Assumptions

Given: A Noetherian integrally closed domain R and a height-one prime ideal p.

[F1]

The height of p is ht(p)=dim(Rp) (The height of a prime ideal).

[F2]

Localisation at a prime means inverting Rp (Localisation at a prime ideal: Rp=(Rp)1R).

[L1]

The ring Rp is local with maximal ideal pRp (Rp is local with unique maximal ideal pRp).

[F3]

A domain is integrally closed when every element of its fraction field integral over it already lies in the domain (Integral closure in an extension ring and integrally closed domains).

[L3]

Localisations of Noetherian rings are Noetherian (Every quotient and every localisation of a Noetherian ring is Noetherian).

[L4]

A nonfield domain is a DVR exactly when it is a one-dimensional Noetherian local integrally closed domain (Equivalent characterizations of a DVR).

Proof

technique · direct
1.1

By [L1] and [L3], the ring Rp is a Noetherian local domain. By [F1], its Krull dimension is dim(Rp)=ht(p)=1.

F1L1L3given
1.2

The localisation remains integrally closed. Let x lie in the fraction field of Rp and be integral over Rp. Write a monic equation xn+an1sn1xn1++a0s0=0 with each sip. Put s=s0sn1. Then sx is integral over R, so [F3] gives sxR. Since sp, we conclude x=(sx)/sRp. Thus Rp is integrally closed.

F2F3givenalgebra
1.3

The maximal ideal of Rp is nonzero. Choose 0ap. If a/1=0 in Rp, then some sp satisfies sa=0, impossible in the domain R. Hence a/1pRp is nonzero, so Rp is not a field.

L1givenalgebra
2.1

Steps 1.1, 1.2, and 1.3 verify condition 3 of [L4] for the ring Rp. Therefore Rp is a discrete valuation ring.

L4step 1.1step 1.2step 1.3

Depends on

Used by

Nothing in the library uses this result yet.

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