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 send to . For any there is a canonical isomorphism of -schemes
Facts & Assumptions
Given: The objects, hypotheses and conventions in the statement above.
For a morphism and any point , its scheme-theoretic fibre is viewed as a -scheme. The map 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 need not be closed. A fibre over a generic point is called a generic fibre. Empty fibres are allowed. (Scheme-theoretic fibre)
For and an -scheme , there is a canonical isomorphism It is functorial in and compatible with the induced maps of -schemes. (Iterated base change)
For every field and scheme , morphisms correspond bijectively to pairs with and a field embedding . The identity embedding gives a canonical morphism , compatible with all scheme morphisms. More generally, for a nonzero local ring , morphisms correspond to pairs with a local homomorphism . Assuming Choice, two field-valued points have the same image in 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
By F3 the canonical point factors through via the residue-field embedding. F1 and F2 identify the left side with .
Apply F2 once more to the factorization through . It gives exactly the displayed right side, with the same projection to . Both operations are canonical on test morphisms and are inverse regroupings; no closure, finite extension or flatness assumption is needed. If is empty both sides represent only empty test schemes; identity residue-field extension gives .
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
- Vakil 10.3.C (standard reference, not scraped)