LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-04

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.

Parameters make a complete local domain finite over the image of a power-series map

Statement

Assume the Axiom of Dependent Choice.

Let $(A, m)$ be a complete equicharacteristic Noetherian local domain of dimension $d$ , let $k \subseteq A$ be a coefficient field, and let $x_{1}, \dots, x_{d}$ be a system of parameters. Then the continuous map $ϕ : k ⟦ X_{1}, \dots, X_{d} ⟧ \to A, X_{i} \mapsto x_{i},$ has image $A_{0}$ such that $A$ is a finite $A_{0}$ -module.

Facts & Assumptions

Given: A complete equicharacteristic Noetherian local domain $(A, m)$ of dimension $d$ , a coefficient field $k \subseteq A$ , a system of parameters $x_{1}, \dots, x_{d}$ , and the Axiom of Dependent Choice.

[L1]

A system of parameters generates an $m$ -primary ideal (Systems of parameters and parameter ideals, Parameter ideals are exactly the m-primary d-generated ideals).

[L2]

The continuous map from the formal power-series ring exists (Formal power-series substitution is the unique continuous k-algebra map).

[L3]

Complete Nakayama lifts generators modulo an ideal to actual generators (Complete Nakayama lemma).

Proof

technique · choose finitely many residue representatives modulo the parameter ideal and apply complete Nakayama over the source power-series ring

1.1

Let $J = (x_{1}, \dots, x_{d})$ . By [L1], $J$ is $m$ -primary, so $A / J$ has finite length and hence is a finite-dimensional $k$ -vector space. Choose lifts $y_{1}, \dots, y_{r} \in A$ of a $k$ -basis of $A / J$ .

L1givenchoose

2.1

By [L2], the map $ϕ$ exists. Put $B = k ⟦ X_{1}, \dots, X_{d} ⟧$ , $I_{0} = (X_{1}, \dots, X_{d})$ , and $A_{0} = ϕ (B)$ . Regard $A$ as a $B$ -module through $ϕ$ . Then $I_{0} A = J$ , and step 1.1 says that the classes of $y_{1}, \dots, y_{r}$ generate $A / I_{0} A = A / J$ as a module over $B / I_{0} = k$ .

L2step 1.1algebra

3.1

The ring $B$ is $I_{0}$ -adically complete by its coefficientwise formal-series construction. The $B$ -module $A$ is $I_{0}$ -adically separated: indeed, $I_{0}^{n} A = J^{n} \subseteq m^{n}$ for every $n$ , and $A$ is $m$ -adically separated. Therefore [L3] applies to the $B$ -module $A$ and the ideal $I_{0}$ , showing that $y_{1}, \dots, y_{r}$ generate $A$ as a $B$ -module. Since the $B$ -action factors through $A_{0} = ϕ (B)$ , the same elements generate $A$ as an $A_{0}$ -module. Hence $A$ is finite over $A_{0}$ .

L3step 2.1given

4.1

Therefore a complete equicharacteristic local domain is finite over the image of the parameter power-series map determined by any system of parameters and a coefficient field.

step 3.1∎

Depends on

Used by

Dependency tree · two levels

18 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

Melvin Hochster, The structure theory of complete local rings (standard reference, not scraped)
The Stacks Project, Section 10.160: The Cohen structure theorem (standard reference, not scraped)