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 graph of a polynomial map as a closed subscheme

Example

Let $k$ be a field, let $m, n \geq 0$ , and let $g : A_{k}^{m} \to A_{k}^{n}$ be given by polynomials $g_{1}, \dots, g_{n} \in k [x_{1}, \dots, x_{m}]$ . Then the graph $Γ_{g} : A_{k}^{m} \to A_{k}^{m} \times_{k} A_{k}^{n}$ is a closed immersion, and after identifying $A_{k}^{m} \times_{k} A_{k}^{n} = Spec k [x_{1}, \dots, x_{m}, y_{1}, \dots, y_{n}]$ its ideal is $(y_{1} - g_{1} (x), \dots, y_{n} - g_{n} (x)) .$ Moreover the first projection restricts to an isomorphism $Γ_{g} \to A_{k}^{m}$ with inverse $Γ_{g}$ , so the graph is a closed subscheme isomorphic to the source through ${pr}_{1}$ .

Facts & Assumptions

Given: A field $k$ , integers $m, n \geq 0$ , the affine spaces $A_{k}^{m} = Spec k [x_{1}, \dots, x_{m}]$ and $A_{k}^{n} = Spec k [y_{1}, \dots, y_{n}]$ over $Spec k$ , and the morphism $g$ with coordinate polynomials $g_{1}, \dots, g_{n}$ .

[F1]

For an $S$ -morphism $u : X \to Y$ the graph morphism is the $S$ -morphism $Γ_{u} = ({id}_{X}, u) : X \to X \times_{S} Y$ ; its composites with the two projections are ${id}_{X}$ and $u$ , and the definition alone does not assert that its image is closed. (The graph morphism over a base)

[F2]

If $Y \to S$ is separated and $u : X \to Y$ is an $S$ -morphism, then $Γ_{u}$ is a closed immersion. (Closed graphs over separated targets)

[F3]

Every affine morphism is separated. (Affine morphisms are separated)

[F4]

For ring maps $k \to B$ , $k \to C$ one has $Spec B \times_{Spec k} Spec C ≅ Spec (B \otimes_{k} C)$ , with projections $b \mapsto b \otimes 1$ and $c \mapsto 1 \otimes c$ . (Affine fibre products are spectra of tensor products)

[F5]

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)

Verification

1.1

The structure morphism $A_{k}^{n} \to Spec k$ is affine, hence separated by [F3], so [F2] applies to the $Spec k$ -morphism $g$ and the graph $Γ_{g}$ is a closed immersion. By [F4] the product is $Spec (k [x] \otimes_{k} k [y]) = Spec k [x_{1}, \dots, x_{m}, y_{1}, \dots, y_{n}]$ , with ${pr}_{1}$ acting as $x_{i} \mapsto x_{i}$ and ${pr}_{2}$ as $y_{j} \mapsto y_{j}$ .

F2F3F4

2.1

Under the identification of step 1.1 the morphism $Γ_{g} = (id, g)$ corresponds to the $k$ -algebra map $φ : k [x, y] \to k [x]$ with $φ (x_{i}) = x_{i}$ and $φ (y_{j}) = g_{j} (x)$ .

F1step 1.1

3.1

The map $φ$ is surjective and its kernel is the ideal $I = (y_{1} - g_{1} (x), \dots, y_{n} - g_{n} (x))$ : clearly $I \subseteq \ker φ$ , and conversely if $f \in \ker φ$ then writing $f$ as a polynomial in the variables $u_{j} = y_{j} - g_{j} (x)$ with coefficients in $k [x]$ gives $f \equiv f (x, g (x)) = 0$ modulo $I$ , so $f \in I$ .

step 2.1algebra

4.1

By [F5] the closed subscheme with ideal $I$ is, up to unique isomorphism over the product, the image of $φ$ , so the graph is the closed subscheme $V (I)$ of $Spec k [x, y]$ with the displayed ideal.

F5step 3.1

4.2

By [F1] the composite ${pr}_{1} \circ Γ_{g}$ is the identity of $A_{k}^{m}$ , so the first projection restricts to a morphism $Γ_{g} \to A_{k}^{m}$ with inverse $Γ_{g}$ ; hence ${pr}_{1} ∣_{Γ_{g}}$ is an isomorphism. In coordinate rings this is the isomorphism $k [x, y] / I \to k [x]$ inverse to $φ$ .

F1step 3.1

4.3

The degenerate cases are included: for $n = 0$ the list of equations is empty, $I = 0$ , and the graph is the identity of $A_{k}^{m}$ ; for $m = 0$ the source is a single $k$ -rational point and the graph is the closed point $(g_{1}, \dots, g_{n}) \in A_{k}^{n}$ cut out by $y_{j} - g_{j}$ .

step 2.1step 3.1

5.1

Steps 1.1, 4.1 and 4.2 show that $Γ_{g}$ is a closed subscheme of $A_{k}^{m} \times_{k} A_{k}^{n}$ with ideal $(y_{1} - g_{1} (x), \dots, y_{n} - g_{n} (x))$ whose first projection is an isomorphism onto $A_{k}^{m}$ , which is the assertion.

step 1.1step 4.1step 4.2∎

Remarks

The fibre-product page already records the calculation of this ideal, with the roles of the two factors exchanged, as The ideal of a polynomial graph. The present item adds the identification of the abstract graph morphism of The graph morphism over a base with that closed subscheme and the statement that the first projection restricts to an isomorphism; no separate computation is needed for the ideal itself.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

20 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.10, printed p.42 (standard reference, not scraped)
Ravi Vakil, The Rising Sea, Proposition 11.3.6, printed p.309 (standard reference, not scraped)