CorollaryStatement: 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.

Prime ideals and dimension of a DVR

Statement

Let $V$ be a discrete valuation ring with maximal ideal $m$ . Then the only prime ideals of $V$ are $(0)$ and $m$ . In particular, $\dim V = 1.$

Facts & Assumptions

Given: A discrete valuation ring $V$ with maximal ideal $m = (π)$ .

[L1]

Every nonzero ideal of $V$ is $(π^{n}) = m^{n}$ for a unique $n \geq 0$ (Ideals in a DVR are powers of the maximal ideal).

[F1]

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

[A1]

A discrete valuation ring is a domain, so $(0)$ is prime.

Proof

technique · direct

1.1L1givenalgebra

Let $p$ be a nonzero prime ideal of $V$ . Choose $0 \neq x \in p$ . By [L1], $x = u π^{n}$ for some unit $u$ and some $n \geq 1$ , so $π^{n} \in p$ . Since $p$ is prime, $π \in p$ . Therefore $m = (π) \subseteq p$ , and maximality of $m$ forces $p = m$ .

2.1F1A1step 1.1∎

By [A1], $(0)$ is prime, and step 1.1 shows there are no other nonzero primes besides $m$ . Therefore the prime spectrum has exactly the strict chain $(0) ⊊ m$ . Its length is $1$ , and no longer chain exists. Hence [F1] gives $\dim V = 1$ .

Depends on

Used by

Dependency tree · two levels

5 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

M. Mustata, Commutative Algebra, Remark 8.9 (standard reference, not scraped)
Allen B. Altman and Steven L. Kleiman, A Term of Commutative Algebra, 13th ed., (23.1) (standard reference, not scraped)