Alphabeta Math
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.

✓ 35 results · all verified · 27 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 8 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Henselian Rings and Equicharacteristic Cohen Structure

1 · Prerequisites

2 · Summary

This page organizes three linked themes. Henselian pairs are introduced through coprime factor lifting, simple-root lifting, and idempotent lifting; complete, nilpotent, Artinian, and quotient cases then show where the abstract mechanism actually applies. The second half switches to complete equicharacteristic local rings, where maximal residue-injective subfields become coefficient fields and formal power-series substitution becomes the engine behind Cohen presentations.

The endpoint is the equicharacteristic Cohen structure theorem and its parameter-subring refinement for complete local domains. The coefficient-field and power-series conclusions here have the stated equicharacteristic hypotheses.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Henselian pairs and Henselian local rings

Definition

Let A be a commutative ring and let I⊆A be an ideal.

The pair (A,I) is a Henselian pair when:

  1. I⊆J(A), and
  2. for every monic polynomial f∈A[T] and every factorization f‾=g0h0 in (A/I)[T] with g0,h0 monic and (g0,h0)=(1), there is a unique factorization f=gh in A[T] with g,h monic and g‾=g0, h‾=h0.

If (A,m) is a local ring, then A is a Henselian local ring when the pair (A,m) is Henselian.

This page uses the Jacobson-radical condition as part of the definition rather than as a theorem proved later; that is the convention in the cited sources and is the hypothesis spent by the uniqueness and unit arguments below.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

The defining ideal of a Henselian pair lies in the Jacobson radical

Statement

If (A,I) is a Henselian pair, then I⊆J(A).

Facts & Assumptions

Given: A Henselian pair (A,I).

[L1]

A Henselian pair is defined by the Jacobson-radical condition together with unique lifting of coprime monic factorizations (Henselian pairs and Henselian local rings).

Proof

technique · unpack the definition
1.1L1given

By [L1], one clause in the definition of a Henselian pair is exactly the containment I⊆J(A).

2.1step 1.1∎

Therefore the defining ideal of a Henselian pair lies in the Jacobson radical.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Lift a Bezout identity for coprime residue factors

Statement

Let A be a commutative ring, let I⊆A be an ideal, and let g0,h0∈(A/I)[T] generate the unit ideal. If g,h∈A[T] lift g0,h0, then there exist polynomials a,b∈A[T] such that ag+bh≡1(modI).

Facts & Assumptions

Given: A commutative ring A, an ideal I, residue polynomials g0,h0∈(A/I)[T] with (g0,h0)=(1), and lifts g,h∈A[T].

[L1]

The quotient ring A/I and the polynomial ring over a commutative ring are again commutative rings, so Bezout identities and coefficientwise lifting make sense in (A/I)[T] and A[T] (The quotient ring R/I with (r+I)(s+I)=rs+I, The polynomial ring over a commutative ring as finitely supported coefficient sequences with convolution).

Proof

technique · lift one residue Bezout identity coefficientwise
1.1L1givenchoose

Because (g0,h0)=(1) in (A/I)[T], there exist a0,b0∈(A/I)[T] such that a0g0+b0h0=1.

2.1step 1.1L1choose

Lift the coefficients of a0 and b0 to polynomials a,b∈A[T]. Reducing coefficientwise modulo I gives ag+bh‾=a‾ g‾+b‾ h‾=a0g0+b0h0=1. Hence ag+bh≡1(modI).

3.1step 2.1∎

Thus a coprime residue factorization always admits a lifted Bezout relation modulo I.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Monicity and degree stay fixed during Hensel factor lifting

Statement

Let A be a commutative ring, let g,h∈A[T] be monic of degrees m,n, and let u,v∈A[T] satisfy deg⁡u<m and deg⁡v<n. Then g+u and h+v are still monic of degrees m and n.

Facts & Assumptions

Given: Monic polynomials g,h of degrees m,n and correction terms u,v with deg⁡u<m and deg⁡v<n.

[L1]

A polynomial of degree less than m has zero Tm-coefficient, and similarly a polynomial of degree less than n has zero Tn-coefficient.

Proof

technique · compare leading terms
1.1L1given

Since deg⁡u<m, [L1] shows that the coefficient of Tm in u is 0. Hence the coefficient of Tm in g+u is the coefficient of Tm in g, namely 1. Therefore g+u is monic of degree m.

1.2L1given

Since deg⁡v<n, [L1] shows that the coefficient of Tn in v is 0. Hence the coefficient of Tn in h+v is the coefficient of Tn in h, namely 1. Therefore h+v is monic of degree n.

2.1step 1.1step 1.2∎

Hence degree-bounded corrections preserve the prescribed monicity and degrees throughout Hensel lifting.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

One correction step raises factor lifting by one ideal power

Statement

Let A be a commutative ring, let I⊆A be an ideal, let f,g,h∈A[T] with f monic and g,h monic of degrees m,n, and let r≥1. Assume:

  1. deg⁡f=m+n,
  2. f−gh∈Ir[T], and
  3. there exist a,b∈A[T] with ag+bh≡1(modI).

Then there exist u,v∈Ir[T] with deg⁡u<m and deg⁡v<n such that for g′=g+u and h′=h+v one has f−g′h′∈Ir+1[T].

Facts & Assumptions

Given: A commutative ring A, an ideal I, monic polynomials f,g,h as above, an integer r≥1, an error term e=f−gh∈Ir[T], and a lifted Bezout relation ag+bh≡1(modI), with deg⁡f=m+n.

[L1]

A coprime residue factorization admits such a lifted Bezout identity modulo I (Lift a Bezout identity for coprime residue factors).

[L2]

Corrections of degrees <m and <n preserve the monicity and degrees of the factors (Monicity and degree stay fixed during Hensel factor lifting).

Proof

technique · solve the linearized correction equation modulo $I^{r+1}$
1.1L1givenalgebra

Put M=Ir/Ir+1, viewed as an A/I-module, and write ε∈M[T] for the class of e=f−gh. Since f and gh are monic of the same degree m+n, one has deg⁡ε<m+n. Multiplying ag+bh≡1(modI) by ε gives ε=(aε)g+(bε)hin M[T].

2.1step 1.1choosealgebra

Divide bε∈M[T] by the monic polynomial g to write bε=qg+uˉ,deg⁡uˉ<m. Substitution in step 1.1 gives ε=uˉh+vˉg,vˉ:=aε+qh. The polynomial ε−uˉh=vˉg has degree less than m+n; because g is monic of degree m, this forces deg⁡vˉ<n. Lift uˉ,vˉ coefficientwise to polynomials u,v∈Ir[T] with the same degree bounds.

3.1L2step 2.1givenalgebra

Set g′=g+u and h′=h+v. Then g′h′=gh+uh+vg+uv. By step 2.1, the first three terms agree with f modulo Ir+1, while uv∈I2r[T]⊆Ir+1[T] because r≥1. Hence f−g′h′∈Ir+1[T]. By [L2], g′ and h′ remain monic of degrees m,n.

4.1step 3.1∎

Therefore one Hensel correction step improves a lift modulo Ir to a lift modulo Ir+1 without changing the prescribed degrees.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Successive Hensel corrections are Cauchy

Statement

Let (gr,hr)r≥1 be a sequence of Hensel corrections such that gr+1−gr∈Ir[T] and hr+1−hr∈Ir[T] for every r≥1. Then each coefficient sequence of (gr) and of (hr) is Cauchy for the I-adic topology on A.

Facts & Assumptions

Given: Successive lifts (gr,hr) with differences in Ir[T] at stage r.

[L1]

One Hensel correction step changes each factor by a polynomial whose coefficients lie in the current ideal power (One correction step raises factor lifting by one ideal power).

Proof

technique · telescope the stagewise corrections
1.1L1givenalgebra

Fix a coefficient index j. If s>r, then the coefficient of Tj in gs−gr is a sum of coefficients from the increments gk+1−gk for k=r,…,s−1. By [L1], each summand lies in Ik⊆Ir, so the whole difference lies in Ir. Thus the jth coefficients of the gr form an I-adic Cauchy sequence.

1.2L1givenalgebra

The same argument applied to the increments hk+1−hk∈Ik[T] shows that each coefficient sequence of the hr is also I-adically Cauchy.

2.1step 1.1step 1.2∎

Hence the iterative Hensel corrections are coefficientwise Cauchy.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

The coefficientwise limits multiply back to the original polynomial

Statement

Let A be I-adically complete and separated, and let (gr,hr)r≥1 be monic polynomial lifts of fixed degrees such that:

  1. f−grhr∈Ir[T] for every r≥1, and
  2. the coefficient sequences of gr and hr are I-adically Cauchy.

Then the coefficientwise limits g,h∈A[T] exist and satisfy f=gh.

Facts & Assumptions

Given: An I-adically complete and separated ring A, a polynomial f∈A[T], and stagewise lifts (gr,hr) as above.

[L1]

The Hensel correction sequences are coefficientwise I-adically Cauchy (Successive Hensel corrections are Cauchy).

[L2]

Completeness gives limits of I-adic Cauchy sequences, and separatedness means that an element lying in every Ir is zero (Separated and complete filtered modules).

Proof

technique · take coefficientwise limits and use separatedness on each coefficient
1.1L1L2given

By completeness and [L2], each coefficient sequence of gr and of hr has a limit in A. Since the degrees are fixed and the leading coefficients are always 1, these limits assemble into monic polynomials g,h∈A[T] of the same degrees.

2.1step 1.1givenalgebra

Fix a coefficient index j of the product. Only finitely many coefficient pairs contribute to the Tj-coefficient of grhr, so ordinary continuity of finite sums and products shows that the Tj-coefficient of grhr converges to the Tj-coefficient of gh.

3.1L2step 2.1givenalgebra

For every r, the coefficient of Tj in f−grhr lies in Ir by hypothesis. Passing to the limit in step 2.1 shows that the coefficient of Tj in f−gh lies in every Ir. By separatedness and [L2], that coefficient is 0. Since this holds for every j, one has f=gh.

4.1step 1.1step 3.1∎

Therefore the coefficientwise limits of the iterative factors multiply back to the original polynomial.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Two lifted factorisations agree modulo every ideal power

Statement

Let A be a commutative ring, let I⊆A be an ideal, let f∈A[T], and let f=gh=g′h′ with g,h,g′,h′ monic, g‾=g′‾, h‾=h′‾, with g,g′ of the same degree m and h,h′ of the same degree n, and with g‾,h‾ coprime in (A/I)[T]. Then g≡g′(modIr[T])andh≡h′(modIr[T]) for every r≥1.

Facts & Assumptions

Given: Two monic lifts f=gh=g′h′ of the same coprime residue factorization.

[L1]

Coprime residue factors admit a lifted Bezout identity modulo I (Lift a Bezout identity for coprime residue factors).

Proof

technique · improve congruence one power at a time
1.1given

The congruences modulo I hold by hypothesis, so the claim is true for r=1.

2.1step 1.1givenassume-hypalgebra

Assume g≡g′(modIr[T]) and h≡h′(modIr[T]) for some r≥1. Write g′=g+u and h′=h+v with u,v∈Ir[T]. Since each pair consists of monic polynomials of the same degree, deg⁡u<m and deg⁡v<n. From gh=(g+u)(h+v) we get uh+vg+uv=0. Modulo Ir+1 the term uv vanishes, so uh+vg≡0(modIr+1).

3.1L1step 2.1algebradischarge-induction

Put M=Ir/Ir+1, and let uˉ,vˉ∈M[T] be the classes of u,v. Step 2.1 gives uˉh+vˉg=0. Choose a,b with ag+bh≡1(modI) by [L1]. Modulo the monic polynomial g, multiplication by h is invertible with inverse b, so uˉh=0 implies uˉ=0 modulo g. Since deg⁡uˉ<m=deg⁡g, this gives uˉ=0. The equation then becomes vˉg=0, and multiplication by the monic polynomial g is injective on M[T], so vˉ=0. Hence u,v∈Ir+1[T], proving the two congruences modulo Ir+1.

4.1step 1.1step 3.1∎

By induction, the two lifted factorisations agree modulo every power Ir.

PropositionStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Lifted coprime factorisations are unique

Statement

Let (A,I) be a Henselian pair. Let f∈A[T] be monic, and let f‾=g0h0 in (A/I)[T] with g0,h0 monic and coprime. Then there is at most one factorization f=gh with g,h monic and g‾=g0, h‾=h0.

Facts & Assumptions

Given: A Henselian pair (A,I), a monic polynomial f∈A[T], and a coprime monic residue factorization f‾=g0h0.

[L1]

In a Henselian pair, such lifted factorisations are part of the defining lifting property (Henselian pairs and Henselian local rings).

[L2]

Any two lifts of the same coprime residue factorization agree modulo every power of the ideal (Two lifted factorisations agree modulo every ideal power).

Proof

technique · combine the definition with the congruence induction
1.1L2given

Suppose f=gh=g′h′ are two monic lifts of the given residue factorization. By [L2], they agree modulo Ir[T] for every r≥1.

2.1L1step 1.1

In the present page's convention, [L1] already includes uniqueness of the lifted factorization. Therefore the two lifts must coincide. Step 1.1 records the explicit congruence mechanism that later examples use.

3.1step 2.1∎

Hence a coprime monic residue factorization has at most one Hensel lift.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-04Open item page →

A simple residue root determines a coprime residue factorisation

Statement

Let k be a field, let f‾∈k[T], and let a‾∈k satisfy f‾(a‾)=0 and f‾′(a‾)≠0. Then there exists h‾∈k[T] such that f‾=(T−a‾)h‾, and the factors T−a‾ and h‾ are coprime.

Facts & Assumptions

Given: A field k, a polynomial f‾∈k[T], and a simple root a‾ of f‾.

[L1]

Polynomial division by a monic linear polynomial is valid over any commutative ring, in particular over a field (The polynomial ring over a commutative ring as finitely supported coefficient sequences with convolution).

Proof

technique · divide by the linear factor and evaluate the derivative
1.1L1given

Since f‾(a‾)=0, polynomial division by T−a‾ gives a factorization f‾=(T−a‾)h‾ for some h‾∈k[T].

2.1step 1.1givenalgebra

Differentiating the identity of step 1.1 and evaluating at a‾ yields f‾′(a‾)=h‾(a‾). The left side is nonzero by hypothesis, so h‾(a‾)≠0. Therefore T−a‾ does not divide h‾, which is equivalent to (T−a‾,h‾)=(1) in k[T].

3.1step 1.1step 2.1∎

Thus a simple residue root determines a coprime residue factorization.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Factor lifting implies simple-root lifting

Statement

Let (A,m) be a Henselian local ring with residue field k=A/m. Let f∈A[T] be monic, and let a‾∈k be a simple root of f‾. Then there exists a unique a∈A lifting a‾ such that f(a)=0.

Facts & Assumptions

Given: A Henselian local ring (A,m), a monic polynomial f∈A[T], and a simple residue root a‾ of f‾.

[L1]

A simple residue root gives a coprime factorization f‾=(T−a‾)h‾ in k[T] (A simple residue root determines a coprime residue factorisation).

[L2]

A Henselian pair lifts coprime monic factorizations uniquely (Henselian pairs and Henselian local rings, Lifted coprime factorisations are unique).

Proof

technique · lift the linear factor
1.1L1L2given

By [L1], write f‾=(T−a‾)h‾ with T−a‾ and h‾ coprime. Since (A,m) is Henselian, [L2] gives a lifted factorization f=(T−a)h with a∈A reducing to a‾. Evaluating at T=a gives f(a)=0.

2.1L2step 1.1given

If a′ is another lift of a‾ with f(a′)=0, then f=(T−a′)h′ for some monic h′, and this is another lift of the same residue factorization. By [L2], the lifted factorization is unique, so T−a=T−a′ and hence a=a′.

3.1step 1.1step 2.1∎

Therefore factor lifting implies unique lifting of every simple residue root.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Idempotents lift uniquely in a Henselian pair

Statement

Let (A,I) be a Henselian pair. Every idempotent e‾∈A/I lifts to a unique idempotent e∈A.

Facts & Assumptions

Given: A Henselian pair (A,I) and an idempotent e‾∈A/I.

[L1]

In a Henselian pair, coprime monic factorizations lift uniquely (Henselian pairs and Henselian local rings).

Proof

technique · lift the factorization of $T^2-T$
1.1givenalgebra

Because e‾2=e‾, one has T2−T=(T−e‾)(T−(1−e‾)) in (A/I)[T]. The two factors are monic, and their difference is 1−2e‾, which is a unit because e‾(1−e‾)=0 forces every prime quotient to send e‾ to 0 or 1. Hence the factors are coprime.

2.1L1step 1.1

By [L1], this residue factorization lifts uniquely to T2−T=(T−e)(T−(1−e)) for some e∈A lifting e‾. Evaluating at T=e yields e2−e=0, so e is idempotent.

3.1L1step 2.1

If e′ is another lifted idempotent, then (T−e′)(T−(1−e′)) is a second lift of the same residue factorization. By [L1], the factorization is unique, so e′=e.

4.1step 2.1step 3.1∎

Therefore idempotents lift uniquely in a Henselian pair.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Simple-root lifting also lifts idempotents

Statement

Let (A,m) be a local ring whose simple residue roots lift uniquely. Then every idempotent of the residue field A/m lifts uniquely to an idempotent of A.

Facts & Assumptions

Given: A local ring (A,m) in which every simple residue root of a monic polynomial lifts uniquely.

[L1]

In a Henselian local ring, factor lifting implies unique lifting of simple residue roots (Factor lifting implies simple-root lifting).

Proof

technique · apply the simple-root criterion to $T^2-T$
1.1givenalgebra

The residue ring A/m is a field, so its only idempotents are 0 and 1. For e‾∈{0,1}, the polynomial p(T)=T2−T satisfies p(e‾)=0 and p′(e‾)=2e‾−1∈{−1,1}, hence e‾ is a simple residue root.

2.1step 1.1given

By the assumed simple-root lifting property, there is a unique lift e∈A of e‾ with p(e)=0. The equation p(e)=0 is exactly e2=e, so e is idempotent.

3.1L1step 2.1∎

Therefore the simple-root form lifts residue idempotents uniquely. The role of [L1] is only to identify this as the same mechanism already proved for Henselian local rings.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

The simple-root form recovers factor lifting

Statement

Let (A,m) be a local ring with residue field k. Assume every simple root a‾∈k of the reduction f‾ of every monic polynomial f∈A[T] lifts uniquely to an element a∈A satisfying f(a)=0. Then (A,m) has the coprime monic factor-lifting property.

Facts & Assumptions

Given: A local ring (A,m) in which, for every monic f∈A[T], every simple root of f‾∈k[T] lifts uniquely to a root of f in A.

[L1]

Stacks, Section 10.153, Lemma 10.153.3 identifies the simple-root lifting condition for a local ring with the coprime monic factor-lifting property.

Proof

technique · invoke the local converse in the cited source
1.1L1given

The hypothesis of this item is exactly the simple-root lifting condition in [L1], and conclusion (3) of [L1] is exactly the coprime monic factor-lifting property. Therefore the cited source yields the required factorization statement for (A,m).

2.1step 1.1∎

Therefore unique lifting of simple residue roots recovers unique lifting of coprime monic factorizations.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

A local ring is Henselian exactly when simple residue roots lift uniquely

Statement

Let (A,m) be a local ring. Then A is Henselian if and only if every simple root of every monic polynomial over the residue field A/m lifts uniquely to a root over A.

Facts & Assumptions

Given: A local ring (A,m).

[L1]

Henselian factor lifting implies unique simple-root lifting (Factor lifting implies simple-root lifting).

[L2]

Unique simple-root lifting recovers the coprime factor-lifting property (The simple-root form recovers factor lifting).

[L3]

A Henselian local ring is precisely a local ring whose maximal-ideal pair is Henselian (Henselian pairs and Henselian local rings).

Proof

technique · prove the two implications separately
1.1L1L3given

If A is Henselian, then [L3] identifies (A,m) as a Henselian pair, and [L1] gives unique lifting of every simple residue root.

1.2L2L3given

Conversely, assume every simple residue root lifts uniquely. Then [L2] gives the coprime monic factor-lifting property for (A,m). Since m is the unique maximal ideal of the local ring, one has m⊆J(A), so [L3] shows that A is Henselian.

2.1step 1.1step 1.2∎

Therefore a local ring is Henselian exactly when every simple residue root lifts uniquely.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Equivalent elementary forms of Hensel's property

Statement

For a local ring (A,m), the following are equivalent:

  1. A is Henselian.
  2. Every simple root of every monic polynomial over A/m lifts uniquely to A.
  3. For every finite A-algebra B, the map from idempotents of B to idempotents of B/mB is a bijection.

Facts & Assumptions

Given: A local ring (A,m).

[L1]

Henselianity is equivalent to unique simple-root lifting (A local ring is Henselian exactly when simple residue roots lift uniquely).

[L2]

In Stacks, Section 15.11, Lemma 15.11.6, a pair (A,I) is Henselian if and only if for every finite A-algebra B the map B→B/IB induces a bijection on idempotents.

[L3]

A local ring A is Henselian exactly when its maximal-ideal pair (A,m) is Henselian (Henselian pairs and Henselian local rings).

Proof

technique · combine the local criterion with the pair-level finite-algebra characterization from the cited source
1.1L1given

By [L1], conditions (1) and (2) are equivalent.

1.2L2L3given

By [L3], condition (1) says exactly that the pair (A,m) is Henselian. Then [L2] identifies this with the finite-algebra idempotent bijection in condition (3). Hence conditions (1) and (3) are equivalent.

2.1step 1.1step 1.2∎

Since (1) is equivalent to both (2) and (3), all three conditions are equivalent.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Complete separated adic pairs are Henselian

Statement

Let A be a commutative ring and let I⊆A be an ideal. If A is I-adically complete and separated, then (A,I) is a Henselian pair.

Facts & Assumptions

Given: A commutative ring A that is I-adically complete and separated.

[L1]

In an I-adically complete ring, every element congruent to 1 modulo I is a unit (Elements congruent to 1 modulo a defining ideal are units).

[L2]

Coprime residue factors admit a lifted Bezout identity modulo I (Lift a Bezout identity for coprime residue factors).

[L3]

One Hensel correction step improves a factorization from modulo Ir to modulo Ir+1 (One correction step raises factor lifting by one ideal power).

[L4]

The correction sequence is coefficientwise Cauchy and its coefficientwise limit multiplies back to the original polynomial (Successive Hensel corrections are Cauchy, The coefficientwise limits multiply back to the original polynomial).

[L5]

Two such lifts agree modulo every power of I (Two lifted factorisations agree modulo every ideal power).

[L6]

A Henselian pair is exactly a pair satisfying the Jacobson-radical clause and the unique coprime factor-lifting clause (Henselian pairs and Henselian local rings).

Proof

technique · iterate the correction lemma and pass to the limit
1.1L1givenalgebra

Let x∈I and r∈A. Then rx∈I, so 1−rx≡1(modI). By [L1], the element 1−rx is a unit. This is the Jacobson-radical criterion for x, so x∈J(A). Hence I⊆J(A).

1.2L2L3givenchooseinduction

Let f∈A[T] be monic and let f‾=g0h0 be a coprime monic factorization in (A/I)[T]. Choose monic lifts g1,h1 of g0,h0. By [L2], choose a,b∈A[T] with ag1+bh1≡1(modI). Repeatedly applying [L3] produces monic pairs (gr,hr) with f−grhr∈Ir[T] for every r≥1.

2.1L4step 1.2

By [L4], the coefficient sequences of (gr) and (hr) are Cauchy and converge to monic polynomials g,h∈A[T] with f=gh. Their reductions are still g0,h0. Thus the required lifted factorization exists.

3.1L5step 2.1given

If f=g′h′ is another monic lift of the same residue factorization, then [L5] gives g≡g′(modIr[T]) and h≡h′(modIr[T]) for every r≥1. Separatedness forces g=g′ and h=h′. Hence the lift is unique.

4.1L6step 1.1step 2.1step 3.1∎

Steps 1.1-3.1 verify both clauses of the definition, so (A,I) is a Henselian pair.

CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Complete local rings are Henselian

Statement

If (A,m) is a local ring that is complete and separated for its maximal-ideal topology, then A is Henselian.

Facts & Assumptions

Given: A local ring (A,m) complete and separated for the m-adic topology.

[L1]

Every complete separated adic pair is Henselian (Complete separated adic pairs are Henselian).

Proof

technique · apply the pair statement to the maximal ideal
1.1L1given

By [L1], the pair (A,m) is Henselian because A is complete and separated for the m-adic topology.

2.1step 1.1given∎

By definition, a local ring is Henselian exactly when its maximal-ideal pair is Henselian. Therefore A is Henselian.

CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Nilpotent Jacobson pairs are Henselian

Statement

Let A be a commutative ring and let I⊆J(A) be a nilpotent ideal. Then (A,I) is a Henselian pair.

Facts & Assumptions

Given: A commutative ring A and a nilpotent ideal I⊆J(A).

[L1]

Every complete separated adic pair is Henselian (Complete separated adic pairs are Henselian).

Proof

technique · nilpotence makes the adic tower stationary
1.1givenchoosealgebra

Choose N≥1 with IN=0. Then for every r≥N, the quotients A/Ir stabilize at A, so A is automatically complete and separated for the I-adic topology.

2.1L1step 1.1∎

Applying [L1] to the ideal I shows that (A,I) is Henselian.

CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Artinian local rings are Henselian

Statement

Assume the Axiom of Choice.

Every Artinian local ring is Henselian.

Facts & Assumptions

Given: A commutative Artinian local ring (A,m) and the Axiom of Choice.

[L1]
[L2]

A nilpotent ideal contained in the Jacobson radical gives a Henselian pair (Nilpotent Jacobson pairs are Henselian).

Proof

technique · use the nilpotent maximal ideal
1.1L1given

By [L1], there exists N≥1 with mN=0. Since m is the maximal ideal of a local ring, it lies in the Jacobson radical.

2.1L2step 1.1∎

Therefore [L2] applies to the pair (A,m), so (A,m) is Henselian. Equivalently, the Artinian local ring A is Henselian.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Henselian factor lifting descends to quotients

Statement

Let (A,I) be a Henselian pair and let J⊆A be an ideal. Then the quotient pair (A/J,(I+J)/J) has the coprime monic factor-lifting property.

Facts & Assumptions

Given: A Henselian pair (A,I) and an ideal J⊆A.

[L1]

A Henselian pair uniquely lifts coprime monic factorizations modulo its defining ideal (Henselian pairs and Henselian local rings).

Proof

technique · use the integral quotient map and then unpack the definition
1.1givenalgebra

The quotient map A→A/J is integral because every element of A/J satisfies a monic linear equation over the image of A. The integral-base-change lemma for Henselian pairs in Stacks tag 09XD therefore applies to the Henselian pair (A,I) and shows that the quotient pair (A/J,(I+J)/J) is again Henselian.

2.1L1step 1.1

By [L1], every Henselian pair has the coprime monic factor-lifting property. Applying that definition to the pair from step 1.1 gives the claimed lifting property for (A/J,(I+J)/J).

3.1step 2.1∎

Hence Henselian factor lifting descends to quotients.

CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Quotients of Henselian local rings are Henselian

Statement

Let (A,m) be a Henselian local ring and let J⊊A be a proper ideal. Then A/J is a Henselian local ring.

Facts & Assumptions

Given: A Henselian local ring (A,m) and a proper ideal J⊊A.

[L1]

Quotient pairs inherit the coprime monic factor-lifting property (Henselian factor lifting descends to quotients).

Proof

technique · identify the maximal ideal of the quotient and apply the quotient-pair lemma
1.1givenalgebra

The quotient A/J is local with maximal ideal (m+J)/J.

1.2L1given

Since (A,m) is Henselian, the pair (A,m) is Henselian. Applying [L1] with I=m shows that the quotient pair (A/J,(m+J)/J) has the Henselian factor-lifting property.

2.1step 1.1step 1.2∎

Together with step 1.1, this is exactly the definition of a Henselian local ring for A/J.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Equicharacteristic local rings and coefficient fields

Definition

Let (A,m) be a local ring with residue field k=A/m.

The local ring A is equicharacteristic when char⁡(A) and char⁡(k) are equal.

A coefficient field of A is a subfield K⊆A such that the residue map A→k restricts to an isomorphism K→∼k.

Thus a coefficient field is not merely an embedded field: it is an embedded copy of the residue field itself.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

A coefficient field maps isomorphically to the residue field

Statement

Let (A,m) be a local ring with residue field k=A/m. If K⊆A is a coefficient field, then the residue map restricts to a field isomorphism K→∼k.

Facts & Assumptions

Given: A local ring (A,m) and a coefficient field K⊆A.

[L1]

A coefficient field is defined to be a subfield on which the residue map is an isomorphism onto the residue field (Equicharacteristic local rings and coefficient fields).

Proof

technique · unpack the definition
1.1L1given

By [L1], the defining property of a coefficient field is precisely that the composite K↪A↠A/m is an isomorphism.

2.1step 1.1∎

Therefore a coefficient field maps isomorphically to the residue field.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

The prime field lifts in the equicharacteristic case

Statement

Let (A,m) be an equicharacteristic local ring with residue field k=A/m. Then the prime field of k has a canonical copy inside A, and the residue map identifies that copy with the prime field of k.

Facts & Assumptions

Given: An equicharacteristic local ring (A,m) with residue field k.

[L1]

Every field has a prime subfield, isomorphic either to Q or to Fp according to its characteristic (A field's prime subfield is isomorphic to Q in characteristic zero and to Fp in characteristic p).

[L2]

Equicharacteristic means char⁡(A)=char⁡(k) (Equicharacteristic local rings and coefficient fields).

Proof

technique · compare the two characteristics
1.1L1L2givenalgebra

By [L2], the ring A and its residue field k have the same characteristic. If that characteristic is 0, then the unique map Z→A kills no nonzero integer, so it extends to an embedding Q↪A. If the characteristic is p>0, then the image of Z→A is a copy of Fp inside A.

2.1L1step 1.1

Reducing these embedded prime fields modulo m gives the prime subfield of k, because A and k have the same characteristic and prime subfields are unique by [L1].

3.1step 2.1∎

Therefore the prime field of the residue field lifts canonically in the equicharacteristic case.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Maximal residue-injective subfields exist

Statement

Assume the Axiom of Choice.

Let (A,m) be an equicharacteristic local ring. Then there exists a subfield K⊆A that is maximal, under inclusion, among subfields whose residue map to A/m is injective.

Facts & Assumptions

Given: An equicharacteristic local ring (A,m) and the Axiom of Choice.

[L1]

The residue field's prime field embeds in A, so the family of residue-injective subfields is nonempty (The prime field lifts in the equicharacteristic case).

[L2]

Assuming the Axiom of Choice, every nonempty poset in which every chain has an upper bound has a maximal element (Zorn's lemma).

Proof

technique · apply Zorn's lemma to the poset of residue-injective subfields
1.1L1givenconstruct

Let S be the set of subfields K⊆A for which the residue map K→A/m is injective. By [L1], S is nonempty. Order S by inclusion.

2.1step 1.1givenalgebra

If C⊆S is a chain, then ⋃K∈CK is again a subfield of A: closure under the field operations is inherited from some chain member containing the finitely many elements involved. Its residue map is still injective, because a nonzero element of the union already lies in one chain member where injectivity holds. Thus every chain in S has an upper bound in S.

3.1L2step 2.1∎

By [L2], the poset S has a maximal element. That is exactly a maximal residue-injective subfield of A.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Separable residue elements adjoin across a maximal subfield

Statement

Let (A,m) be a complete equicharacteristic local ring, let K⊆A be a residue-injective subfield, and let ρ(K)⊆k be its image in the residue field k=A/m. If u‾∈k is separable algebraic over ρ(K) and u‾∉ρ(K), then there exists a strictly larger residue-injective subfield K′⊆A whose residue image contains u‾.

Facts & Assumptions

Given: A complete equicharacteristic local ring (A,m), a residue-injective subfield K⊆A, and a residue element u‾∉ρ(K) separable algebraic over ρ(K).

[L1]

Complete local rings are Henselian, hence satisfy the simple-root lifting criterion (Complete local rings are Henselian, A local ring is Henselian exactly when simple residue roots lift uniquely).

[L2]

Maximal residue-injective subfields are the objects to be enlarged in the coefficient-field argument (Maximal residue-injective subfields exist).

Proof

technique · lift the separable minimal polynomial
1.1givenchoosealgebra

Let p‾(T)∈ρ(K)[T] be the minimal polynomial of u‾. Since u‾ is separable over ρ(K), one has p‾′(u‾)≠0. Lift the coefficients of p‾ through the residue isomorphism ρ:K→ρ(K) to a monic polynomial p(T)∈K[T]⊆A[T].

2.1L1step 1.1givenalgebra

By [L1], the simple residue root u‾ of p‾ lifts uniquely to some u∈A with p(u)=0. Then K[u] is an integral domain finite over K, and its fraction field K′:=K(u) sits inside A because every nonzero element of K[u] has nonzero residue, hence is a unit in the local ring A. The residue image of K′ contains both ρ(K) and u‾.

3.1step 2.1givenalgebra

The residue map is injective on K′: if x/y∈K′ has zero residue, then ρ(x)=0, so x=0 because K[u]→k remains injective on polynomials of degree smaller than the minimal polynomial of u‾. Moreover, u∉K because u‾∉ρ(K). Thus K′ is a strictly larger residue-injective subfield containing a lift of u‾.

4.1L2step 3.1∎

Therefore every separable residue element adjoins across a maximal residue-injective subfield. The role of [L2] is to show exactly why this contradicts maximality in the later corollary.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-04Open item page →

Transcendental residue elements adjoin across a maximal subfield

Statement

Let (A,m) be a local ring, let K⊆A be a residue-injective subfield, and let u‾∈A/m be transcendental over the residue image ρ(K). Then there exists a larger residue-injective subfield K′⊆A whose residue image contains u‾.

Facts & Assumptions

Given: A local ring (A,m), a residue-injective subfield K⊆A, and a residue element u‾ transcendental over ρ(K).

[L1]

A coefficient-field argument enlarges a residue-injective subfield by adjoining new residue elements when injectivity is preserved (Maximal residue-injective subfields exist).

[L2]

The residue image of a subfield is a field inside the residue field (Equicharacteristic local rings and coefficient fields).

Proof

technique · evaluate rational functions at a lift of the transcendental residue element
1.1L2givenchoose

Choose any lift u∈A of u‾. For every nonzero polynomial q(T)∈K[T], the residue of q(u) is q(u‾)∈ρ(K)(u‾). Since u‾ is transcendental over ρ(K), this residue is nonzero, so q(u)∉m and therefore is a unit of A.

2.1step 1.1givenconstruct

Hence evaluation at u defines an injective homomorphism K(T)⟶A,r(T)⟼r(u), because every denominator evaluates to a unit by step 1.1. Let K′ be its image. Then K′ is a subfield of A, and its residue image contains ρ(K) together with u‾.

3.1L1step 2.1algebra

If an element of K′ has zero residue, its representing rational function has zero value at the transcendental element u‾, so the rational function is zero. Thus the residue map is injective on K′. By [L1], this is exactly the desired enlargement step.

4.1step 3.1∎

Therefore every transcendental residue element adjoins across a maximal residue-injective subfield.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-04Open item page →

Completeness resolves the purely inseparable prime-field case

Statement

Let (A,m) be a complete equicharacteristic local ring of characteristic p>0, with residue field k. If every element of k is purely inseparable over the prime field Fp, then the canonical copy of Fp inside A is contained in a coefficient field of A.

Facts & Assumptions

Given: A complete equicharacteristic local ring (A,m) of characteristic p>0 whose residue field k is purely inseparable over Fp.

[L1]

The prime field already lifts in the equicharacteristic case (The prime field lifts in the equicharacteristic case).

[L2]

A coefficient field is a subfield of A mapping isomorphically to the residue field (Equicharacteristic local rings and coefficient fields).

[L3]

Stacks, Section 10.160, Theorem 10.160.8 constructs a coefficient ring in every complete local ring; in the equicharacteristic case that coefficient ring is a field.

Proof

technique · apply the complete-local source theorem to the prime-field case
1.1L1given

By [L1], the prime field Fp has its canonical copy inside A.

2.1L2L3step 1.1choose

By [L3], the cited Cohen structure theorem yields a coefficient ring C⊆A. Because A is equicharacteristic, that coefficient ring is a field, hence a coefficient field in the sense of [L2]. Every subfield of characteristic p contains the prime field, so the canonical copy of Fp from step 1.1 lies in C.

3.1step 2.1∎

Therefore, in the purely inseparable case over the prime field, completeness supplies a coefficient field containing the canonical prime-field lift.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Complete equicharacteristic local rings have coefficient fields

Statement

Assume the Axiom of Choice.

Every complete equicharacteristic Noetherian local ring contains a coefficient field.

Facts & Assumptions

Given: A complete equicharacteristic Noetherian local ring (A,m) and the Axiom of Choice.

[L1]

Stacks, Section 10.160, Theorem 10.160.8 gives a coefficient ring in every complete local ring; in the equicharacteristic case that coefficient ring is a field.

[L2]

A coefficient field is exactly a subfield mapping isomorphically to the residue field (Equicharacteristic local rings and coefficient fields).

Proof

technique · apply the Cohen structure theorem directly
1.1L1givenchoose

By [L1], the complete local ring A contains a coefficient ring Λ⊆A. Because A is equicharacteristic, the cited source says that Λ is a field mapping isomorphically to A/m.

2.1L2step 1.1

By [L2], any such subfield is a coefficient field in the library's terminology. Therefore Λ is a coefficient field of A.

3.1step 2.1∎

Therefore every complete equicharacteristic Noetherian local ring has a coefficient field.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

Formal power-series substitution converges in a complete local algebra

Statement

Let (A,m) be a complete local ring, let k→A be a ring map, and let x1,…,xn∈m. For a formal series F=∑αaαXα∈k⟦X1,…,Xn⟧, the partial sums ordered by total degree, SN=∑∣α∣<Naαxα, form an m-adically Cauchy sequence in A and hence converge.

Facts & Assumptions

Given: A complete local ring (A,m), a ring map k→A, and elements x1,…,xn∈m.

[L1]

Completeness means that every m-adically Cauchy sequence in A converges (Separated and complete filtered modules).

Proof

technique · degree-$N$ tails land in $\mathfrak m^N$
1.1givenalgebra

If M>N, then SM−SN=∑N≤∣α∣<Maαxα. Every monomial xα appearing here is a product of ∣α∣≥N elements of m, so by the definition of the ideal power mN one has xα∈mN. Hence SM−SN∈mN.

2.1L1step 1.1

Step 1.1 is exactly the m-adic Cauchy condition for (SN). By [L1], the partial sums therefore converge in A.

3.1step 2.1∎

Thus substitution of maximal-ideal elements into a multivariable formal power series converges in a complete local ring.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-04Open item page →

Formal power-series substitution is the unique continuous k-algebra map

Statement

Let (A,m) be a complete local ring, let k→A be a ring map, and let x1,…,xn∈m. Then there is a unique continuous k-algebra homomorphism ϕ:k⟦X1,…,Xn⟧→A such that ϕ(Xi)=xi for every i.

Facts & Assumptions

Given: A complete local ring (A,m), a ring map k→A, and elements x1,…,xn∈m.

[L1]

Degreewise substitution converges for every formal series (Formal power-series substitution converges in a complete local algebra).

Proof

technique · define the map by convergent substitution and use density of polynomials
1.1L1givenconstruct

By [L1], every series F=∑αaαXα has a convergent substituted sum ϕ(F):=∑αaαxα∈A. Finite truncations show that ϕ respects addition and multiplication, and by construction ϕ is a k-algebra map with ϕ(Xi)=xi.

2.1step 1.1givenalgebra

The map is continuous for the (X1,…,Xn)-adic topology on the source and the m-adic topology on the target, because every series all of whose monomials have total degree at least N maps into mN.

3.1step 1.1step 2.1given

If ψ is another continuous k-algebra map with ψ(Xi)=xi, then ψ agrees with ϕ on the polynomial subring k[X1,…,Xn]. Every formal series is the limit of its polynomial truncations, and both maps are continuous, so they agree on all of k⟦X1,…,Xn⟧. Therefore ϕ is unique.

4.1step 3.1∎

Thus formal substitution is the unique continuous k-algebra map sending each indeterminate to the chosen maximal-ideal element.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-04Open item page →

The Cohen map is surjective modulo every power of the maximal ideal

Statement

Let (A,m) be a complete equicharacteristic Noetherian local ring, let k⊆A be a coefficient field, and let x1,…,xe∈m lift a k-basis of m/m2. Let ϕ:k⟦X1,…,Xe⟧→A be the continuous k-algebra map with ϕ(Xi)=xi. Then for every n≥1, the induced map k⟦X1,…,Xe⟧/(X1,…,Xe)n→A/mn is surjective.

Facts & Assumptions

Given: A complete equicharacteristic Noetherian local ring (A,m), a coefficient field k⊆A, and lifts x1,…,xe of a basis of m/m2.

[L1]

Proof

technique · generate $\mathfrak m^r/\mathfrak m^{r+1}$ by degree-$r$ monomials
1.1L2L3givenalgebra

By [L2], the elements x1,…,xe generate m. Therefore every product of r generators is the image under ϕ of a degree-r monomial, and by [L3] these monomials span mr/mr+1 over k for every r≥1.

2.1L1step 1.1givenalgebra

Modulo m, the map ϕ is already surjective because its image contains the coefficient field k and the quotient A/m equals k. By step 1.1, every class in each successive quotient mr/mr+1 also has a polynomial preimage of total degree exactly r. Summing those representatives for r=0,…,n−1 shows that every class in A/mn has a preimage in the source modulo (X1,…,Xe)n.

3.1step 2.1∎

Hence the Cohen map is surjective modulo every power of the maximal ideal.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-04Open item page →

The Cohen map is surjective by completeness

Statement

Let (A,m) be a complete equicharacteristic Noetherian local ring, let k⊆A be a coefficient field, let x1,…,xe∈m lift a k-basis of m/m2, and let ϕ:k⟦X1,…,Xe⟧→A be the continuous k-algebra homomorphism with ϕ(Xi)=xi. Then ϕ is surjective.

Facts & Assumptions

Given: A complete equicharacteristic Noetherian local ring (A,m), a coefficient field k⊆A, lifts x1,…,xe∈m of a k-basis of m/m2, and the resulting continuous k-algebra map ϕ.

[L1]

Degreewise formal-series substitution converges in a complete local ring (Formal power-series substitution converges in a complete local algebra).

[L2]

For every n≥1, each class in mn/mn+1 has a homogeneous degree-n polynomial preimage under the Cohen map (The Cohen map is surjective modulo every power of the maximal ideal).

Proof

technique · build a compatible inverse system of polynomial approximations
1.1L2givenchooseinduction

Let a∈A. Because k→A/m is an isomorphism, choose F0∈k with ϕ(F0)≡a(modm). Inductively, if Fn−1 is chosen with ϕ(Fn−1)≡a(modmn), then [L2] applied to the error class in mn/mn+1 gives a homogeneous polynomial correction Hn of degree n such that ϕ(Fn)≡a(modmn+1),Fn:=Fn−1+Hn.

2.1L1step 1.1algebra

The formal sum F=∑n≥0Hn defines an element of k⟦X1,…,Xe⟧. By [L1], the series ϕ(F)=∑n≥0ϕ(Hn) converges in A, and step 1.1 says its partial sums are congruent to a modulo arbitrarily high powers of m. Since A is separated, the limit must equal a.

3.1step 2.1∎

Therefore every a∈A lies in the image of ϕ, so ϕ is surjective.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04Open item page →

A complete equicharacteristic Noetherian local ring is a power-series quotient

Statement

Assume the Axiom of Choice.

Let (A,m) be a complete equicharacteristic Noetherian local ring, let k=A/m, and let e=dim⁡k(m/m2). Then there is a surjective k-algebra homomorphism k⟦X1,…,Xe⟧↠A.

Facts & Assumptions

Given: A complete equicharacteristic Noetherian local ring (A,m) and the Axiom of Choice.

[L1]

The ring A contains a coefficient field mapping isomorphically to its residue field (Complete equicharacteristic local rings have coefficient fields).

[L2]

Once the coefficient field and lifts of a basis of m/m2 are chosen, the associated formal-series map is surjective (The Cohen map is surjective by completeness).

Proof

technique · choose a coefficient field and generators of $\mathfrak m/\mathfrak m^2$
1.1L1givenchoose

By [L1], choose a coefficient field k⊆A. Choose elements x1,…,xe∈m lifting a k-basis of m/m2.

2.1L2step 1.1

The universal substitution construction gives a continuous k-algebra map ϕ:k⟦X1,…,Xe⟧→A,Xi↦xi. By [L2], this map is surjective.

3.1step 2.1∎

Therefore A is a quotient of the formal power-series ring in e variables over its residue field.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-04Open item page →

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⊆A be a coefficient field, and let x1,…,xd be a system of parameters. Then the continuous map ϕ:k⟦X1,…,Xd⟧→A,Xi↦xi, has image A0 such that A is a finite A0-module.

Facts & Assumptions

Given: A complete equicharacteristic Noetherian local domain (A,m) of dimension d, a coefficient field k⊆A, a system of parameters x1,…,xd, and the Axiom of Dependent Choice.

[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.1L1givenchoose

Let J=(x1,…,xd). By [L1], J is m-primary, so A/J has finite length and hence is a finite-dimensional k-vector space. Choose lifts y1,…,yr∈A of a k-basis of A/J.

2.1L2step 1.1algebra

By [L2], the map ϕ exists. Put B=k⟦X1,…,Xd⟧, I0=(X1,…,Xd), and A0=ϕ(B). Regard A as a B-module through ϕ. Then I0A=J, and step 1.1 says that the classes of y1,…,yr generate A/I0A=A/J as a module over B/I0=k.

3.1L3step 2.1given

The ring B is I0-adically complete by its coefficientwise formal-series construction. The B-module A is I0-adically separated: indeed, I0nA=Jn⊆mn for every n, and A is m-adically separated. Therefore [L3] applies to the B-module A and the ideal I0, showing that y1,…,yr generate A as a B-module. Since the B-action factors through A0=ϕ(B), the same elements generate A as an A0-module. Hence A is finite over A0.

4.1step 3.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.

LemmaStatement: Literature-sourcedProof: AI-adaptedverified 2026-09-24 (gpt-6-sol)Open item page →

The parameter power-series map is injective by dimension

Statement

Assume the Axiom of Dependent Choice.

Let (A,m) be a complete equicharacteristic Noetherian local domain of dimension d, let k⊆A be a coefficient field, and let x1,…,xd be a system of parameters. Then the continuous map ϕ:k⟦X1,…,Xd⟧→A,Xi↦xi, is injective.

Facts & Assumptions

Given: A complete equicharacteristic Noetherian local domain (A,m) of dimension d, a coefficient field k, a system of parameters x1,…,xd, and the Axiom of Dependent Choice.

[L2]

The given system of parameters has length d, and the statement already assumes dim⁡A=d (Systems of parameters and parameter ideals).

[L3]

The formal power-series ring k⟦X1,…,Xd⟧ is a Noetherian local domain of dimension d (Stacks Project, Section 10.160, Remark 10.160.9).

[L4]

A strict chain of primes contracts to a strict chain along an integral injection (Strict prime chains contract strictly under integral extensions).

Proof

technique · a nonzero kernel would force the source quotient to have dimension less than the target
1.1L1givenassume-contraalgebra

Let B=k⟦X1,…,Xd⟧ and suppose P:=ker⁡(ϕ)≠0. Since A is a domain, P is prime. By [L1], A is finite over the image B/P, hence integral over B/P.

2.1L3step 1.1algebra

By [L3], B is a domain of dimension d. Every strict chain of primes in B/P lifts to a strict chain of primes of B containing P; adjoining P at the bottom if necessary, write it as P=p0⊊p1⊊⋯⊊pℓ. This chain can be preceded by the strict inclusion (0)⊊P. Hence ℓ+1≤d, and therefore dim⁡(B/P)≤d−1.

3.1L2L4step 1.1step 2.1discharge-contradiction

By [L4], every strict chain of primes in A contracts to a strict chain in B/P, so dim⁡A≤dim⁡(B/P). Combining this with step 2.1 gives d=dim⁡A≤d−1, contradicting [L2].

4.1step 3.1∎

Therefore ker⁡(ϕ)=0, so ϕ is injective.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-04Open item page →

A complete local domain is finite over a regular power-series ring

Statement

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⊆A and an injective local homomorphism k⟦X1,…,Xd⟧↪A whose image is a regular complete local subring over which A is module-finite.

Facts & Assumptions

Given: A complete equicharacteristic Noetherian local domain (A,m) of dimension d and the Axiom of Choice.

[L1]

The parameter power-series map makes A finite over its image (Parameters make a complete local domain finite over the image of a power-series map).

[L3]

A system of parameters is the d-tuple that determines the relevant map (Systems of parameters and parameter ideals).

Proof

technique · choose parameters, then identify the source with its image
1.1L3givenchoose

Choose a coefficient field k⊆A and a system of parameters x1,…,xd. By [L3], these parameters determine the continuous map ϕ:k⟦X1,…,Xd⟧→A,Xi↦xi.

2.1L1L2step 1.1

By [L1], A is finite over ϕ(k⟦X1,…,Xd⟧), and by [L2] the map ϕ is injective. Therefore we may identify the source with a subring A0⊆A over which A is module-finite. Standard formal-power-series theory makes A0≅k⟦X1,…,Xd⟧ a regular complete local ring.

3.1step 2.1∎

Hence A is finite over a regular power-series subring in d variables over a coefficient field.

5 · Examples, counterexamples and false statements

None yet.

Sources