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.

Equivalent characterizations of a DVR

Statement

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.

Facts & Assumptions

Given: A nonfield domain R with fraction field K.

[F1]

A local ring is a nonzero commutative ring with a unique maximal ideal (A local ring is a nonzero commutative ring with a unique maximal ideal).

[F3]

A principal ideal domain is an integral domain in which every ideal is principal (Principal ideal domain).

[F4]

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).

[L1]

Valuation rings are integrally closed (Valuation rings are integrally closed).

[L2]

In a valuation ring the ideals are linearly ordered, and every finitely generated ideal is principal (Characterizations of valuation rings).

[L3]

A valuation ring is local (A valuation ring is local).

[L4]

In a discrete valuation ring every nonzero ideal is a power of the maximal ideal (Ideals in a DVR are powers of the maximal ideal).

[L5]

A discrete valuation ring has exactly two prime ideals and dimension 1 (Prime ideals and dimension of a DVR).

[L6]

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

[L7]

The nilradical of a Noetherian ring is nilpotent (The nilradical of a Noetherian ring is nilpotent).

[L8]

For a positive-size square matrix A over a commutative ring, Aadj⁡(A)=det⁡(A)I (For every positive-sized square matrix over a commutative ring, Aadj⁡(A)=adj⁡(A)A=det⁡(A)I).

[F5]

Krull dimension is the supremum of the lengths of strict chains of prime ideals (Krull dimension of a nonzero ring).

Proof

technique · direct
1.1F2F3L1L3L4L5

Assume condition 1. Then [L3] makes R local. By [L4], every ideal of R is principal, so [F3] shows that R is a PID; in particular it is condition 4. Because every ideal is principal, [F2] makes R Noetherian, so condition 2 holds as well. By [L1] and [L5], R is integrally closed and one-dimensional, so condition 3 also holds.

1.2F2L2L3givenchoose

Assume condition 2. By [L3], the ring is local with maximal ideal m. Because R is not a field, m≠0. By [F2], every ideal of R is finitely generated, so choose generators a1,…,ar of m. By [L2], one of them divides all the others; rename it π. Then m=(π).

1.3F1F5L6L7givenchoose

Assume condition 3. Let m be the unique maximal ideal. It is nonzero because R is not a field. Choose 0≠x∈m. The quotient R/xR is Noetherian by [L6]. Every prime ideal of R containing xR is nonzero, hence equals m because dim⁡R=1. Therefore the nilradical of R/xR is m/xR, so [L7] yields an integer n≥1 with mn⊆xR.

1.4F1F2F3givenalgebra

Assume condition 4. Then the ring is local with nonzero maximal ideal m=(π). Because every ideal is principal, [F2] makes R Noetherian. Every element outside m is a unit: if x∉m, then (x) is not contained in the unique maximal ideal, so (x)=R. Hence every nonunit is a multiple of π.

2.1step 1.2step 1.4algebra

In the situations of steps 1.2 and 1.4, the ring is a Noetherian local domain with nonzero principal maximal ideal m=(π). Let 0≠x∈R. If x is not a unit, the maximal-ideal description gives x=πx1. If x1 is not a unit, write x1=πx2, and continue. This process stops, for otherwise (x)⊊(x1)⊊(x2)⊊⋯ would be a strict ascending chain of ideals, contradicting Noetherianity. Thus every nonzero element has the form uπn with u a unit and n≥0. If uπn=u′πm with units u,u′, then n=m, for otherwise a positive power of the nonunit π would equal a unit.

3.1step 1.2step 2.1givenchoosealgebra

In the same situations, every nonzero ideal I of R is (πn) for a unique integer n≥0: choose 0≠x∈I whose exponent in step 2.1 is minimal, say x=uπn. Then πn=u−1x∈I. For any nonzero y∈I, write y=u′πm by step 2.1; minimality gives m≥n, so y∈(πn). Hence I=(πn). Therefore step 1.2 already yields condition 4.

3.2step 1.4step 2.1algebra

Under condition 4, let x=a/b∈K× with a,b∈R∖{0}. By step 2.1, write a=uπm and b=vπn. Then x=(uv−1)πm−n. If m≥n, then x∈R; if m<n, then x−1∈R. Thus R is a valuation ring, and step 1.4 already makes it Noetherian. Therefore condition 2 holds.

4.1step 1.3step 3.1choosealgebra

Return to condition 3. Choose n≥1 minimal with mn⊆xR. If n=1, then m=(x), so steps 1.3 and 3.1 give condition 4. Suppose instead that n>1, and choose y∈mn−1∖xR. Then ym⊆mn⊆xR, so z:=y/x∈K satisfies zm⊆R while z∉R.

4.2step 2.1algebra

Under condition 4, define v:K→Z∪{∞} by v(0)=∞ and v(x)=m−n when x=(uv−1)πm−n as in step 3.2. The uniqueness part of step 2.1 makes this well defined. Multiplicativity is immediate from exponents. If v(x)≤v(y), write x=uπm and y=u′πn with m≤n; then x+y=πm(u+u′πn−m), and the bracket lies in R, so v(x+y)≥m=min⁡{v(x),v(y)}. Because v(π)=1, this valuation is surjective, and its nonnegative locus is exactly R. Therefore condition 1 holds.

5.1F2F4L8step 4.1givenchoosealgebra

Still under condition 3, suppose also that zm⊆m. Because R is Noetherian, [F2] lets us choose generators b1,…,br of m. Write zbj=∑i=1rcijbi with cij∈R. In matrix form this is (zIr−C)b=0. By [L8], det⁡(zIr−C)b=0. Choose an index j with bj≠0; since R is a domain, the equality det⁡(zIr−C)bj=0 forces det⁡(zIr−C)=0. This is a monic polynomial equation for z with coefficients in R, so z is integral over R. Because z∈K and condition 3 says R is integrally closed, [F4] then forces z∈R, a contradiction. Hence zm⊈m.

6.1F1step 1.3step 3.1step 4.1step 5.1algebra

By step 5.1, choose a∈m with az∉m. Since zm⊆R, the element u:=az lies in R. Being outside the maximal ideal, u is a unit. For every b∈m, the element zb lies in R, so b=u−1a(zb)∈aR. Thus m⊆aR⊆m, and m=aR is principal. Together with step 1.3, step 3.1 now gives condition 4.

7.1step 1.1step 1.2step 3.1step 3.2step 4.2step 6.1∎

Step 1.1 proves (1)⇒(2),(1)⇒(3),(1)⇒(4); steps 1.2 and 3.1 prove (2)⇒(4); step 3.2 proves (4)⇒(2); step 4.2 proves (4)⇒(1); and steps 1.3 to 6.1 prove (3)⇒(4). Therefore all four conditions are equivalent.

Depends on

Used by

Dependency tree · two levels

45 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