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.

Surjectivity survives arbitrary base change

Statement

Assuming the Axiom of Choice, a surjective scheme morphism $f : X \to S$ remains surjective after every base change $S^{'} \to S$ . In particular, for a field extension $K / k$ , a nonempty $k$ -scheme $X$ has nonempty $X_{K}$ .

Facts & Assumptions

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

[F1]

For scheme morphisms $f : X \to S$ and $g : Y \to S$ , points of $P = X \times_{S} Y$ are in bijection with quadruples $(x, y, s, r)$ where $f (x) = g (y) = s$ and $r \in Spec (κ (x) \otimes_{κ (s)} κ (y)) .$ The residue field at the corresponding point of $P$ is canonically $κ (r)$ . (Points of a fibre product via residue-field tensors)

[F2]

Let $R$ be a commutative ring. If $M$ is free with basis $(e_{i})_{i \in I}$ and $N$ is free with basis $(f_{j})_{j \in J}$ , then $M \otimes_{R} N$ is free with basis $(e_{i} \otimes f_{j})_{(i, j) \in I \times J} .$ Equivalently, the canonical map $R^{(I \times J)} \to M \otimes_{R} N$ sending the standard basis vector at $(i, j)$ to $e_{i} \otimes f_{j}$ is an isomorphism. This includes an empty basis in either factor. (The elementary tensors of two bases form the product basis of the tensor product)

[F3]

Assume the Axiom of Choice (def-axiom-of-choice). In a nonzero commutative ring, every proper ideal is contained in a maximal ideal. (In a nonzero commutative ring, every proper ideal is contained in a maximal ideal)

Proof

1.1

Let $s^{'} \in S^{'}$ and let $s$ be its image. Surjectivity gives $x \in X$ with $f (x) = s$ . The residue fields $κ (x)$ and $κ (s^{'})$ are nonzero vector spaces over $κ (s)$ . Under Choice choose bases containing the element 1; F2 makes their tensor product free on the nonempty product of those bases, so it is a nonzero ring. The same basis argument shows that $A \to A \otimes_{k} K$ , $a \mapsto a \otimes 1$ , is injective for any $k$ -algebra and field extension $K / k$ : choosing a basis of $K$ containing 1 identifies this map with inclusion of one summand (or use bases of both vector spaces).

givenF2

2.1

By F3 the zero ideal of that nonzero ring lies in a maximal ideal, which is prime. F1 then supplies a point of $X \times_{S} S^{'}$ projecting to $s^{'}$ . This proves surjectivity. If $S^{'}$ is empty the assertion is vacuous; if $S$ is empty both sources are empty.

F1F3step 1.1

3.1

A nonempty $X$ maps surjectively to the one-point scheme $Spec k$ . Applying the result to $Spec K \to Spec k$ gives a point of $X_{K}$ . Identity extensions also satisfy the argument; no algebraicity or reducedness hypothesis is used.

step 2.1given∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

19 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.4.D (standard reference, not scraped)