LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Degree-p inseparable extensions of complete regular surfaces have bounded H1

Statement

Assume AC and DC. Let $A = k [⁣ [u, v] ⁣]$ have characteristic $p > 0$ , let $L / K$ be a purely inseparable degree- $p$ extension of its fraction field, and let $B$ be the finite normalization of $A$ in $L$ . Then normal modification H1 over $B$ is uniformly bounded.

Facts & Assumptions

Given: The complete regular surface $A = k [⁣ [u, v] ⁣]$ of characteristic $p > 0$ , a purely inseparable degree- $p$ extension $L / K$ of its fraction field, and the finite normalization $B$ of $A$ in $L$ .

[F1]

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)

[F2]

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)

[F3]

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. For finite $J \subset I$ put $k_{J} = k^{p} (b_{i} : i \notin J)$ , $A_{J} = k_{J} [⁣ [X_{1}^{p}, \dots, X_{n}^{p}] ⁣] [Y_{1}^{p}, \dots, Y_{m}^{p}]$ and $K_{J} = Frac A_{J}$ . Then $A$ is finite free over $A_{J}$ , the family $(K_{J})$ is downward directed with intersection $K^{p}$ , and for every finite field extension $L / K$ , $⋂_{J} L^{p} K_{J} = L^{p}$ . (Surface p basis subfield separation)

[F4]

lem-degree-p-inseparable-differential-trace-extends-on-normal-surfaces. Assume AC and DC. Let $S$ be a scheme and let $Y \overset{π}{\to} X$ be a finite dominant $S$ -morphism of normal integral Noetherian schemes of characteristic $p$ whose function fields have purely inseparable degree $p$ . If $Ω_{X / S}$ is coherent, then for $q \geq 1$ the generic differential trace extends canonically to $π_{*} \land^{q} Ω_{Y / S} \to (\land^{q} Ω_{X / S})^{* *}$ . For a monogenic algebra $B = A [z] / (z^{p} - f)$ it kills forms pulled back from $A$ and sends $η \land z^{i} d z$ to zero for $i < p - 1$ and to $η \land d f$ for $i = p - 1$ . (Degree-p differential trace extends across normal surface valuations)

[F5]

lem-finite-closed-immersion-derived-coinduction-adjunction. Assume AC. For a finite homomorphism $A \to B$ of Noetherian rings and $G \in D^{+} (A)$ , the complex $f^{!} G = R {Hom}_{A} (B, G)$ has its natural $B$ -action and is right adjoint to restriction of scalars. (Derived adjunction for finite rings and closed immersions)

[F6]

lem-finite-domination-of-surface-modifications-via-relative-hilbert-scheme. Assume AC and DC. Let $A$ be a normal Noetherian local domain of dimension two essentially of finite type over a field or a complete equicharacteristic Noetherian local ring. Let $B$ be a finite normal local $A$ -domain, and let $Y \to Spec B$ be a normal integral modification. (Finite domination of surface modifications by a relative Hilbert scheme)

[F7]

lem-positive-characteristic-top-differentials-map-to-blown-up-canonical-module. Assume AC and DC. Let $A$ be a regular local surface of characteristic $p$ , and let $A_{0} \subset A$ have coherent differential module $Ω_{A / A_{0}}$ free of finite rank $r$ . Choose $ω_{A} = \land^{r} Ω_{A / A_{0}}$ . Every finite sequence of regular point blowups $X \to Spec A$ has a generic-compatible map $(\land^{r} Ω_{X / A_{0}})^{* *} \to ω_{X}$ . (Top differential lattices map into point-blowup canonical modules)

[F8]

lem-regular-base-dualizing-traces-compose-on-rational-modifications. Assume AC and DC. Let $R$ be regular local of dimension two, $A$ finite normal local over $R$ , and let $g : X^{'} \to X$ be a morphism of projective normal modifications over $A$ . Their regular-base dualizing complexes are independent of the chosen projective embeddings up to the unique isomorphism preserving their duality pairings. (Dualizing traces compose and become isomorphisms on rational modifications)

[F9]

lem-normal-surface-trace-cokernel-dualizes-h1-and-bounds-it. Assume AC and DC. Let $R$ be regular local of dimension two and $A$ a finite normal local $R$ -domain in the permitted class. For a projective normal modification $X$ , put $M = H^{1} (X, O_{X})$ . (Trace cokernels detect and bound normal surface H1)

[F10]

lem-normal-surface-modification-leray-short-exact-sequence. Assume AC and DC. Let $A$ be a normal local domain of dimension two in the field/complete-equicharacteristic finite-type class, and $X^{'} \overset{g}{\to} X \to Spec A$ normal integral modifications. Then $g_{*} O_{X^{'}} = O_{X}$ and $H^{1} (X, O_{X}) \to H^{1} (X^{'}, O_{X^{'}})$ is injective. (The Leray sequence for normal surface modifications)

[F11]

lem-surface-finite-type-normalization-finite. Assume AC and DC. Every integral finite-type algebra over a field or a complete equicharacteristic Noetherian local base has finite normalization, and so do its localizations. Integral schemes of finite type over these bases consequently have finite scheme normalization. (Surface finite type normalization finite)

[F12]

lem-normal-projective-surface-dualizing-module-over-regular-local-base. Assume AC and DC. Let $R$ be a regular Noetherian local ring of dimension two, let $A$ be a finite normal local $R$ -domain of dimension two, with $R ↪ A$ local, and let $X$ be a normal integral scheme of dimension two projective over $R$ , with a proper birational map $f : X \to Spec A$ . Put $ω_{A} = {Hom}_{R} (A, R)$ . (Dualizing modules and trace pairing for normal projective surface modifications)

Proof

1.1F2F3given

Choose $z \in L$ with $L = K (z)$ and $z^{p} = f \in A$ after scaling to clear denominators; then $f \notin K^{p}$ , since otherwise $z \in K$ . Let $(b_{i})_{i \in I}$ be the $p$ -basis in [F3]. For finite $J \subset I$ , write $A_{J} = k_{J} [⁣ [u^{p}, v^{p}] ⁣]$ and $K_{J} = Frac A_{J}$ . The helper gives $⋂_{J} L^{p} K_{J} = L^{p}$ and $⋂_{J} K_{J} = K^{p}$ . If $f$ belonged to every $K_{J}$ , then $L^{p} K_{J} = K_{J}$ for every $J$ because $L^{p} = K^{p} (f)$ ; this would force $L^{p} = K^{p}$ , a contradiction. Choose $J$ with $f \notin K_{J}$ . The finite-free monomial basis of $A$ over $A_{J}$ gives $Ω_{A / A_{J}}$ the free basis ${d b_{i} : i \in J} \cup {d u, d v}$ , so its rank is $r = ∣ J ∣ + 2$ . Since $K / K_{J}$ has exponent one and $f \notin K_{J}$ , $d f \neq 0$ in $Ω_{K / K_{J}}$ , hence in the free module $Ω_{A / A_{J}}$ . Choose a basis coordinate of $d f$ with nonzero coefficient and let $η$ be the wedge of the other $r - 1$ basis elements; then $θ = η \land d f \neq 0$ in $ω_{A} = \land^{r} Ω_{A / A_{J}}$ . Set $A_{0} = A_{J}$ and let $z \in B$ be the image of the chosen generator.

2.1F4F5F12step 1.1

At the generic point $L = K [z] / (z^{p} - f)$ , so the degree- $p$ differential-trace formula [F4] gives $Tr (z^{j} α_{i}) = δ_{i j} θ$ for $α_{i} = η \land z^{p - 1 - i} d z$ and $0 \leq i, j < p$ . The chosen $z$ is integral, hence lies in $B$ , so every $α_{i}$ is a global section of $\land^{r} Ω_{B / A_{0}}$ . Finite coinduction identifies the trace map with $c ⁣ : \land^{r} Ω_{B / A_{0}} \to ω_{B} = {Hom}_{A} (B, ω_{A})$ , $α \mapsto (b \mapsto Tr (b α))$ ; since $1, z, \dots, z^{p - 1}$ is a $K$ -basis of $L$ , the displayed formula makes $c$ an isomorphism generically between rank-one $B$ -modules. Its coherent cokernel is therefore torsion and is killed by a fixed nonzero $d \in B$ .

3.1F6F11givenstep 2.1

For an arbitrary normal projective modification $Y$ of $B$ , the regular specialization of finite domination produces a normal integral modification $Y^{'} \to Y$ that is finite over a regular point-blowup modification $X$ of $Spec A$ , with $X$ and $Y^{'}$ projective over $A$ and all normalizations finite.

4.1F4F5F7F8F12step 2.1step 3.1

Write $π : Y^{'} \to X$ and $Q = \land^{r} Ω_{Y^{'} / A_{0}}$ . Apply [F4] over $Spec A_{0}$ and compose with [F7] to obtain an $O_{X}$ -linear map $τ : π_{*} Q \to ω_{X}$ . Finite coinduction [F5] turns it into the $O_{Y^{'}}$ -linear map $Q \to π^{!} ω_{X}$ , given on an affine chart by $α \mapsto (b \mapsto τ (b α))$ . Here $π^{!} ω_{X} = ω_{Y^{'}}$ : finite adjunction with $D_{X} = ω_{X} [2]$ gives the regular-base duality pairing on $Y^{'}$ , so the pairing uniqueness in [F8] and the concentration in [F12] identify $π^{!} D_{X}$ with $D_{Y^{'}}$ . Taking degree $- 2$ gives the stated module identification. Generically this map is exactly $c$ of step 2.1, with the same functional formula.

5.1F8F9F12step 2.1step 4.1

Forms pulled back from $B$ are global forms on $Y^{'}$ , and the map in step 4.1 sends them to global sections of $ω_{Y^{'}}$ whose trace to $ω_{B}$ equals $c$ generically and hence everywhere, since $ω_{B}$ is torsion-free. Thus that trace image contains $c (\land^{r} Ω_{B / A_{0}})$ and its cokernel is killed by the fixed nonzero $d$ . Trace composition [F8] for $Y^{'} \to Y \to Spec B$ makes this image a submodule of the trace image from $Y$ , so $d$ also kills the trace cokernel of every original normal projective modification $Y$ .

6.1F9F10step 5.1

The trace-cokernel criterion, applied with regular base $A$ and finite normal local domain $B$ , converts annihilation of every trace cokernel by the fixed nonzero $d$ into a uniform bound on the length of $H^{1}$ of normal modifications over $B$ ; the Leray short exact sequence injects $H^{1} (Y, O_{Y})$ into $H^{1} (Y^{'}, O_{Y^{'}})$ , so the bound is inherited by the arbitrary modification $Y$ and normal modification H1 over $B$ is uniformly bounded.

7.1F1F2step 6.1∎

The Axiom of Choice and the Axiom of Dependent Choice are inherited from the cited resolution, duality and normalization suppliers, and no ordinary field trace is substituted for the differential trace.

Remarks

The fixed element $d$ is produced by the finite presentation of the degree- $p$ extension and is independent of the modification.
The differential trace is essential in characteristic $p$ where the ordinary field trace vanishes.

Depends on

Used by

Dependency tree · two levels

71 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, Resolution of Surfaces, Sections 54.8–54.9: complete source arguments with local prerequisite replacements (standard reference, not scraped)