Hensel's lemma and local extensions

For $f\in\mathbb Z_p[x]$ and $a_1\in\mathbb Z_p$, assume $f(a_1)\equiv0\pmod p$ and $f'(a_1)\not\equiv0\pmod p$. There is a unique root a in Z_p congruent to a₁ modulo p. To lift a root approximation modulo $p^n$, write the next one as $a_n+t p^n$ with t chosen modulo p. Taylor expansion modulo $p^{n+1}$ makes the correction equation linear in t, and the unit derivative makes its solution unique.

The resulting approximations are compatible and Cauchy, so completeness supplies their limit and continuity makes it an exact root. This proof does not claim that a polynomial has only one root globally: distinct simple residue roots can lift to different roots. Nor does it work by real bisection or by choosing the ordinary-real closest root. Its error control measures increasing p-adic divisibility, and its uniqueness is within the declared residue class.

A common stronger form assumes $f'(a_0)\ne0$ and $v_p(f(a_0))>2v_p(f'(a_0))$ for a₀ in Z_p. Then a root exists and is unique in the ball $v_p(a-a_0)>v_p(f'(a_0))$. This is narrower than claiming uniqueness in the entire residue class when the derivative is not a unit. Newton iteration proves the result using a strict improvement of the error valuation. The derivative and function valuations must use the same normalization.

If the simple-root hypothesis fails, roots may still exist, may branch, or may disappear at a higher congruence level. For example x²−1 has two 2-adic roots, plus and minus one, both congruent to one modulo two; a simple-root uniqueness claim at that residue would be false because the derivative is even. Different valuation-based versions of Hensel's lemma have different non-strict or ball-size conditions, so quote the actual variant being applied rather than replacing it by a slogan that every modular root lifts.

A monic polynomial in Z_p[x] whose reduction is irreducible and separable of degree f over F_p gives an unramified degree-f extension when a root is adjoined to Q_p. Its residue field enlarges to F_(p^f) while p remains a uniformizer. By contrast an Eisenstein polynomial is monic, all nonleading coefficients are divisible by p, and its constant term is not divisible by p². It is irreducible and generates a totally ramified extension; its root is a uniformizer. These are sufficient constructions, not a claim that every defining polynomial is already in one of these forms.

For x^e−p, Eisenstein gives degree e, ramification index e, and residue degree one, including cases where ramification is wild. With the extension's integer-valued uniformizer normalization, the root has valuation one and p has valuation e. Under the valuation extending v_p, the root instead has valuation 1/e. Comparing these two conventions explicitly prevents a correct local-extension construction from appearing to contradict the base-field normalization used in the root-lifting inequalities.