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 be a Noetherian integrally closed domain, and let be a prime ideal of height . Then the localisation is a discrete valuation ring.
Facts & Assumptions
Given: A Noetherian integrally closed domain and a height-one prime ideal .
The height of is (The height of a prime ideal).
Localisation at a prime means inverting (Localisation at a prime ideal: ).
The ring is local with maximal ideal ( is local with unique maximal ideal ).
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).
Localisations of Noetherian rings are Noetherian (Every quotient and every localisation of a Noetherian ring is Noetherian).
A nonfield domain is a DVR exactly when it is a one-dimensional Noetherian local integrally closed domain (Equivalent characterizations of a DVR).
Proof
By [L1] and [L3], the ring is a Noetherian local domain. By [F1], its Krull dimension is .
The localisation remains integrally closed. Let lie in the fraction field of and be integral over . Write a monic equation with each . Put . Then is integral over , so [F3] gives . Since , we conclude . Thus is integrally closed.
The maximal ideal of is nonzero. Choose . If in , then some satisfies , impossible in the domain . Hence is nonzero, so is not a field.
Steps 1.1, 1.2, and 1.3 verify condition 3 of [L4] for the ring . Therefore is a discrete valuation ring.
Depends on
- The height of a prime ideal
- Localisation at a prime ideal: $R_{\mathfrak p}=(R\setminus\mathfrak p)^{-1}R$
- $R_{\mathfrak p}$ is local with unique maximal ideal $\mathfrak pR_{\mathfrak p}$
- Prime ideals of a localization are exactly the primes disjoint from the denominator set
- Integral closure in an extension ring and integrally closed domains
- Left and right Noetherian rings
- Equivalent characterizations of a DVR
- Every quotient and every localisation of a Noetherian ring is Noetherian
Used by
- K-morphisms from smooth models into abelian schemes extend uniquely Corollary
- The degree of a divisor descends to the Picard group of a normal proper curve Corollary
- Order codimension one rational function Definition
- Pulling a divisor back along the cusp normalization Example
- Under AC, effective divisors on normal proper curves give finite subschemes of the same degree Example
- A connected special étale cover stays connected on the geometric generic fibre Lemma
- A divisorial valuation restricts to a divisorial valuation or the trivial valuation Lemma
- A nonsingular formal arc on a normal Noetherian surface becomes regular Lemma
- A normal Noetherian domain is the intersection of its height-one localizations Lemma
- A rational map from a normal variety to a proper variety extends in codimension one Lemma
- A root of the uniformizer kills the prime-to-residue-characteristic ramification required in specialization Lemma
- A square-conic blowup has cubic-controlled singular successors Lemma
- Degree-p differential trace extends across normal surface valuations Lemma
- Fibre degree of the finite locally free map to the projective line Lemma
- Localizing a Dedekind domain at a nonzero prime gives a DVR Lemma
- normal domain implies r one Lemma
- Proper normal curve rational function map Lemma
- Reduced Cartier multiples on a normal local surface Lemma
- Tame symbol reciprocity in dimension two (the Key Lemma) Lemma
- The dominant Borel-Weil section extends from the big cell Lemma
- The Picard group and intersection form of a product of projective lines Lemma
- The Picard group of a point blowup of the projective plane Lemma
- The smooth locus of a normal completion of a group has only constant functions Lemma
- A normal variety is regular in codimension one Theorem
- Normalization of a reduced curve is finite Theorem
- Principal divisors on a normal proper curve have degree zero Theorem
- Rosenlicht dichotomy for smooth connected algebraic groups Theorem
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
- Allen B. Altman and Steven L. Kleiman, A Term of Commutative Algebra, 13th ed., Theorem (23.10) (standard reference, not scraped)
- J. S. Milne, A Primer of Commutative Algebra, v4.03, Proposition 20.5 and Corollary 20.6 (standard reference, not scraped)