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.

Affine charts after extension of the ground field

Statement

For a field extension $K / k$ and a $k$ -scheme $X$ , the inverse image under $X_{K} \to X$ of every affine open $U = Spec A$ in $X$ is $Spec (A \otimes_{k} K)$ . These affine charts cover $X_{K}$ and are compatible on overlaps and with coefficient localizations.

Facts & Assumptions

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

[F1]

Let $h : S^{'} \to S$ . For an $S$ -scheme $f : X \to S$ , its base change is $X_{S^{'}} = X \times_{S} S^{'}$ , with structure map the second projection. For an $S$ -morphism $u : X \to Y$ , define $u_{S^{'}} : X_{S^{'}} \to Y_{S^{'}}$ by its projections $u \circ {pr}_{X}$ and ${pr}_{S^{'}}$ . Existence and uniqueness follow from thm-fibre-products-of-schemes-exist; the meaning of $S$ -morphism is def-scheme-over-base. These formulas preserve identities and composition because their projections do, so they define a functor. A property of morphisms is stable under arbitrary base change when every pullback of a morphism with that property again has it. No restriction such as flatness is implicit in “arbitrary”. (Base change of objects, morphisms and properties)

[F2]

Every diagram $X \to S \leftarrow Y$ of schemes has a fibre product. Given an affine cover $S = ⋃_{i} Spec A_{i}$ and affine covers $f^{- 1} (Spec A_{i}) = ⋃_{j} Spec B_{i j}$ and $g^{- 1} (Spec A_{i}) = ⋃_{k} Spec C_{i k}$ , the product has open affine cover $Spec (B_{i j} \otimes_{A_{i}} C_{i k}) .$ (Existence of all scheme fibre 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

Apply the affine cover assertion of F2 over the single affine base $Spec k$ and its new base $Spec K$ . With the base-change definition F1, it identifies each inverse-image chart with $Spec (A \otimes_{k} K)$ and shows they cover.

givenF1F2

2.1

For a principal subchart $D (a)$ , F3 gives $A_{a} \otimes_{k} K ≅ (A \otimes_{k} K)_{a \otimes 1}$ , with exactly the same coefficient restrictions. Covering any overlap by affine subcharts proves compatibility there as well; the universal projections determine the same identification. Empty charts have ring zero, and $K = k$ gives the original charts. No reduction or algebraicity assumption has entered. The same polynomial coefficient formula gives $A_{C}^{n} ≅ A_{A}^{n} \times_{Spec A} Spec C$ for every ring map $A \to C$ , including $A = Z$ and $n = 0$ .

F3step 1.1∎

Depends on

Used by

A reduced field spectrum becomes nonreduced Counterexample
An integral real scheme splits over the complex numbers Counterexample
Geometric fibres and geometric points Definition
A real conic acquires complex points Example
Why geometric properties differ from ordinary ones Remark

Dependency tree · two levels

9 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.2.3 (standard reference, not scraped)