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 of dimension one.
embedding dimension and regular local ring: Regularity means .
Determinant trick for Nakayama: If a finite module satisfies , some has . 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 , so is a unit: otherwise would force .
Equivalent characterizations of a DVR: Let be a nonfield domain. The following are equivalent. 1. is a discrete valuation ring. 2. is a Noetherian valuation ring. 3. is a one-dimensional Noetherian local integrally closed domain. 4. is a local principal ideal domain with nonzero maximal ideal.
The first clause of The Krull intersection is the -torsion submodule, and it vanishes in the Jacobson-radical case identifies with the elements annihilated by for some . By [F2], each such is a unit under the stated AC premise, so this intersection is .
Proof
Suppose is regular. Lift a basis of the one-dimensional vector space to . Then . The finite module satisfies , so [F2] gives and . Since , and is a nonzero nonunit. Also is not nilpotent: if , every prime contains and hence , making the only prime and forcing dimension zero.
By [F4], . Thus for every nonzero there is a largest with . Write . If then , a contradiction; therefore is a unit. Products of nonzero elements and are nonzero because is not nilpotent, so is a domain. In a nonzero ideal choose an element with least such exponent ; it generates the ideal. The zero ideal is principal too. Thus is a local PID with nonzero maximal ideal, hence a DVR by [F3].
Conversely, a DVR is a nonfield local PID of dimension one by [F3]. Its maximal ideal is nonzero, and by cancellation in a domain, so has basis the class of . Its embedding dimension is one, and it is regular by [F1].
Depends on
- The Axiom of Choice
- embedding dimension and regular local ring
- Determinant trick for Nakayama
- In a nonzero commutative ring, every proper ideal is contained in a maximal ideal
- Equivalent characterizations of a DVR
- The Krull intersection is the $(1-a)$-torsion submodule, and it vanishes in the Jacobson-radical case
Used by
- Regular centers have projective-bundle exceptional divisors Corollary
- regular local ring satisfies r one Corollary
- serre normality criterion two directions Corollary
- Finite normalization alone does not make a curve regular Counterexample
- Contact order of two regular components at a point Definition
- Delta invariant of a curve singularity Definition
- Uniformising parameters at smooth points of a plane curve Definition
- A divisor supported in a special fibre has positive conormal degree on some component Lemma
- A fixed-coordinate point-blowup chain defines a formal arc Lemma
- A normal-surface modification is an isomorphism in codimension one Lemma
- A point blowup drops pairwise intersection multiplicity by at least one Lemma
- A point blowup lowers pairwise contact order by one and separates transverse branches Lemma
- A root of the uniformizer kills the prime-to-residue-characteristic ramification required in specialization Lemma
- A triple-cubic surface branch reduces after two successors Lemma
- Blowing up a multiple point separates pairwise transverse components Lemma
- Blowing up a non-regular point strictly increases the finite normalization subalgebra Lemma
- Codimension-one components of a maximal-order support Lemma
- Fibres of a proper birational morphism of regular surfaces Lemma
- Intersection with a line is the order of vanishing of the restricted equation Lemma
- Multiplicity one characterises smooth points with a unique tangent Lemma
- Normalized point blowups dominate local normal surface modifications Lemma
- Point blowups of regular surfaces stay regular, with rational exceptional curves at two-dimensional local rings Lemma
- Positive conormal degree for a fibre divisor on a normal surface Lemma
- Projective modification of a proper integral DVR-scheme, unchanged in codimension one when regular Lemma
- Pushforward and vanishing for point blowups on a surface Lemma
- Rational maps from a smooth curve to a proper scheme are morphisms Lemma
- Strict henselization of a DVR and smooth sections Lemma
- Strictification Lemma
- The blowup of a one-dimensional integral Noetherian scheme at a closed point is finite Lemma
- The double-plus-simple cubic surface branch terminates Lemma
- The finite normalization of a curve factors through the blowup of a closed point Lemma
- The normalization defect is an Euler characteristic and a weighted sum of local lengths Lemma
- The order function of a one-dimensional Noetherian local domain Lemma
- A normal curve over a perfect field is nonsingular Theorem
- A normal variety is regular in codimension one Theorem
- Local rings at closed points of smooth curves are discrete valuation rings Theorem
- Normalization of a reduced curve is finite Theorem
- Regularization of a one-dimensional integral curve with finite normalization by point blowups Theorem
- serre normality criterion Theorem
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
- Example 12.10, p.116 (standard reference, not scraped)