LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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.

Points and topology of a fibre

Statement

For $f : X \to S$ and $s \in S$ , the projection $X_{s} \to X$ is a homeomorphism onto $f^{- 1} (s)$ with the subspace topology and preserves the residue field at every point. In compatible affine charts $A \to B$ , $s = p$ , its points correspond exactly to primes $q \subset B$ contracting to $p$ ; no extra embedding choice occurs. Also $X \times_{S} Spec O_{S, s} \to X$ is a homeomorphism onto the inverse image of the set of generalizations of $s$ .

Facts & Assumptions

Given: The objects, hypotheses and conventions in the statement above.

[F1]

Let $A \to B$ be a ring map, $p \in Spec A$ , and $M = A ∖ p$ , acting on $B$ through the ring map. The fibre over $p$ is canonically $Spec (B \otimes_{A} κ (p)) ≅ Spec (M^{- 1} B / p M^{- 1} B) .$ The residue field is $κ (p) = A_{p} / p A_{p}$ . No reduction of the tensor ring is taken. (Coordinate ring of an affine fibre)

[F2]

Suppose $P = X \times_{S} Y$ exists, with projections $p, q$ . If opens $V \subseteq X$ , $W \subseteq Y$ map into an open $U \subseteq S$ , then the open subscheme $Q = p^{- 1} (V) \cap q^{- 1} (W)$ represents $V \times_{U} W$ , and also $V \times_{S} W$ . Independently, for $f : X \to S$ and an open $U \subseteq S$ , the open subscheme $f^{- 1} (U)$ represents $X \times_{S} U$ . (Restricting fibre products to open subschemes)

[F3]

Let $R$ be a commutative ring, let $S \subseteq R$ be multiplicative, and let $λ : R \to S^{- 1} R$ be the localisation map. Then contraction along $λ$ is a homeomorphism from $Spec (S^{- 1} R)$ onto the subspace $X : = {p \in Spec (R) : p \cap S = \emptyset} .$ (The spectrum of a localisation is the subspace of primes disjoint from the denominator set)

[F4]

Let $R$ be a commutative ring, let $I ⊴ R$ be an ideal, and let $π : R \to R / I$ be the quotient map. Then contraction along $π$ induces an inclusion-preserving bijection $Spec (R / I) \to V (I)$ , sending $q$ to $π^{- 1} (q)$ . Its inverse sends a prime ideal $p \supseteq I$ to $p / I$ . (Prime ideals of a quotient ring are exactly the prime ideals containing the ideal)

Proof

1.1

On compatible affine charts put $M = A ∖ p$ . F1 gives the fibre ring $D = M^{- 1} B / p M^{- 1} B$ . By F3 and F4 its primes are exactly primes $q$ of $B$ disjoint from $M$ and containing $p B$ . These two requirements say precisely $q \cap A = p$ . Extension followed by quotient and contraction are inverse.

givenF1F3F4

2.1

The basic open $D_{D} (\overline{b / m})$ corresponds to $D_{B} (b) \cap f^{- 1} (p)$ , since $m$ is already a unit. Such opens form a basis on both sides, proving the subspace topology assertion, not merely a bijection. Localizing $D$ at this prime and then taking its residue field gives $Frac (B / q)$ , the original residue field.

step 1.1algebra

3.1

F2 restricts the fibre to the same affine opens, so these identifications agree on overlaps by contraction and glue to the global homeomorphism. Empty affine fibres contribute no primes. Without the quotient by $p$ , F3 identifies the local-base pullback with primes whose contractions are contained in $p$ , exactly the generalizations of $s$ . The same basic-open calculation and gluing prove the last assertion. This includes generic and closed points.

F2F3step 1.1step 2.1∎

Depends on

Used by

Stalks of the scheme-theoretic fibre Lemma
What the underlying fibre set forgets Remark

Dependency tree · two levels

15 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

Stacks 26.18.5; Vakil 10.3.B (standard reference, not scraped)