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

Coordinate ring of an affine fibre

Statement

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.

Facts & Assumptions

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

[F1]

For a morphism $f : X \to S$ and any point $s \in S$ , its scheme-theoretic fibre is $X_{s} = X \times_{S} Spec κ (s),$ viewed as a $κ (s)$ -scheme. The map $Spec κ (s) \to S$ is the canonical residue-field point from lem-field-valued-points-of-schemes, and the product is base change as in def-base-change-morphism-schemes. The point $s$ need not be closed. A fibre over a generic point is called a generic fibre. Empty fibres are allowed. (Scheme-theoretic fibre)

[F2]

Let $A \to B$ and $A \to C$ be maps of commutative unital rings, allowing the zero ring. In the category of all schemes, $Spec B \times_{Spec A} Spec C ≅ Spec (B \otimes_{A} C) .$ The projections correspond to $b \mapsto b \otimes 1$ and $c \mapsto 1 \otimes c$ . (Affine fibre products are spectra of tensor products)

[F3]

Let $A \to C$ be a unital ring map. For any set of variables $(t_{i})$ and any ideal $I \subseteq A [t_{i}]$ , $(A [t_{i}] / I) \otimes_{A} C ≅ C [t_{i}] / I C [t_{i}] .$ Here the extended ideal is generated by the coefficient images of all elements of $I$ . For a multiplicative subset $M \subseteq A$ , $(M^{- 1} A) \otimes_{A} C ≅ {\overline{M}}^{- 1} C .$ These are ring isomorphisms; no flatness, finite-generation or nonzero-ring hypothesis is required. (Presentations and localization under base extension)

Proof

1.1

F1 defines the fibre as base change by $Spec κ (p)$ . F2 therefore gives its coordinate ring $B \otimes_{A} κ (p)$ .

givenF1F2

2.1

Write $κ (p) = A_{p} / p A_{p}$ . Localizing coefficients and then imposing the ideal relations, using F3, identifies the ring with $M^{- 1} B / p M^{- 1} B$ . The maps send $b \otimes (a / s m o d p)$ to $a b / s m o d p$ .

F3step 1.1

3.1

The formula preserves every element, including nilpotents. If the quotient is zero the fibre is empty; otherwise its primes and residue fields are retained. For $p = (0)$ in a domain it is extension to the fraction field, and for $B = A$ it is the one-point spectrum of $κ (p)$ .

step 2.1algebra∎

Depends on

Used by

Equal fibre points can have different multiplicities Counterexample
A closed-immersion fibre is one residue point or empty Example
An empty fibre from a zero tensor ring Example
Quadratic fibres over rational points and the generic point Example
The fibres of xy=t Example
Points and topology of a fibre Lemma
Stalks of the scheme-theoretic fibre Lemma

Dependency tree · two levels

10 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

Vakil 10.3.2; Stacks 26.18.4–5 (standard reference, not scraped)