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.

Field-valued points and local-ring points

Statement

For every field $K$ and scheme $X$ , morphisms $Spec K \to X$ correspond bijectively to pairs $(x, ι)$ with $x \in X$ and a field embedding $ι : κ (x) \to K$ . The identity embedding gives a canonical morphism $Spec κ (x) \to X$ , compatible with all scheme morphisms. More generally, for a nonzero local ring $(R, m)$ , morphisms $Spec R \to X$ correspond to pairs $(x, φ)$ with a local homomorphism $φ : O_{X, x} \to R$ . 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.

Facts & Assumptions

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

[F1]

For a point $x$ of a locally ringed space, put $κ (x) = O_{X, x} / m_{x}$ . If $x = p$ in an affine spectrum, the canonical isomorphism $O_{X, p} ≅ A_{p}$ carries $m_{p}$ to $p A_{p}$ and therefore induces canonical field isomorphisms $κ (p) ≅ A_{p} / p A_{p} ≅ Frac (A / p) .$ (The residue field at a point of an affine scheme)

[F2]

For a scheme $X$ and a ring $A$ , taking global sections induces a natural bijection $Hom (X, Spec A) ≅ {Hom}_{C R i n g} (A, Γ (X, O_{X})) .$ (Morphisms to an affine scheme and global sections)

[F3]

Let $(f, f^{♯}) : (X, O_{X}) \to (Y, O_{Y})$ be a morphism of locally ringed spaces, and let $x \in X$ . Then the local stalk map $f_{x}^{♯} : O_{Y, f (x)} ⟶ O_{X, x}$ induces a field homomorphism $κ (f (x)) ⟶ κ (x)$ between residue fields. (A local morphism of stalks induces a residue-field map)

[F4]

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)

[F5]

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

If $U = Spec A$ contains $x$ , F2 identifies a morphism $Spec R \to U$ with $ψ : A \to R$ . The preimage $p = ψ^{- 1} (m)$ is prime, and every element outside it maps to a unit. Thus $ψ$ factors uniquely through a local map $A_{p} \to R$ . Conversely any such local map gives $ψ$ and has closed-point image $p$ .

2.1step 1.1algebra

Every open neighbourhood of the closed point of $Spec R$ is the whole spectrum: a basic open containing that point is defined by an element outside $m$ , hence by a unit. Therefore any morphism to $X$ factors through every affine neighbourhood of its closed-point image. The affine constructions agree after shrinking to a common neighbourhood, by uniqueness of the map induced from the stalk. They consequently give inverse constructions globally; for $X = \emptyset$ both sets are empty.

3.1F1F3step 2.1

For $R = K$ a field, locality says precisely that the maximal ideal of $O_{X, x}$ maps to zero. Factoring through the quotient F1 gives a unital field map, necessarily injective. Conversely such an embedding gives a local map. Taking $R = O_{X, x}$ and its identity gives the canonical $Spec O_{X, x} \to X$ ; composing with its residue-field point gives $Spec κ (x) \to X$ . Every field-valued representative at $x$ factors uniquely through this residue-field representative by the specified embedding, so it is the smallest representative in its class. Identity embeddings give the canonical points, and F3 gives their compatibility with a morphism $X \to S$ by composing the residue-field maps.

4.1F4F5step 3.1∎

If two representatives at $x$ use fields $K, L$ , their tensor product over $κ (x)$ is nonzero: choose bases of these nonzero vector spaces and apply F4. By F5 choose a maximal ideal and take its quotient field $Ω$ . The unital maps $K, L \to Ω$ are injective and agree on $κ (x)$ , hence give a common representative by step 3.1. Conversely a common representative maps its unique point to both images, forcing those images equal. This is exactly where Choice is used.

Depends on

Used by

Dependency tree · two levels

26 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

Stacks 26.13, paragraphs preceding 26.13.3 and its field-valued special case (standard reference, not scraped)