Hensel lifting of coprime factorizations over power series

Let R be a commutative ring and P a monic polynomial over R⟦t⟧. If the reduction of P modulo t factors as g * h with g and h monic and coprime in R[X], then P = G * H for unique monic G and H over R⟦t⟧ reducing to g and h. In particular G and H have the degrees of g and h, by Polynomial.Monic.natDegree_map. This is the coprime-factor form of Hensel's lemma for R⟦t⟧; for a field R it is the factor-splitting step of the Newton–Puiseux algorithm.

The proof is the classical coefficient recursion. A polynomial over R⟦t⟧ is rewritten as a power series in t whose coefficients are polynomials over R, through the ring homomorphism Polynomial.swapPowerSeries : R⟦X⟧[X] →+* R[X]⟦X⟧ (TauCeti.RingTheory.PowerSeries.Swap). Write G = Σ Gₖ tᵏ and H = Σ Hₖ tᵏ with G₀ = g and H₀ = h. The coefficient of tᵏ in G * H = P reads

g * Hₖ + h * Gₖ = Pₖ - Σ_{0 < i < k} Gᵢ * H_{k - i},

and, G and H being monic of the degrees of g and h, the corrections satisfy deg Gₖ < deg g and deg Hₖ < deg h for k ≥ 1. Writing u * g + v * h = 1, Bézout and division by g give the unique solution of this equation within those degree bounds (IsCoprime.exists_mem_degreeLT_mul_add_mul_eq, IsCoprime.eq_zero_of_mul_add_mul_eq_zero). Solving it for k = 1, 2, ... produces the factors one power of t at a time; uniqueness of each step gives uniqueness of the factorization.

Main results

• PowerSeries.eq_zero_of_mul_add_mul_eq_zero: if the constant coefficient of F₂ is monic and coprime to that of F₁, then F₂ * B + F₁ * A = 0 over R[X]⟦t⟧, with the coefficients of A of degree below that of the constant coefficient of F₂, forces A = 0 and B = 0.
• Polynomial.Monic.exists_monic_mul_eq_of_isCoprime: existence of the lifted factorization.
• Polynomial.Monic.eq_and_eq_of_mul_eq_mul_of_isCoprime: uniqueness of the lifted factorization.
• Polynomial.Monic.exists_monic_mul_eq_of_nextCoeff_map_eq_zero: over a field K, a monic polynomial over K⟦t⟧ whose reduction is depressed, splits, has invertible degree and is not a power of X factors into two monic factors of positive degree. This is the degree-lowering splitting step of the Newton–Puiseux algorithm, combining the coprime splitting of the reduction (Polynomial.Monic.exists_isCoprime_mul_eq_of_nextCoeff_eq_zero) with Hensel lifting.
• PowerSeries.henselianLocalRing: over a field K, K⟦t⟧ is a Henselian local ring, being complete for its maximal ideal (t).
• PowerSeries.exists_pow_eq_of_constantCoeff_eq_pow and PowerSeries.exists_pow_eq_of_isUnit: a unit of K⟦t⟧ whose constant coefficient is a nonzero n-th power, with n invertible in K, is an n-th power; over an algebraically closed field every unit of K⟦t⟧ has an n-th root for every n invertible in K.

References

• D. Eisenbud, Commutative Algebra with a View Toward Algebraic Geometry, Theorem 7.18, for Hensel's lemma over complete local rings by successive approximation.
• H. Mannaa and T. Coquand, Dynamic Newton–Puiseux Theorem, arXiv:1304.6770, §1, where the factor-lifting form of Hensel's lemma is the splitting step of the Newton–Puiseux algorithm.

theorem PowerSeries.eq_zero_of_mul_add_mul_eq_zero {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) {A B F₁ F₂ : PowerSeries (Polynomial R)} (hcop : IsCoprime g (constantCoeff F₁)) (hF₂ : constantCoeff F₂ = g) (hA : ∀ (k : ℕ), (coeff k) A ∈ Polynomial.degreeLT R g.natDegree) (h : F₂ * B + F₁ * A = 0) : A = 0 ∧ B = 0

If F₂ * B + F₁ * A = 0 for power series over R[X], where the constant coefficient g of F₂ is monic and coprime to that of F₁ and every coefficient of A has degree < deg g, then A = 0 and B = 0: the coefficient recursion of Hensel lifting has unique solutions.

theorem Polynomial.Monic.exists_monic_mul_eq_of_isCoprime {R : Type u_1} [CommRing R] {P : Polynomial (PowerSeries R)} (hP : P.Monic) {g h : Polynomial R} (hg : g.Monic) (hgh : IsCoprime g h) (hPgh : Polynomial.map PowerSeries.constantCoeff P = g * h) : ∃ (G : Polynomial (PowerSeries R)) (H : Polynomial (PowerSeries R)), G.Monic ∧ H.Monic ∧ Polynomial.map PowerSeries.constantCoeff G = g ∧ Polynomial.map PowerSeries.constantCoeff H = h ∧ G * H = P

A monic polynomial P over R⟦t⟧ whose reduction modulo t is a product g * h of coprime polynomials with g monic factors as P = G * H with G and H monic and reducing to g and h. This is the coprime-factor form of Hensel's lemma over R⟦t⟧; h is automatically monic, and the factors are unique by Polynomial.Monic.eq_and_eq_of_mul_eq_mul_of_isCoprime.

theorem Polynomial.Monic.eq_and_eq_of_mul_eq_mul_of_isCoprime {R : Type u_1} [CommRing R] {G G' H H' : Polynomial (PowerSeries R)} (hG : G.Monic) (hG' : G'.Monic) (hGG' : Polynomial.map PowerSeries.constantCoeff G = Polynomial.map PowerSeries.constantCoeff G') (hcop : IsCoprime (Polynomial.map PowerSeries.constantCoeff G) (Polynomial.map PowerSeries.constantCoeff H)) (h : G * H = G' * H') : G = G' ∧ H = H'

Uniqueness of Hensel lifting over R⟦t⟧: if G * H = G' * H' with G and G' monic and reducing modulo t to the same polynomial, coprime to the reduction of H, then G = G' and H = H'. No monicity of H or H' is needed.

theorem Polynomial.Monic.exists_monic_mul_eq_of_nextCoeff_map_eq_zero {K : Type u_1} [Field K] {P : Polynomial (PowerSeries K)} (hP : P.Monic) (hs : (Polynomial.map PowerSeries.constantCoeff P).Splits) (hm : ↑P.natDegree ≠ 0) (hnext : (Polynomial.map PowerSeries.constantCoeff P).nextCoeff = 0) (hX : Polynomial.map PowerSeries.constantCoeff P ≠ X ^ P.natDegree) : ∃ (G : Polynomial (PowerSeries K)) (H : Polynomial (PowerSeries K)), G.Monic ∧ H.Monic ∧ G * H = P ∧ 0 < G.natDegree ∧ 0 < H.natDegree

A monic polynomial P over K⟦t⟧ whose reduction modulo t has vanishing subleading coefficient, splits, has invertible degree and is not X ^ P.natDegree factors as P = G * H with G and H monic of positive degree. This is the splitting step of the Newton–Puiseux algorithm: the reduction splits into coprime monic factors of positive degree (Polynomial.Monic.exists_isCoprime_mul_eq_of_nextCoeff_eq_zero), and Hensel's lemma lifts them. In particular both factors have degree less than that of P, by Polynomial.Monic.natDegree_mul.

instance PowerSeries.henselianLocalRing {K : Type u_1} [Field K] : HenselianLocalRing (PowerSeries K)

Hensel's lemma for K⟦t⟧. Over a field K, the power series ring K⟦t⟧ is a Henselian local ring: it is complete for its maximal ideal (t), so this is Mathlib's IsAdicComplete.henselianRing at the maximal ideal, read through TauCeti.IsAdicComplete.henselianLocalRing.

theorem PowerSeries.exists_pow_eq_of_constantCoeff_eq_pow {K : Type u_1} [Field K] {n : ℕ} (hn : ↑n ≠ 0) {u : PowerSeries K} {c : K} (hc : c ≠ 0) (hu : constantCoeff u = c ^ n) : ∃ (v : PowerSeries K), v ^ n = u ∧ constantCoeff v = c

n-th roots of units in K⟦t⟧. If n is invertible in K and the constant coefficient of u is c ^ n for some c ≠ 0, then u has an n-th root with constant coefficient c, by Hensel's lemma applied to X ^ n - u at the approximate root c.

theorem PowerSeries.exists_pow_eq_of_isUnit {K : Type u_1} [Field K] [IsAlgClosed K] {n : ℕ} (hn : ↑n ≠ 0) {u : PowerSeries K} (hu : IsUnit u) : ∃ (v : PowerSeries K), v ^ n = u

Over an algebraically closed field K, every unit of K⟦t⟧ has an n-th root for every n invertible in K.