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 projective-line diagonal from the bihomogeneous equation

Example

For every scheme $S$ , the diagonal of $P_{S}^{1} \to S$ is the closed subscheme of $P_{S}^{1} \times_{S} P_{S}^{1}$ cut out by the bihomogeneous equation $x_{0} y_{1} - x_{1} y_{0} = 0$ , read in the two pairs of homogeneous coordinates $x_{0} : x_{1}$ and $y_{0} : y_{1}$ . On the four products $U_{i} \times_{S} V_{j}$ of standard charts the equation becomes $y_{1} / y_{0} - x_{1} / x_{0} = 0, (x_{1} / x_{0}) (y_{0} / y_{1}) - 1 = 0, (x_{0} / x_{1}) (y_{1} / y_{0}) - 1 = 0, y_{0} / y_{1} - x_{0} / x_{1} = 0,$ which is the equality of the two chart coordinates on the overlap $U_{i} \cap V_{j}$ in each case. Over $S = Spec k$ for a field $k$ this is the classical description of the diagonal of $P_{k}^{1}$ .

Facts & Assumptions

Given: A scheme $S$ , the relative projective line $P_{S}^{1}$ with its two standard charts $U_{0}, U_{1}$ and coordinates $x = x_{1} / x_{0}$ on $U_{0}$ , $v = x_{0} / x_{1}$ on $U_{1}$ , the second factor with charts $V_{0}, V_{1}$ and coordinates $y = y_{1} / y_{0}$ , $z = y_{0} / y_{1}$ , and the diagonal $Δ$ of $P_{S}^{1} \to S$ .

[F1]

The charts $U_{i}$ are affine and cover $P_{S}^{1}$ ; on an affine base $S = Spec A$ one has $U_{0} = Spec A [x]$ , $U_{1} = Spec A [v]$ and $U_{0} \cap U_{1} = Spec A [x, x^{- 1}] = Spec A [v, v^{- 1}]$ , all compatible with base change. (Relative projective space from standard charts)

[F2]

For $i \neq j$ the restriction of $Δ$ to $U_{i} \times_{S} U_{j}$ is the closed immersion of the affine overlap $U_{i} \cap U_{j}$ cut out in the chart-product coordinate ring by $x_{j}^{(i)} y_{i}^{(j)} - 1$ and $y_{m}^{(j)} - x_{m}^{(i)} y_{i}^{(j)}$ for $m \neq i, j$ ; for $i = j$ the chart form is the difference of the two coordinates. These generators are dehomogenized forms of $x_{a} y_{b} - x_{b} y_{a}$ . (The relative projective-space diagonal is closed)

[F3]

For ring maps $A \to B$ , $A \to C$ the fibre product of the affine spectra is $Spec (B \otimes_{A} C)$ . (Affine fibre products are spectra of tensor products)

Verification

1.1

Over an affine base $S = Spec A$ the four products of charts are affine by [F3]: $U_{0} \times_{S} U_{0} = Spec A [x, y]$ , $U_{0} \times_{S} U_{1} = Spec A [x, z]$ , $U_{1} \times_{S} U_{0} = Spec A [v, y]$ , $U_{1} \times_{S} U_{1} = Spec A [v, z]$ .

F1F3

1.2

The equation $x_{0} y_{1} - x_{1} y_{0} = 0$ is bihomogeneous of bidegree $(1, 1)$ , so its restriction to each product of charts is obtained by dividing by the two chosen coordinates; this gives the four displayed equations in the order $(U_{0}, V_{0}), (U_{0}, V_{1}), (U_{1}, V_{0}), (U_{1}, V_{1})$ .

F1given

2.1

On $U_{0} \times_{S} U_{0} = Spec A [x, y]$ the equation becomes $y - x = 0$ , which is the difference of the two copies of the coordinate $x_{1} / x_{0}$ ; by [F2] this is the chart form of the diagonal, and $A [x, y] \to A [x]$ , $y \mapsto x$ , exhibits it as a closed immersion with image the diagonal copy of $U_{0}$ .

F2step 1.2

2.2

On $U_{0} \times_{S} U_{1} = Spec A [x, z]$ the equation becomes $1 - x z = 0$ , exactly [F2]'s mixed-chart generator $x_{1}^{(0)} y_{0}^{(1)} - 1$ up to sign, with $z = y_{0} / y_{1}$ and $x = x_{1} / x_{0}$ ; the quotient is $A [x, x^{- 1}]$ via $z \mapsto x^{- 1}$ , so the diagonal over this chart product is the closed subscheme isomorphic to the overlap $U_{0} \cap U_{1}$ .

F2step 1.2

3.1

The remaining two products are obtained from steps 2.1 and 2.2 by swapping the two factors: on $U_{1} \times_{S} U_{0} = Spec A [v, y]$ the equation becomes $v y = 1$ , and on $U_{1} \times_{S} U_{1} = Spec A [v, z]$ it becomes $z - v = 0$ .

step 1.2step 2.1step 2.2F2

4.1

Both sides are compatible with base change along any $S^{'} \to S$ by [F1], so the four chart computations glue: on every standard chart product the diagonal is the closed subscheme cut out by $x_{0} y_{1} - x_{1} y_{0} = 0$ , which is the assertion.

F1step 2.1step 2.2step 3.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

16 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, Example 26.21.8 (tag 01KQ), printed p.41 (standard reference, not scraped)
Ravi Vakil, The Rising Sea, Proposition 11.3.8, printed pp.309-310 (standard reference, not scraped)