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.

Differentials of k[x,y]

Example

Let $k$ be a commutative ring and let $P = k [x, y]$ be the polynomial algebra on the two indeterminates $x, y$ . Then $Ω_{P / k} = P d x \oplus P d y,$ the free $P$ -module on the two differentials, and for all integers $a, b \geq 0$ $d (x^{a} y^{b}) = a x^{a - 1} y^{b} d x + b x^{a} y^{b - 1} d y,$ where the integer coefficients $a$ and $b$ are read in $k$ through the ring map $Z \to k$ , and where a term with exponent $0$ is read as $0$ (for $a = 0$ the $x$ -term is $0$ , and for $b = 0$ the $y$ -term is $0$ ). Since $k$ need not have characteristic $0$ , an integer coefficient can vanish: if $k$ has characteristic $p$ and $p ∣ a$ , the class $a \in k$ is $0$ and the $d x$ -coefficient of $d (x^{a})$ vanishes.

Facts & Assumptions

Given: A commutative ring $k$ , the polynomial algebra $P = k [x, y]$ over $k$ , the derivations $\partial / \partial x$ and $\partial / \partial y$ of $P$ that are $k$ -linear, and the integers $a, b \geq 0$ .

[F1]

Polynomial differentials are free with $n = 2$ : $Ω_{P / k}$ is a free $P$ -module with basis $d x, d y$ ; the derivations $\partial / \partial x, \partial / \partial y$ satisfy $\partial x / \partial x = 1$ , $\partial y / \partial x = 0$ , $\partial x / \partial y = 0$ , $\partial y / \partial y = 1$ ; and for every $f \in P$ one has $d f = (\partial f / \partial x) d x + (\partial f / \partial y) d y$ .

[F2]

Derivation of an algebra: a $k$ -derivation $D ⁣ : P \to M$ into a $P$ -module $M$ is additive, satisfies the Leibniz rule $D (f g) = f D (g) + g D (f)$ , and annihilates $k$ , that is $D (c) = 0$ for every $c \in k$ ; in particular $D (1) = 0$ .

Verification

1.1

By [F1] the module $Ω_{P / k}$ is free with basis $d x, d y$ over $P$ , and $d f = (\partial f / \partial x) d x + (\partial f / \partial y) d y$ for every $f \in P$ .

F1given

1.2

We compute the partial derivatives of the powers of the variables: $\partial (x^{n}) / \partial x = n x^{n - 1}$ for every $n \geq 0$ , where the case $n = 0$ reads $\partial (1) / \partial x = 0$ , and $\partial (y^{m}) / \partial x = 0$ for every $m \geq 0$ . Indeed, $\partial (1) / \partial x = 0$ because $1 \in k$ is annihilated by a $k$ -derivation [F2], and if $\partial (x^{n - 1}) / \partial x = (n - 1) x^{n - 2}$ then the Leibniz rule [F2] and $\partial x / \partial x = 1$ [F1] give $\partial (x^{n}) / \partial x = \partial (x \cdot x^{n - 1}) / \partial x = x^{n - 1} + x (n - 1) x^{n - 2} = n x^{n - 1}$ ; the same induction with $\partial y / \partial x = 0$ gives $\partial (y^{m}) / \partial x = 0$ . Interchanging the roles of $x$ and $y$ gives $\partial (x^{n}) / \partial y = 0$ and $\partial (y^{m}) / \partial y = m y^{m - 1}$ .

F1F2induction

2.1

Multiplying out with the Leibniz rule: $\partial (x^{a} y^{b}) / \partial x = y^{b} \partial (x^{a}) / \partial x + x^{a} \partial (y^{b}) / \partial x = a x^{a - 1} y^{b}$ , the term being $0$ when $a = 0$ , and likewise $\partial (x^{a} y^{b}) / \partial y = x^{a} \partial (y^{b}) / \partial y = b x^{a} y^{b - 1}$ , the term being $0$ when $b = 0$ .

step 1.2F2

3.1

Substituting step 2.1 into the formula of step 1.1 gives $d (x^{a} y^{b}) = a x^{a - 1} y^{b} d x + b x^{a} y^{b - 1} d y$ for all $a, b \geq 0$ , with the integer coefficients evaluated in $k$ : if $k$ has characteristic $p$ and $p ∣ a$ , then $a = 0$ in $k$ and the $d x$ -term vanishes, while the class $x^{a - 1} y^{b}$ remains meaningful for $a \geq 1$ and the case $a = 0$ is handled as $0$ . Since $d x, d y$ form a basis of the free module $Ω_{P / k}$ , the formula determines $d$ on every monomial and, by additivity and $k$ -linearity of the universal derivation, on all of $P$ ; in particular $d x$ and $d y$ are $k$ -linearly independent elements of $Ω_{P / k}$ .

step 1.1step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

6 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.131.14 (standard reference, not scraped)
Vakil 22.2.3, p.575 (standard reference, not scraped)