ExampleConstruction: Literature-sourcedVerification: 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.

Ideals in a valuation ring are linearly ordered

Example

Let $V$ be the valuation ring from A nondiscrete rank-one valuation from incommensurate values, with value group $Γ = Z + Z \sqrt{2}$ . Then any two ideals of $V$ are comparable. The ideal

I : = {x \in V : x = 0 or v (x) > 1}

is an explicit nonprincipal ideal.

Facts & Assumptions

Given: The valuation ring $V$ and valuation $v$ constructed in A nondiscrete rank-one valuation from incommensurate values.

[L1]

In a valuation ring the ideals are linearly ordered by inclusion (Characterizations of valuation rings).

[L2]

The valuation ring in the incommensurate-value example has value group $Γ = Z + Z \sqrt{2}$ , and that ordered group has no least positive element (A nondiscrete rank-one valuation from incommensurate values).

Verification

technique · direct

1.1

The ideal-comparability statement is exactly [L1]. For the displayed set $I$ , closure under multiplication by elements of $V$ is immediate because $v (z x) = v (z) + v (x) \geq v (x) > 1$ when $v (z) \geq 0$ . If $x, y \in I$ , then $v (x + y) \geq \min {v (x), v (y)} > 1$ , so $x + y \in I$ . Thus $I$ is an ideal of $V$ .

L1L2givenalgebra

2.1

If $I = (a)$ were principal, then $v (a) > 1$ and every element of $I$ would have value at least $v (a)$ . But [L2] says there is no least element of the set ${γ \in Γ : γ > 1}$ , so one can choose $1 < γ < v (a)$ and then an element $x \in V$ with $v (x) = γ$ . Such an $x$ lies in $I$ but not in $(a)$ , contradiction. Hence $I$ is nonprincipal.

L2step 1.1algebra∎

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

Allen B. Altman and Steven L. Kleiman, A Term of Commutative Algebra, 13th ed., Exercise (26.3) and Example (26.12) (standard reference, not scraped)
The Stacks Project, Section 10.50: Valuation rings (standard reference, not scraped)