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

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.

Polynomial Proj charts

Example

Assume the Axiom of Choice (The Axiom of Choice). Let $k$ be a field and $n \geq 0$ , and give $S = k [x_{0}, \dots, x_{n}]$ the total-degree grading with $\deg x_{i} = 1$ . Then $Proj S = P_{k}^{n},$ the chart $D_{+} (x_{i})$ is $Spec k [x_{0} / x_{i}, \dots, x_{n} / x_{i}]$ with the variable $x_{i} / x_{i}$ omitted (it equals $1$ ), and on the overlap $D_{+} (x_{i} x_{j})$ the coordinate change between the $i$ -th and $j$ -th charts sends $\frac{x_{a}}{x_{j}} = \frac{x_{a} / x_{i}}{x_{j} / x_{i}},$ so it is the transition formula $x_{a}^{(i)} \mapsto x_{a}^{(j)} / x_{i}^{(j)}$ of the published charts of $P_{k}^{n}$ (Relative projective space from standard charts). For $n = 0$ the space is the one-point scheme $Spec k$ .

Facts & Assumptions

Given: The Axiom of Choice, A field $k$ , an integer $n \geq 0$ , the graded polynomial ring $S = k [x_{0}, \dots, x_{n}]$ with $\deg x_{i} = 1$ , and the scheme $P_{k}^{n}$ with its standard charts.

[F1]

$Proj k [x_{0}, \dots, x_{n}] ≅ P_{k}^{n}$ canonically over $Spec k$ , with $D_{+} (x_{i})$ corresponding to the $i$ -th standard chart $U_{i} = Spec k [x_{ℓ}^{(i)} : ℓ \neq i]$ and transition isomorphisms $x_{ℓ}^{(i)} \mapsto x_{ℓ}^{(j)} / x_{i}^{(j)}$ , $x_{j}^{(i)} \mapsto 1 / x_{i}^{(j)}$ on $U_{i} \cap U_{j}$ . (Projective space is Proj of a polynomial ring, Relative projective space from standard charts)

[F2]

For homogeneous $f \in S$ of positive degree the chart map $D_{+} (f) \to Spec S_{(f)}$ is an isomorphism of schemes. (Standard opens are affine)

[F3]

For a field $k$ the scheme $Spec k$ has exactly one point, namely $(0)$ . (The spectrum of a field is a one-point affine scheme)

[F4]

The assumed Axiom of Choice is the choice-function principle (The Axiom of Choice); it licenses the AC-qualified Proj and associated-sheaf suppliers at step 2.1.

Verification

technique · direct: compute the degree-zero localisations of the polynomial ring at the variables and match them with the published charts and transition formulas

1.1algebra

Chart coordinates. Fix $i$ . A degree-zero element of $S [x_{i}^{- 1}]$ has the form $a / x_{i}^{d}$ with $a$ homogeneous of degree $d$ , and every monomial $x_{0}^{a_{0}} \dots x_{n}^{a_{n}}$ of degree $d$ gives $x_{0}^{a_{0}} \dots x_{n}^{a_{n}} / x_{i}^{d} = \prod_{ℓ \neq i} (x_{ℓ} / x_{i})^{a_{ℓ}}$ ; hence $S_{(x_{i})} = k [x_{ℓ} / x_{i} : ℓ \neq i],$ the polynomial ring in the $n$ variables $x_{ℓ}^{(i)} : = x_{ℓ} / x_{i}$ .

2.1F1F2F4step 1.1

The charts. Under the assumed AC [F4], by [F2] the chart $D_{+} (x_{i})$ is $Spec S_{(x_{i})} = Spec k [x_{ℓ} / x_{i} : ℓ \neq i]$ , which is exactly the $i$ -th standard chart $U_{i} = Spec k [x_{ℓ}^{(i)} : ℓ \neq i]$ of $P_{k}^{n}$ under the identification $x_{ℓ}^{(i)} = x_{ℓ} / x_{i}$ of [F1].

2.2F1step 1.1algebra

The overlap. On $D_{+} (x_{i} x_{j})$ both $x_{i}$ and $x_{j}$ are invertible, so the relation $\frac{x_{a}}{x_{j}} = \frac{x_{a} / x_{i}}{x_{j} / x_{i}}$ is an identity of regular functions in the localised rings; expressed in the coordinates of step 1.1 it reads $x_{a}^{(j)} = x_{a}^{(i)} / x_{j}^{(i)}$ , which is exactly the transition formula of the published charts in [F1], together with $x_{i}^{(j)} = 1 / x_{j}^{(i)}$ for $a = i$ . Hence the overlapping charts are glued by the same isomorphisms.

2.3F1F3step 1.1cases: n=0

The case $n = 0$ . For $n = 0$ we have $S = k [x_{0}]$ with $S_{(x_{0})} = k$ by step 1.1 with $n = 0$ variables, so $Proj k [x_{0}] = D_{+} (x_{0}) = Spec k$ , which is the one-point scheme of [F3]; equivalently $P_{k}^{0} = Spec k$ in the published charts.

3.1

Conclusion. Steps 2.1 and 2.2 identify the charts and gluing of $Proj k [x_{0}, \dots, x_{n}]$ with those of $P_{k}^{n}$ , in agreement with the canonical isomorphism of [F1], and step 2.3 settles $n = 0$ ; the displayed coordinate change is the transition formula of the published charts. [F1, step 2.1, step 2.2, step 2.3] \qed

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

21 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, Constructions of Schemes, Sections 27.8-27.21 (standard reference, not scraped)
Ravi Vakil, The Rising Sea, 29 August 2022, Sections 4.5, 7.4, 9.3, 10.6, 17.4, 17.6, 18.2 (standard reference, not scraped)
Gao-Zhang, Lectures on Algebraic Geometry, Chapter 5 (standard reference, not scraped)