LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

Surface non pth power detected by derivation

Statement

Assume AC. Let $B$ be a domain of characteristic $p > 0$ finite type over a complete equicharacteristic Noetherian local ring, and let $f \in B$ not be a $p$ th power in $Frac B$ . There is a derivation $D : B \to B$ with $D (f) \neq 0$ .

Facts & Assumptions

Given: A domain $B$ of characteristic $p > 0$ , finite type over a complete equicharacteristic Noetherian local ring, and $f \in B$ that is not a $p$ th power in $Frac B$ .

[F1]

cor-complete-local-domain-finite-over-a-regular-power-series-ring. Assume the Axiom of Choice. Let $(A, m)$ be a complete equicharacteristic Noetherian local domain of dimension $d$ . Then there exists a coefficient field $k \subseteq A$ and an injective local homomorphism $k ⟦ X_{1}, \dots, X_{d} ⟧ ↪ A$ whose image is a regular complete local subring over which $A$ is module-finite. (A complete local domain is finite over a regular power-series ring)

[F2]

cor-noether-normalisation-module-finiteness. Let $k$ be a field and let $A$ be a nonzero finite-type $k$ -algebra. Then there exist algebraically independent elements $z_{1}, \dots, z_{d} \in A$ such that $A$ is a module-finite algebra over the polynomial ring $k [z_{1}, \dots, z_{d}]$ . (Noether normalisation yields module finiteness over a polynomial subring)

[F3]

def-axiom-of-choice. The Axiom of Choice (AC) is the following statement. > Every family of nonempty sets has a choice function > (def-choice-function). Written out: for every set $F$ all of whose members are nonempty, there exists a function $g$ with domain $F$ satisfying $g (S) \in S$ for all $S \in F$ . (The Axiom of Choice)

[F4]

def-dependent-choice. Let $X$ be a set and let $R \subseteq X \times X$ be a binary relation on $X$ . Call $R$ entire on $X$ when $for every x \in X there is y \in X with x R y .$ The Axiom of Dependent Choice, written $D C$ , is the following statement. (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain)

[F5]

def-derivation-algebra. Let $A \overset{φ}{\to} B$ be a homomorphism of commutative rings (def-commutative-ring), so that $B$ is an $A$ -algebra, and let $M$ be a $B$ -module (def-left-and-right-modules). (Derivation of an algebra)

[F6]

def-kahler-differentials-algebra. Let $A \overset{φ}{\to} B$ be a homomorphism of commutative rings and let ${Der}_{A} (B, -)$ be the derivation functor of Derivation of an algebra. (Universal Kähler differential module)

[F7]

lem-surface-p-basis-subfield-separation. Assume AC. Let $k$ have characteristic $p > 0$ , $A = k [⁣ [X_{1}, \dots, X_{n}] ⁣] [Y_{1}, \dots, Y_{m}]$ and $K = Frac A$ . Choose a possibly infinite $p$ -basis $(b_{i})_{i \in I}$ of $k / k^{p}$ , meaning its restricted monomials of finite support form a $k^{p}$ -basis. (Surface p basis subfield separation)

Proof

1.1F1F2given

Replacing the base by its image gives a complete local domain, which is finite over a regular power-series subring; generic Noether normalisation then produces a polynomial subring $R [Y] \subseteq B^{'} \subseteq B$ with $B^{'}$ finite over $R [Y]$ and $B_{g}^{'} = B_{g}$ for a nonzero $g \in R$ , obtained by normalising over $Frac (R)$ and clearing the finitely many monic equations of the algebra generators by multiplying them by powers of $g$ .

2.1F6F7step 1.1

In $L = Frac (B^{'})$ the differential $d f$ is nonzero: the kernel of the universal absolute derivation is the subfield $L^{p}$ , so a nonzero $d f$ is exactly the statement that $f$ is not a $p$ th power, which is preserved when $f$ is multiplied by the $p$ th power $g^{p N}$ used to move it into $B^{'}$ .

3.1F5F7step 2.1

Apply the separation lemma to $f \notin L^{p} = ⋂_{J} L^{p} K_{J}$ to choose $J$ with $f \notin L^{p} K_{J}$ . A finite relative $p$ -basis of $L$ over $L^{p} K_{J}$ has restricted monomials as a basis; its coordinate derivations show that the kernel of $d : L \to Ω_{L / K_{J}}$ is exactly $L^{p} K_{J}$ . Thus $d f \neq 0$ in that finite-dimensional differential space; a linear functional on the finite-dimensional differential space nonzero on $d f$ then defines a $K_{J}$ -derivation of $L$ with nonzero value on $f$ . Clearing denominators of its values on finitely many $A_{J}$ -module generators of $B^{'}$ produces a derivation $D^{'} ⁣ : B^{'} \to B^{'}$ .

4.1F3F4F5step 3.1∎

Derivations extend through localization by the quotient rule, and multiplying $D^{'}$ by $g^{N + 1}$ , where $g^{N}$ times each $B^{'}$ -algebra generator of $B$ lies in $B^{'}$ , gives a derivation $B \to B$ ; the initial multiplier $g^{p N}$ has zero derivative, so the resulting derivation still satisfies $D (f) \neq 0$ , as required. The Axiom of Choice and the Axiom of Dependent Choice are inherited from the normalisation and derivation suppliers.

Remarks

The proof tracks a single element f through the normalisation and the p-basis separation; no statement about derivations of the whole ring is assumed.
The multiplier g^{pN} is invisible to derivations and is used only to move f into the finite subalgebra.

Depends on

Used by

Dependency tree · two levels

19 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: full proof imports for normal-surface resolution, lemma-find-D, lemma-derivation-extends (standard reference, not scraped)
Stacks Lemma 15.49.5 (07PH), complete detecting-derivation proof (standard reference, not scraped)