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

Geometric parameters of a projection of affine spaces

Example

Let $k$ be a field and let $π ⁣ : A_{k}^{m + n} \to A_{k}^{m}$ be the projection onto the first $m$ coordinates, with $m, n \geq 0$ . Write the coordinate ring of the source as $k [y_{1}, \dots, y_{m}, x_{1}, \dots, x_{n}] = k [y_{1}, \dots, y_{m}] [x_{1}, \dots, x_{n}]$ . Then:

$π$ is standard smooth in the chart $g = 1$ with $c = 0$ equations and relative dimension $n$ , the polynomial extension being its own presentation;
at every $k$ -rational point $(a, b)$ of the source the pulled-back classes of $y_{1} - a_{1}, \dots, y_{m} - a_{m}$ are $k$ -linearly independent in the cotangent space $m_{(a, b)} / m_{(a, b)}^{2}$ , being the first $m$ elements of the coordinate cotangent basis;
every fibre of $π$ over a $k$ -rational point is $A_{k}^{n}$ , of dimension $n$ .

The calculation is an explicit polynomial computation; no form of the Axiom of Choice is introduced, and the quoted dimension statement carries no Choice hypothesis.

Facts & Assumptions

Given: A field $k$ , integers $m, n \geq 0$ , the polynomial rings $k [y_{1}, \dots, y_{m}]$ and $k [y_{1}, \dots, y_{m}, x_{1}, \dots, x_{n}]$ , and a $k$ -rational point $(a, b) = (a_{1}, \dots, a_{m}, b_{1}, \dots, b_{n})$ of $A_{k}^{m + n}$ .

[F1]

Standard smooth presentations and locally standard smooth maps: a standard smooth presentation of an $R$ -algebra $S$ consists of $n \geq c \geq 0$ , equations $f_{1}, \dots, f_{c}$ and an element $g$ with $S ≅ (R [x_{1}, \dots, x_{n}] / (f_{1}, \dots, f_{c}))_{g}$ such that some $c \times c$ Jacobian minor is a unit of $S$ ; the relative dimension is $n - c$ , and $c = 0$ is allowed, in which case $S$ is a localisation of a polynomial ring over $R$ and no minor condition is imposed.

[F2]

Differentials of a polynomial quotient and the Jacobian cokernel: for $A = k [y_{1}, \dots, y_{m}]$ and $P = A [x_{1}, \dots, x_{n}]$ the module $Ω_{P / A}$ is free with basis $d x_{1}, \dots, d x_{n}$ ; over $k$ the module $Ω_{k [y, x] / k}$ is free with basis $d y_{1}, \dots, d y_{m}, d x_{1}, \dots, d x_{n}$ .

[F3]

Separable residue and the cotangent sequence of a local algebra: for a Noetherian local $k$ -algebra $R$ with residue field $κ$ finite separable over $k$ , the map $m / m^{2} \to Ω_{R / k} \otimes_{R} κ$ sending the class of $z$ to $d z \otimes 1$ is an isomorphism; in particular at a $k$ -rational point of a polynomial ring the classes of the coordinate differences form a $k$ -basis of the cotangent space.

[F4]

Universal mapping property of the tensor product of commutative algebras, Tensoring is right exact: $k [y, x] \otimes_{k [y]} κ (a) ≅ k [x]$ for the quotient $k [y] / (y_{1} - a_{1}, \dots, y_{m} - a_{m}) ≅ k$ presenting the residue field of the $k$ -rational point $a$ , and base change commutes with quotients.

[F5]

A polynomial ring in n variables over a field has dimension n: $\dim k [x_{1}, \dots, x_{n}] = n$ for $n \geq 0$ , with $\dim k = 0$ when $n = 0$ .

Proof

1.1

The standard smooth chart. The source coordinate ring is the polynomial ring $k [y_{1}, \dots, y_{m}] [x_{1}, \dots, x_{n}]$ , and the map $k [y_{1}, \dots, y_{m}] \to k [y] [x]$ is the structure map of the target algebra over itself, presented by $n$ variables, no equations ( $c = 0$ ) and $g = 1$ ; by [F1] this is a standard smooth presentation of relative dimension $n - 0 = n$ , so $π$ is standard smooth in this single chart, with no minor to check.

F1algebra

1.2

The cotangent parameters. At the $k$ -rational point $(a, b)$ the residue field is $k$ , so [F3] identifies the cotangent space with $Ω_{k [y, x] / k} \otimes k$ , which by [F2] has the $k$ -basis $d y_{1}, \dots, d y_{m}, d x_{1}, \dots, d x_{n}$ and hence the classes of the coordinate differences $y_{i} - a_{i}$ , $x_{j} - b_{j}$ as its $k$ -basis. The pullback map on cotangent spaces induced by $π$ sends the class of $y_{i} - a_{i}$ to the class of $π^{#} (y_{i} - a_{i}) = y_{i} - a_{i}$ , that is, it carries the basis $d y_{1}, \dots, d y_{m}$ of the target cotangent space onto the first $m$ elements of a basis of the source cotangent space; in particular these classes are $k$ -linearly independent.

F2F3algebra

2.1

The fibres. Let $a \in A_{k}^{m} (k)$ be a $k$ -rational point and let $I = (y_{1} - a_{1}, \dots, y_{m} - a_{m}) \subseteq k [y]$ be its maximal ideal, with $k [y] / I ≅ k$ . By [F4] the fibre ring is $k [y, x] \otimes_{k [y]} k ≅ k [y, x] / I k [y, x] ≅ k [x_{1}, \dots, x_{n}]$ , so the fibre over $a$ is $Spec k [x_{1}, \dots, x_{n}] = A_{k}^{n}$ and has dimension $n$ by [F5]; equivalently the fibre of $π$ over any $k$ -rational point is affine $n$ -space. This completes the verification of all three clauses, and the fibre dimension $n$ is exactly the relative dimension of the chart of step 1.1, while the target's $m$ coordinate parameters pull back to independent cotangent classes by step 1.2.

F4F5step 1.1step 1.2algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

26 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

Stacks Algebra 10.137.5 (tag 00T6) and 10.140.5 (tag 00TV) (standard reference, not scraped)
Vakil §26.2.F, pp.690–693 (standard reference, not scraped)