Newton's method over an adically complete ring

Let R be a commutative ring and π ∈ R an element for which R is π-adically complete (IsAdicComplete (Ideal.span {π}) R). Let A : (ι → R) → (ι → R) be a map on a finite free module, M a square matrix over R whose determinant is a unit, and u₀ a point with A u₀ ≡ 0 mod π. Suppose M is a uniform linearisation of A on the residue class of u₀: for every k ≥ 1 and all u, u' in that class with u' ≡ u mod π^k,

A u' ≡ A u + M (u' - u) mod π^(k+1).

Then A has exactly one zero in the residue class of u₀ (TauCeti.IsAdicComplete.existsUnique_eq_zero_of_isUnit_det).

This is a multivariable form of Hensel's lemma with an integral linearisation. No polynomiality of A is assumed: the linearisation hypothesis plays the role of the derivative, and the unit determinant of M that of the nonvanishing of the Jacobian modulo π. Mathlib's Mathlib.NumberTheory.Padics.Hensel is the one-variable polynomial case over ℤ_p. The theorem supplies the canonical character of a Demushkin group: its values on the generators are the zero of the map recording the values of the crossed homomorphisms on the relator.

Main results

• TauCeti.IsAdicComplete.existsUnique_eq_zero_of_isUnit_det: Newton's method, the existence and uniqueness of the zero.

theorem TauCeti.IsAdicComplete.existsUnique_eq_zero_of_isUnit_det {R : Type u_1} {ι : Type u_2} [CommRing R] (π : R) [IsAdicComplete (Ideal.span {π}) R] [Fintype ι] [DecidableEq ι] (A : (ι → R) → ι → R) {M : Matrix ι ι R} (hM : IsUnit M.det) (u₀ : ι → R) (h₀ : ∀ (i : ι), π ∣ A u₀ i) (hA : ∀ (u u' : ι → R), (∀ (i : ι), π ∣ u i - u₀ i) → (∀ (i : ι), π ∣ u' i - u₀ i) → ∀ (k : ℕ), 1 ≤ k → (∀ (i : ι), π ^ k ∣ u' i - u i) → ∀ (i : ι), π ^ (k + 1) ∣ A u' i - A u i - M.mulVec (u' - u) i) : ∃! u : ι → R, (∀ (i : ι), π ∣ u i - u₀ i) ∧ A u = 0

Newton's method over a π-adically complete ring. Let A : (ι → R) → (ι → R), let M be a matrix with unit determinant, and let u₀ satisfy A u₀ ≡ 0 mod π. If M linearises A uniformly on the residue class of u₀, in the sense that A u' ≡ A u + M (u' - u) mod π^(k+1) whenever u, u' lie in that class and u' ≡ u mod π^k with k ≥ 1, then A has exactly one zero in the residue class of u₀.