ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passaudited 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.

A projective hypersurface as a homogeneous quotient

Example

Let $k$ be a field, $n \geq 0$ and let $0 \neq F \in k [x_{0}, \dots, x_{n}]$ be homogeneous of degree $e \geq 1$ . Then $Proj (k [x_{0}, \dots, x_{n}] / (F)) = V_{+} (F) ↪ P_{k}^{n}$ is the closed subscheme of the projective space cut out by $F$ , and on the standard chart $D_{+} (x_{i})$ its coordinate ring is $k [x_{a} / x_{i} : a \neq i] / (F / x_{i}^{e}) .$ The description includes the degenerate cases: for $n = 0$ one has $F = c x_{0}^{e}$ with $c \neq 0$ and the chart ring $k / (c) = 0$ , so $V_{+} (F) = \emptyset$ .

Facts & Assumptions

Given: A field $k$ , an integer $n \geq 0$ , the graded polynomial ring $B = k [x_{0}, \dots, x_{n}]$ with $\deg x_{i} = 1$ , a nonzero homogeneous $F \in B$ of degree $e \geq 1$ , and the homogeneous principal ideal $I = (F) \subseteq B$ .

[A1]

The Axiom of Choice states that every family of nonempty sets has a choice function. (The Axiom of Choice)

[F1]

For a commutative ring $A$ , a homogeneous ideal $I \subseteq A [x_{0}, \dots, x_{n}]$ determines a closed subscheme $V_{+} (I) ↪ P_{A}^{n}$ whose intersection with the chart $D_{+} (x_{i})$ is $Spec (B_{(x_{i})} / I_{(x_{i})})$ , where $I_{(x_{i})} = (I [x_{i}^{- 1}])_{0}$ ; equivalently $V_{+} (I) = Proj (B / I)$ under the canonical closed immersion $Proj (B / I) \to Proj B = P_{A}^{n}$ . (Closed subschemes of projective space and saturated ideals)

[F2]

There is a canonical isomorphism $Proj A [x_{0}, \dots, x_{n}] ≅ P_{A}^{n}$ over $Spec A$ , and over the field $k$ the standard chart $D_{+} (x_{i})$ has coordinate ring $k [x_{a}^{(i)} : a \neq i]$ with $x_{a}^{(i)} = x_{a} / x_{i}$ . (Projective space is Proj of a polynomial ring, Closed subschemes of projective space and saturated ideals)

Verification

technique · direct: read the hypersurface off the homogeneous quotient theorem, compute the degree-zero localisation of the principal ideal at each chart variable, and identify the resulting equation with $F/x_i^{e}$

1.1A1F1F2

The quotient and the closed subscheme. Since $F$ is homogeneous, $I = (F)$ is a homogeneous ideal, so by [F1] the subscheme $V_{+} (I) ↪ P_{k}^{n}$ exists and equals $Proj (B / I) = Proj (k [x_{0}, \dots, x_{n}] / (F))$ ; by [F2] the ambient space $Proj B$ is $P_{k}^{n}$ with charts $D_{+} (x_{i})$ .

2.1F1F2step 1.1algebra

The chart ring. Fix $i$ . By [F2] the chart ring of $P_{k}^{n}$ on $D_{+} (x_{i})$ is $B_{(x_{i})} = k [x_{a}^{(i)} : a \neq i]$ with $x_{a}^{(i)} = x_{a} / x_{i}$ . In the localisation $B [x_{i}^{- 1}]$ the element $x_{i}$ is a unit and $F = x_{i}^{e} \cdot (F / x_{i}^{e})$ , so the ideal generated by $F$ is generated by the degree-zero element $F / x_{i}^{e}$ ; hence $I_{(x_{i})} = (I [x_{i}^{- 1}])_{0} = (F / x_{i}^{e})$ , and the chart ring of $V_{+} (I)$ on $D_{+} (x_{i})$ is $B_{(x_{i})} / I_{(x_{i})} = k [x_{a}^{(i)} : a \neq i] / (F / x_{i}^{e})$ , that is, $k [x_{a} / x_{i} : a \neq i] / (F / x_{i}^{\deg F})$ .

3.1

Conclusion and degenerate cases. Steps 1.1 and 2.1 identify $Proj (k [x_{0}, \dots, x_{n}] / (F))$ with $V_{+} (F) \subseteq P_{k}^{n}$ and compute its chart rings. If $F = c x_{i}^{e}$ is a nonzero multiple of a single coordinate power, then on the $i$ -th chart the equation is the unit $c$ and the chart ring is $k [x_{a}^{(i)}] / (c) = 0$ , so that chart meets $V_{+} (F)$ in the empty scheme; in particular for $n = 0$ one has $F = c x_{0}^{e}$ and $V_{+} (F) = Spec 0 = \emptyset$ , the empty hypersurface. If $F$ is not such a monomial then for every $i$ the element $F / x_{i}^{e}$ is the dehomogenisation of $F$ , a nonzero element of the polynomial ring $k [x_{a}^{(i)} : a \neq i]$ that is not a unit because some monomial of $F$ has a positive exponent at a variable other than $x_{i}$ ; each chart is then the genuine affine hypersurface $k [x_{a}^{(i)}] / (F / x_{i}^{e})$ , which is a nonzero ring. The zero polynomial is excluded by hypothesis. The Axiom of Choice [A1] is inherited from the affine quotient and gluing suppliers of [F1]; no choice is made here. [A1, F1, F2, step 1.1, step 2.1, cases: empty chart and n=0] \qed

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

12 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)