LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-27

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.

Separatedness implies valuative uniqueness

Statement

Let $f : X \to S$ be a separated morphism of schemes. Then $f$ satisfies the uniqueness part of the valuative criterion: for every valuation ring $R$ with fraction field $K$ and every valuative diagram for $f$ , there is at most one lift $Spec R \to X$ . No quasi-separatedness, finite-type, Noetherian or Choice hypothesis is required.

Facts & Assumptions

Given: A separated morphism $f : X \to S$ and a valuative diagram consisting of a valuation ring $R \subseteq K$ with fraction field $K$ , a morphism $g : Spec K \to X$ and a morphism $Spec R \to S$ with $f g$ equal to the composite $Spec K \to Spec R \to S$ .

[F1]

Such data form a valuative diagram for $f$ ; a lift is a morphism $Spec R \to X$ compatible with $g$ and with $Spec R \to S$ . (Valuative uniqueness diagram)

[F2]

A morphism $f : X \to S$ is separated when $Δ_{X / S}$ is a closed immersion. (Separated morphism of schemes)

[F3]

If $Y \to S$ is separated and $a, b : X \to Y$ are $S$ -morphisms, then their equalizer exists as a closed subscheme $e : E ↪ X$ and represents agreement: for every scheme $T$ the morphisms $T \to E$ correspond bijectively to the $t : T \to X$ with $a t = b t$ . (Equalizers into separated schemes are closed)

[F4]

A valuation ring $R \subseteq K$ is a subring of the field $K$ such that for every $x \in K^{\times}$ at least one of $x$ , $x^{- 1}$ lies in $R$ ; in particular $R$ is a domain and the canonical morphism $Spec K \to Spec R$ has image the generic point $(0)$ of $Spec R$ . (Valuation rings)

[F5]

For a ring $A$ , closed immersions $Z \to Spec A$ are, up to unique isomorphism over $Spec A$ , precisely the morphisms $Spec (A / I) \to Spec A$ for ideals $I \subseteq A$ . (Closed immersions into affine schemes are quotient spectra)

Proof

technique · direct

1.1

Suppose $u, v : Spec R \to X$ are two lifts of the given diagram. Then $u$ and $v$ are $S$ -morphisms, since $f u$ and $f v$ both equal the given $Spec R \to S$ , and $u \circ i = v \circ i = g$ where $i : Spec K \to Spec R$ .

F1given

1.2

Apply [F3] to the $S$ -morphisms $u, v : Spec R \to X$ ; here $Y = X$ is separated over $S$ by [F2], so the equalizer is a closed subscheme $e : E \to Spec R$ representing agreement on every scheme.

F2F3given

1.3

By [F4] the ring $R$ is a domain, so $Spec R$ has generic point $(0)$ , the image of $i$ ; the only ideal $I \subseteq R$ with $(0) \in V (I)$ is $I = 0$ .

2.1

Because $u i = v i$ , the universal property of the equalizer in [F3] applied to the test scheme $Spec K$ produces a morphism $Spec K \to E$ whose composite with $e$ is $i$ ; hence the image of the generic morphism $i$ is contained in the image of $e$ .

F3step 1.2

3.1

By [F5] the closed immersion $e : E \to Spec R$ presents $E$ as $Spec (R / I)$ for $I$ the kernel of $R \to Γ (E, O_{E})$ , with underlying space $V (I)$ . Since the generic point $(0)$ of $Spec R$ lies in $e (E) = V (I)$ by step 2.1, we have $I \subseteq (0)$ , so $I = 0$ by step 1.3 and $e$ is an isomorphism.

F5step 2.1step 1.3

4.1

Since $E$ is the equalizer, the identity of $E$ corresponds under [F3] to the pair $(e u, e v)$ , so $u \circ e = v \circ e$ ; as $e$ is an isomorphism by step 3.1, $u = v$ . Hence any two lifts coincide, which is the uniqueness assertion for the given diagram.

F3step 3.1∎

Depends on

Used by

Dependency tree · two levels

16 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

The Stacks Project, Schemes, Lemma 26.22.1 (tag 01KZ), printed p.44 (standard reference, not scraped)