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 complete equicharacteristic finite integral closure

Statement

Assume AC. The integral closure of a complete equicharacteristic Noetherian local domain in every finite extension of its fraction field is a finite module.

Facts & Assumptions

Given: A complete equicharacteristic Noetherian local domain $A$ with fraction field $K$ , and a finite field extension $L / K$ .

[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-localisations-of-regular-local-rings-are-regular. Assume the Axiom of Choice (The Axiom of Choice). Every prime localization $R_{p}$ of a regular local ring $R$ is regular, and $edim R_{p} = ht p$ . (localisations of regular local rings are regular)

[F3]

cor-serre-normality-criterion-two-directions. Assume the Axiom of Choice (The Axiom of Choice). A commutative Noetherian domain is normal if and only if it satisfies $(R_{1})$ and $(S_{2})$ . Equivalently its integral closedness is characterized by these two conditions. (serre normality criterion two directions)

[F4]

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)

[F5]

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)

[F6]

lem-surface-non-pth-power-detected-by-derivation. 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$ . (Surface non pth power detected by derivation)

[F7]

lem-trace-pairing-for-a-finite-separable-extension. Let $L / F$ be a finite separable field extension. Then the bilinear pairing $L \times L \to F$ , $(x, y) \mapsto {Tr}_{L / F} (x y)$ , is nondegenerate. (The trace pairing in a finite separable extension is nondegenerate)

[F8]

thm-regular-local-rings-are-domains-and-cohen-macaulay. Assume the Axiom of Choice (The Axiom of Choice). A regular local ring $R$ of dimension $d$ is a domain and Cohen–Macaulay. For every regular system $(x_{1}, \dots, x_{d})$ , the tuple is $R$ -regular and $R / (x_{1}, \dots, x_{c})$ is regular local of dimension $d - c$ for all $0 \leq c \leq d$ . (regular local rings are domains and cohen macaulay)

Proof

1.1F1F2F3F8given

Choose a finite regular power-series subring $R$ over which $A$ is finite; $R$ is regular and Cohen--Macaulay, and the Serre criterion makes it normal because it and all its prime localizations are regular and Cohen--Macaulay.

2.1F7F8step 1.1

For a finite separable extension of $Frac (R)$ , choose an integral power basis and use the nondegenerate trace pairing: traces of products of integral elements are integral and lie in the fraction field of $R$ , hence in the normal ring $R$ , and inverting one discriminant places every integral element inside a single finite $R$ -module.

3.1F6step 1.1step 2.1

In characteristic $p$ , pass to a finite normal envelope and its maximal purely inseparable subextension. At a degree- $p$ step, let $B$ be the preceding normal finite Noetherian $R$ -algebra and let $L = Frac (B) [z] / (z^{p} - b)$ with $b \in B$ not a $p$ th power; the detecting-derivation lemma gives $D ⁣ : B \to B$ with $D (b) \neq 0$ .

4.1F6F8step 3.1algebra

Put $c = D (b) \neq 0$ . Induct on $i < p$ to show that an integral $u = \sum_{j = 0}^{i} a_{j} z^{j}$ has $c^{i} a_{j} \in B$ for every $j$ . For $i = 0$ this is normality of $B$ . For $i > 0$ , normality gives $u^{p} \in B$ , and $v = \sum_{j = 1}^{i} j c a_{j} z^{j - 1}$ satisfies $v^{p} = c^{p - 1} D (u^{p}) \in B$ , so $v$ is integral. The induction hypothesis gives $j c^{i} a_{j} \in B$ for $1 \leq j \leq i$ ; these $j$ are units in characteristic $p$ . Subtracting those integral terms from $c^{i} u$ makes $c^{i} a_{0}$ integral and in $Frac B$ , hence in $B$ . Taking $i = p - 1$ places every integral element in the finite $B$ -module $\sum_{j < p} B c^{- (p - 1)} z^{j}$ ; its integral closure is a submodule and is finite because $B$ is Noetherian.

5.1F4F5F7step 2.1step 4.1∎

Separable trace finiteness applied to the normal envelope, together with the degree- $p$ induction, shows that the integral closure in $L$ is a finite $R$ -module; the integral closure of the original domain in the intermediate field is a submodule of that finite closure, and transitivity of integrality identifies it with the closure of $R$ , so it is finite as required. The Axiom of Choice and the Axiom of Dependent Choice are inherited from the cited suppliers.

Remarks

The inseparable induction uses the pth-power derivative computation to bound integral elements by the module generated by the powers of z; no Tate or mixed characteristic input is needed.
The separable case is handled by the discriminant of the trace pairing; the two cases together cover every finite extension.

Depends on

Used by

Dependency tree · two levels

36 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-Noetherian-normal-domain-insep-extension, lemma-Noetherian-normal-domain-finite-separable-extension, lemma-domain-char-p-N-1-2 (standard reference, not scraped)