Alphabeta Math
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.

Fibres after base change

Statement

Let SS send s to s. For any XS there is a canonical isomorphism of κ(s)-schemes (XS)sXs×Specκ(s)Specκ(s).

Facts & Assumptions

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

[F1]

For a morphism f:XS and any point sS, its scheme-theoretic fibre is Xs=X×SSpecκ(s), viewed as a κ(s)-scheme. The map Specκ(s)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]

For SkShS and an S-scheme X, there is a canonical isomorphism (X×SS)×SSX×SS. It is functorial in X and compatible with the induced maps of S-schemes. (Iterated base change)

[F3]

For every field K and scheme X, morphisms SpecKX correspond bijectively to pairs (x,ι) with xX and a field embedding ι:κ(x)K. The identity embedding gives a canonical morphism Specκ(x)X, compatible with all scheme morphisms. More generally, for a nonzero local ring (R,m), morphisms SpecRX correspond to pairs (x,φ) with a local homomorphism φ:OX,xR. Assuming Choice, two field-valued points have the same image in X if and only if they are dominated by a common field-valued point, by compatible embeddings of their fields into a third field. (Field-valued points and local-ring points)

Proof

1.1

By F3 the canonical point Specκ(s)S factors through Specκ(s) via the residue-field embedding. F1 and F2 identify the left side with X×SSpecκ(s).

givenF1F2F3
2.1

Apply F2 once more to the factorization through Specκ(s). It gives exactly the displayed right side, with the same projection to Specκ(s). Both operations are canonical on test morphisms and are inverse regroupings; no closure, finite extension or flatness assumption is needed. If Xs is empty both sides represent only empty test schemes; identity residue-field extension gives Xs.

F2step 1.1

Depends on

Used by

Nothing in the library uses this result yet.

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