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.

A valuation ring is recovered from its value group

Statement

Let $V \subseteq K$ be a valuation ring, and let $Γ : = K^{\times} / V^{\times}$ be its value group. Define an order on $Γ$ by $\overline{x} \leq \overline{y} ⟺ y / x \in V .$ Then this order is well defined, total, and translation-invariant, so $Γ$ is a totally ordered abelian group.

If $v : K \to Γ \cup {\infty}$ is defined by $v (0) = \infty$ and $v (x) = \overline{x}$ for $x \in K^{\times}$ , then $v$ is a valuation on $K$ , and its valuation ring is exactly $V$ .

Facts & Assumptions

Given: A valuation ring $V$ in a field $K$ , and the quotient group $Γ = K^{\times} / V^{\times}$ .

[L1]

A valuation on a field is a map to a totally ordered abelian group adjoined with $\infty$ satisfying the exact-zero, multiplicative, and ultrametric laws (Valuations on a field).

[L2]

The value group of $V$ is the quotient group $K^{\times} / V^{\times}$ , and $\overline{x} \leq \overline{y}$ is intended to mean $y / x \in V$ (The value group of a valuation ring).

[A1]

If $u \in V^{\times}$ , then for every $z \in K^{\times}$ one has $z \in V$ if and only if $u z \in V$ .

Proof

technique · direct

1.1L2A1given

The order relation of [L2] is well defined on cosets: if $x^{'} = u x$ and $y^{'} = v y$ with $u, v \in V^{\times}$ , then $y^{'} / x^{'} = (v / u) (y / x)$ , and [A1] shows that $y^{'} / x^{'} \in V$ exactly when $y / x \in V$ .

1.2A1givenalgebra

The order is reflexive because $x / x = 1 \in V$ . It is antisymmetric because if $\overline{x} \leq \overline{y}$ and $\overline{y} \leq \overline{x}$ , then both $y / x$ and $x / y$ lie in $V$ , so $y / x$ is a unit of $V$ . Hence $x$ and $y$ represent the same coset in $Γ$ .

1.3L2givenalgebra

The order is transitive because $y / x \in V$ and $z / y \in V$ imply $z / x = (z / y) (y / x) \in V$ . It is total because $V$ is a valuation ring: for any $x, y \in K^{\times}$ , the quotient $y / x$ either lies in $V$ or has inverse $x / y$ in $V$ . It is translation-invariant because $\overline{x} + \overline{z} \leq \overline{y} + \overline{z}$ is equivalent to $(y z) / (x z) = y / x \in V$ . Thus $Γ$ is a totally ordered abelian group.

2.1L1step 1.3algebra

Define $v (0) = \infty$ and $v (x) = \overline{x}$ for $x \neq 0$ . Then $v (x) = \infty$ exactly when $x = 0$ , and for $x, y \neq 0$ one has $v (x y) = \overline{x y} = \overline{x} + \overline{y} = v (x) + v (y)$ . If $x + y = 0$ , then $v (x + y) = \infty \geq \min {v (x), v (y)}$ . Otherwise, after swapping $x$ and $y$ if needed, step 1.3 gives $v (x) \leq v (y)$ , so $y / x \in V$ and $x + y = x (1 + y / x)$ with $1 + y / x \in V$ ; hence $v (x + y) \geq v (x) = \min {v (x), v (y)}$ . Therefore $v$ satisfies the valuation axioms of [L1].

3.1L1L2step 2.1algebra∎

The nonnegative locus of $v$ is exactly $V$ : for $x \in K^{\times}$ , the condition $0 \leq v (x)$ means $\overline{1} \leq \overline{x}$ , which by [L2] is equivalent to $x \in V$ . Since $0 \in V$ as well, the valuation ring of $v$ is precisely $V$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

6 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, Proposition 8.6 (standard reference, not scraped)
Allen B. Altman and Steven L. Kleiman, A Term of Commutative Algebra, 13th ed., (26.11) (standard reference, not scraped)