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.1givenF1F2

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.

2.1F3step 1.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$ .

Depends on

Used by

A reduced field spectrum becomes nonreduced Counterexample
An integral real scheme splits over the complex numbers Counterexample
The equation must define the intended scheme Counterexample
Geometric fibres and geometric points Definition
Geometric genus of a singular curve Definition
A real conic acquires complex points Example
Function field of an integral finite-type scheme Lemma
Why geometric properties differ from ordinary ones Remark
Purely inseparable field algebras separate regularity from smoothness Theorem
Smooth proper curves, dominant morphisms and function fields Theorem

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)