Write for the valuation ring of , for a uniformizer, , and for the residue field. A useful strong form of Hensel lemma is the following: if and satisfy
then there is a root with , unique among roots in that ball. If , its distance satisfies .
Here is a proof by successive correction. Put , , and
Stop if a root has already been reached. Otherwise the correction has valuation . Integral Taylor expansions show that and
Thus grows at least geometrically, the corrections tend to zero, and completeness gives a limit with . The first correction has strictly smaller valuation than every later nonzero correction, proving the asserted distance. If are in the ball , then
The second factor cannot vanish. Two roots in the ball must therefore coincide. This proves Hensel lemma; in particular a simple root modulo has a unique lift with that residue.
We use this to establish existence and uniqueness of unramified local extensions. For each integer , choose a monic irreducible polynomial of degree and lift it to a monic . Reduction and Gauss lemma show that remains irreducible over . Let
The ring is finite free and complete over , and . An element outside is invertible: lift an inverse from the residue field and invert the remaining by a convergent geometric series. Every nonzero element of is times such a unit, since in a finite free module. Thus is a discrete valuation ring, its fraction field is , and
This constructs an unramified extension of each degree.
Conversely, let be an unramified extension of degree . Its residue field is the unique degree- finite field extension . Choose a residue root of in it. The root is simple, so Hensel lemma lifts it to a root of in . This embeds into , and equality of degrees makes it an isomorphism. All residue conjugates lift in itself; hence is Galois, and reduction identifies its Galois group with the cyclic Galois group of the residue field extension. Its distinguished Frobenius automorphism reduces to .
There is exactly one unramified extension of each degree inside a fixed algebraic closure, and
For the middle equality, every nonzero element of lifts uniquely to a st root of unity, because that exponent is prime to . A primitive such residue generates the finite field extension, so its lift generates . Taking the union gives the maximal unramified extension, with Galois group .
Use the simple-root form of the Hensel lemma: for and satisfying and , there is a unique with as its reduction and .
Let . The residue field is finite, so is separable, and the primitive element theorem gives . Let be the monic irreducible polynomial of , of degree , and choose a monic coefficient lift . Irreducible reduction implies that is irreducible over : any monic factorization over has integral coefficients, since all its roots are integral over the valuation ring, and would reduce to a factorization of .
Adjoin a root and put . Then and . Its reduction satisfies , so contains a copy of over . For finite extensions of non-Archimedean local fields, the fundamental degree relation is
The residue degree is at least , while the left side equals , hence
This constructs the required unramified extension.
For uniqueness, let be another unramified extension with a chosen identification . The element corresponding to is a simple residue root of , because finite fields are perfect. The Hensel lemma in gives a root with this reduction. Since is irreducible of degree , , so . Sending to yields a -isomorphism , compatible with the prescribed residue identification. Thus
This proves the existence and uniqueness of unramified local extensions using the stated version of Hensel's lemma, without assuming the classification in advance.