TheoremStatement: 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-overlap criterion for separatedness

Statement

Let $f : X \to S$ be a morphism of schemes, let $S = ⋃_{i} W_{i}$ be an affine open cover and for each $i$ let $f^{- 1} (W_{i}) = ⋃_{j} U_{i j}$ be an affine open cover. Then $f$ is separated if and only if for every $i, j, k$ , writing $W_{i} = Spec A_{i}$ , $U_{i j} = Spec B_{i j}$ , $U_{i k} = Spec B_{i k}$ , the intersection $U_{i j} \cap U_{i k}$ is affine and the natural ring map $B_{i j} \otimes_{A_{i}} B_{i k} ⟶ Γ (U_{i j} \cap U_{i k}, O_{X})$ is surjective. The same condition may be checked for all pairs of affine opens $U, V \subseteq X$ lying over one and the same affine open of $S$ , without reference to a fixed chosen cover. Empty intersections use the zero ring.

Facts & Assumptions

Given: A morphism $f : X \to S$ with diagonal $Δ_{X / S} : X \to X \times_{S} X$ and projections ${pr}_{1}, {pr}_{2}$ .

[F1]

A morphism is separated when its diagonal is a closed immersion. (Separated morphism of schemes)

[F2]

The diagonal satisfies ${pr}_{1} Δ_{X / S} = {id}_{X} = {pr}_{2} Δ_{X / S}$ . (The diagonal morphism)

[F3]

If affine opens $U, V \subseteq X$ map into an open $W \subseteq S$ , then ${pr}_{1}^{- 1} (U) \cap {pr}_{2}^{- 1} (V)$ is an open subscheme of $X \times_{S} X$ representing $U \times_{W} V$ . (Restricting fibre products to open subschemes)

[F4]

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)

[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)

[F6]

A morphism $Z \to T$ is a closed immersion if and only if its restriction to each member of an open cover of $T$ is a closed immersion. (Closed immersions are local on the target)

[F7]

Every point of a scheme has an affine open neighbourhood, so affine opens form a basis. (Schemes)

Proof

technique · direct

1.1

Fix $i, j, k$ and put $Q = {pr}_{1}^{- 1} (U_{i j}) \cap {pr}_{2}^{- 1} (U_{i k})$ . By [F3] the open subscheme $Q$ of $X \times_{S} X$ represents $U_{i j} \times_{W_{i}} U_{i k}$ , which by [F4] is the affine scheme $Spec (B_{i j} \otimes_{A_{i}} B_{i k})$ .

F3F4given

2.1

By [F2] a point $x \in X$ has $Δ_{X / S} (x) \in Q$ exactly when $x \in U_{i j} \cap U_{i k}$ , so $Δ_{X / S}^{- 1} (Q) = U_{i j} \cap U_{i k}$ , and the restriction of $Δ_{X / S}$ to $Q$ is the canonical morphism $U_{i j} \cap U_{i k} \to Spec (B_{i j} \otimes_{A_{i}} B_{i k})$ .

F2step 1.1

2.2

The subschemes $Q$ of step 1.1 form an open cover of $X \times_{S} X$ : given a point $z$ with common image $w \in S$ , choose $i$ with $w \in W_{i}$ , so that ${pr}_{1} (z), {pr}_{2} (z) \in f^{- 1} (W_{i})$ , and then choose $j, k$ with ${pr}_{1} (z) \in U_{i j}$ and ${pr}_{2} (z) \in U_{i k}$ .

givenstep 1.1

3.1

Assume first the intersection condition of the statement. Then each $U_{i j} \cap U_{i k} = Spec D$ is affine and, as $B_{i j} \otimes_{A_{i}} B_{i k} \to D$ is surjective, [F5] exhibits the restriction of step 2.1 as a closed immersion.

F5step 2.1

3.2

Conversely, if $f$ is separated then the restriction of step 2.1 is a closed immersion, so by [F5] applied over the affine target $Spec (B_{i j} \otimes_{A_{i}} B_{i k})$ the source $U_{i j} \cap U_{i k}$ is affine, say $Spec D$ , and $B_{i j} \otimes_{A_{i}} B_{i k} \to D$ is surjective; for an empty intersection $D = 0$ is the zero ring.

F5step 2.1

3.3

For the version with all affine pairs: given $z$ as above and an affine open $W ∋ w$ , the affine opens of $X$ contained in $f^{- 1} (W)$ form a basis of $f^{- 1} (W)$ by [F7], so there are affine $U ∋ {pr}_{1} (z)$ and $V ∋ {pr}_{2} (z)$ with $U, V \subseteq f^{- 1} (W)$ ; the corresponding open subschemes ${pr}_{1}^{- 1} (U) \cap {pr}_{2}^{- 1} (V)$ again cover $X \times_{S} X$ .

F7step 2.2

4.1

Combining steps 3.1 and 3.2 with the locality statement [F6] applied to the open cover of step 2.2, the diagonal is a closed immersion exactly when the stated intersection condition holds; the same argument applies to the larger family of all affine pairs over a common affine base open by step 3.3.

F6step 3.1step 3.2step 2.2step 3.3

5.1

By [F1] the morphism $f$ is separated exactly in that case. Affineness of the intersections alone is not sufficient: the surjectivity clause is what fails for the doubled-origin line on the companion page.

F1step 4.1∎

Depends on

Used by

The affine line with doubled origin is not separated Corollary
DVR uniqueness need not detect nonseparatedness Counterexample
The relative projective-space diagonal is closed Lemma

Dependency tree · two levels

20 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, Lemmas 26.21.7-8 (tags 01KP-01KQ), printed p.41 (standard reference, not scraped)
Vakil, The Rising Sea, Sections 11.3.11-12, printed pp.311-312 (standard reference, not scraped)