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.

Characterizations of valuation rings

Statement

Let $V$ be a domain with fraction field $K$ . The following are equivalent.

$V$ is a valuation ring of $K$ .
For every $a, b \in V$ , one of $a$ and $b$ divides the other in $V$ .
The ideals of $V$ are linearly ordered by inclusion.

When these conditions hold, every finitely generated ideal of $V$ is principal.

Facts & Assumptions

Given: A domain $V$ with fraction field $K$ .

[F1]

A valuation ring is a subring $V \subseteq K$ such that for every nonzero $x \in K$ at least one of $x$ and $x^{- 1}$ lies in $V$ (Valuation rings).

[L1]

A valuation ring is local, and its nonunits form the unique maximal ideal (A valuation ring is local).

[A1]

Every nonzero element of the fraction field $K$ can be written as $a / b$ with $a, b \in V$ and $b \neq 0$ .

Proof

technique · direct

1.1

Assume condition 1. Let $a, b \in V$ . If $a = 0$ or $b = 0$ , divisibility is trivial. If $a, b \neq 0$ , apply [F1] to $a / b \in K^{\times}$ : if $a / b \in V$ , then $a = (a / b) b$ , so $b$ divides $a$ ; if $b / a \in V$ , then $a$ divides $b$ . Thus condition 2 holds.

F1given

1.2

Assume condition 2. Let $I$ and $J$ be ideals of $V$ . If $I \subseteq̸ J$ , choose $a \in I ∖ J$ . For any $b \in J$ , condition 2 says either $a$ divides $b$ or $b$ divides $a$ ; the second option would put $a$ in $J$ , so $b = c a$ for some $c \in V$ and hence $b \in I$ . Therefore $J \subseteq I$ . By symmetry, any two ideals are comparable, so condition 3 holds.

givenalgebra

1.3

Assume condition 3. Let $x \in K^{\times}$ , and choose $a, b \in V$ with $b \neq 0$ and $x = a / b$ by [A1]. The principal ideals $(a)$ and $(b)$ are comparable. If $(a) \subseteq (b)$ , then $a = b c$ for some $c \in V$ , so $x = c \in V$ . If $(b) \subseteq (a)$ , then $b = a d$ for some $d \in V$ , so $x^{- 1} = d \in V$ . Thus condition 1 holds.

A1givenalgebra

2.1

Under condition 3, a finitely generated ideal $I = (a_{1}, \dots, a_{n})$ is principal: among the finitely many comparable principal ideals $(a_{i})$ , choose a largest one, say $(a_{j})$ . Then every $a_{i}$ lies in $(a_{j})$ , so $I = (a_{j})$ . The zero ideal is $(0)$ , and step 1.3 now identifies $V$ as a valuation ring, so [L1] records the local consequence for nonunits.

L1step 1.3algebra∎

Depends on

Used by

Ideals in a valuation ring are linearly ordered Example
A Noetherian valuation ring is a field or a DVR Theorem
A valuation ring is recovered from its value group Theorem
Equivalent characterizations of a DVR Theorem

Dependency tree · one level

2 results within one dependency step 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, Propositions 8.3-8.6 (standard reference, not scraped)
Allen B. Altman and Steven L. Kleiman, A Term of Commutative Algebra, 13th ed., Exercise (26.3) and Exercise (26.15)(1) (standard reference, not scraped)