ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-27

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.

The diagonal of the affine line

Example

Let $A$ be a commutative unital ring and $S = Spec A$ , and let $A_{S}^{1} = Spec A [x]$ with structure morphism $A \to A [x]$ . Then the diagonal $Δ : Spec A [x] \to Spec A [x] \times_{S} Spec A [x]$ is a closed immersion into $Spec A [x, y] ≅ Spec A [x] \times_{S} Spec A [x]$ whose ideal is $(x - y)$ . Consequently $A_{S}^{1} \to S$ is separated, and for $A = Z$ this is the diagonal of $Spec Z [x]$ . If instead $S$ is an arbitrary scheme and $A_{S}^{1} = Spec Z [x] \times_{Spec Z} S$ , then on each affine open $Spec A \subseteq S$ the same equation $x - y$ cuts out the diagonal, so the formula glues over an arbitrary base.

Facts & Assumptions

Given: A commutative unital ring $A$ , the affine scheme $S = Spec A$ , the affine line $X = Spec A [x]$ over $S$ with structure morphism $A \to A [x]$ , and the diagonal $Δ = Δ_{X / S}$ .

[F1]

For every morphism $X \to S$ the diagonal is the unique morphism $Δ_{X / S} : X \to X \times_{S} X$ with ${pr}_{1} Δ_{X / S} = {id}_{X} = {pr}_{2} Δ_{X / S}$ . (The diagonal morphism)

[F2]

For ring maps $A \to B$ and $A \to C$ there is an isomorphism $Spec B \times_{Spec A} Spec C ≅ Spec (B \otimes_{A} C)$ , with the projections corresponding to $b \mapsto b \otimes 1$ and $c \mapsto 1 \otimes c$ . (Affine fibre products are spectra of tensor products)

[F3]

For a ring $A$ , closed immersions $Z \to Spec A$ are, up to unique isomorphism over $Spec A$ , precisely the morphisms $Spec (A / I) \to Spec A$ for ideals $I \subseteq A$ . (Closed immersions into affine schemes are quotient spectra)

[F4]

A morphism is a closed immersion if and only if its restriction to every member of an open cover of the target is a closed immersion. (Closed immersions are local on the target)

[F5]

For a base change $S^{'} \to S$ of $X \to S$ , the diagonal of $X \times_{S} S^{'} \to S^{'}$ is the base change of $Δ_{X / S}$ along $X \times_{S} X \to S$ ; in particular it is determined on each open of the target by $Δ_{X / S}$ . (The diagonal commutes with base change)

[F6]

For any two schemes with morphisms to a common scheme the fibre product exists, so $A_{S}^{1} = Spec Z [x] \times_{Spec Z} S$ is a scheme over $S$ ; over $S = Spec A$ it is $Spec A [x]$ by [F2]. (Existence of all scheme fibre products)

Verification

1.1

By [F2] applied to $A \to A [x]$ twice, $Spec A [x] \times_{S} Spec A [x] ≅ Spec (A [x] \otimes_{A} A [x])$ , and the latter is $Spec A [x, y]$ with ${pr}_{1}$ corresponding to $x \mapsto x \otimes 1 = x$ and ${pr}_{2}$ to $x \mapsto 1 \otimes x = y$ .

F2given

2.1

By [F1] the diagonal corresponds, under the identification of step 1.1, to a ring map $μ : A [x, y] \to A [x]$ with $μ (x) = x$ and $μ (y) = x$ , namely the multiplication $x \otimes 1 \mapsto x$ , $1 \otimes x \mapsto x$ .

F1step 1.1given

3.1

The map $μ$ is surjective, and its kernel is $(x - y)$ : writing $A [x, y] = A [x] [u]$ with $u = y - x$ , the map $μ$ is the $A [x]$ -algebra map sending $u$ to $0$ , whose kernel is the principal ideal $(u) = (x - y)$ .

step 2.1algebra

4.1

By [F3] the closed subscheme of $Spec A [x, y]$ with ideal $(x - y)$ is presentable as $Spec (A [x, y] / (x - y))$ , and $A [x, y] / (x - y) \to A [x]$ , $x \mapsto x$ , $y \mapsto x$ , is an isomorphism of $A$ -algebras; hence the diagonal is exactly the closed subscheme $V (x - y)$ and in particular a closed immersion.

F3step 3.1

5.1

Now let $S$ be arbitrary and $A_{S}^{1} = Spec Z [x] \times_{Spec Z} S$ as in [F6], and let $Spec A \subseteq S$ be an affine open. Base changing along $Spec A ↪ S$ produces the affine line $Spec A [x]$ over $Spec A$ , whose diagonal is cut out by $x - y$ as computed in step 4.1, and by [F5] these local diagonal conditions are the restrictions to the open subscheme $Spec A \times_{S} Spec A$ of the product. Since these products over an affine open cover of $S$ cover $A_{S}^{1} \times_{S} A_{S}^{1}$ , [F4] shows that the diagonal of $A_{S}^{1} \to S$ is a closed immersion cut out by $x - y$ on each such piece, and by [F1] and [F3] its ideal in the chart ring $A [x, y]$ is $(x - y)$ .

F1F3F4F5F6step 4.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

15 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

The Stacks Project, Schemes, Lemma 26.21.1 (tag 01KI) and Definition 26.21.3, printed pp.39-40 (standard reference, not scraped)
Ravi Vakil, The Rising Sea, Proposition 11.3.1, printed pp.306-307 (standard reference, not scraped)