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

Affine schemes and affine morphisms are separated

Statement

Every morphism of affine schemes $Spec B \to Spec A$ is separated. Every affine scheme is separated over $Spec Z$ , that is, absolutely separated. More generally every affine morphism to an arbitrary scheme is separated. Affineness is not inferred back from separatedness.

Facts & Assumptions

Given: A ring map $A \to B$ , the induced morphism $u : Spec B \to Spec A$ , and an affine open subscheme $U = Spec R \subseteq Spec A$ .

[F1]

Every affine morphism of schemes is separated. (Affine morphisms are separated)

[F2]

A morphism $f : X \to S$ is affine when $f^{- 1} (W)$ is affine for every affine open subscheme $W \subseteq S$ ; the empty scheme is affine, being $Spec 0$ . (Affine morphisms)

[F3]

An $S$ -scheme $X$ is separated over $S$ when its structure morphism $X \to S$ is separated, and absolutely separated when it is separated over $Spec Z$ . (Separated S-scheme)

[F4]

For $f : X \to S$ and an open $W \subseteq S$ , the open subscheme $f^{- 1} (W)$ represents the fibre product $X \times_{S} W$ . (Restricting fibre products to open subschemes)

[F5]

For ring maps $A \to B$ , $A \to C$ , allowing the zero ring, $Spec B \times_{Spec A} Spec C ≅ Spec (B \otimes_{A} C)$ . (Affine fibre products are spectra of tensor products)

Proof

1.1

Let $U = Spec R$ be an affine open subscheme of $Spec A$ . By [F4] the inverse image $u^{- 1} (U)$ represents $Spec B \times_{Spec A} U$ , and by [F5] this fibre product is $Spec (B \otimes_{A} R)$ , an affine scheme; the zero-ring cases $B = 0$ and $R = 0$ are included. Hence $u$ is affine by [F2].

F2F4F5given

1.2

For any scheme $S$ and any affine morphism $g : X \to S$ , the morphism $g$ is separated by [F1], whatever $S$ and $X$ are; in particular no separatedness of $X$ over another base is deduced.

F1given

2.1

Applying step 1.1 to the unique ring map $Z \to B$ shows that the structure morphism $Spec B \to Spec Z$ is affine, hence separated by [F1]; by [F3] the scheme $Spec B$ is absolutely separated. The zero ring $B = 0$ is allowed: $Spec 0 = \emptyset$ is affine by [F2] and its structure morphism is again affine.

F1F2F3step 1.1

2.2

Taking $X = Spec B$ and $S = Spec A$ in step 1.2 gives the separatedness of $u$ ; taking an arbitrary scheme as $S$ and an arbitrary affine morphism as $g$ gives the third assertion.

step 1.2

3.1

Steps 2.1 and 2.2 prove that every morphism of affine schemes, every structure morphism $Spec B \to Spec Z$ , and every affine morphism to an arbitrary scheme is separated. Separatedness is a property of the structure morphism and of a chosen base, so nothing here identifies separatedness with affineness.

step 2.1step 2.2∎

Depends on

Used by

A separated scheme whose point space is not Hausdorff Counterexample
Separated is not Zariski Hausdorff Remark

Dependency tree · two levels

19 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.21.15, printed p.42 (standard reference, not scraped)