Hensel splitting for polynomials over power series

In this file we derive from the Weierstrass preparation theorem (PowerSeries.exists_isWeierstrassFactorization) a Hensel-style splitting for a monic polynomial p over K⟦X⟧: a root of multiplicity k of the reduction of p modulo the maximal ideal of K⟦X⟧ (that is, of the coefficientwise application of PowerSeries.constantCoeff to p) lifts to a monic factor of p of degree k.

Main results

• Polynomial.Monic.exists_factorization_rootMultiplicity_zero: a monic p over K⟦X⟧ of degree m whose reduction has 0 as a root of multiplicity k with k ≤ m factors as p = g * h with g, h monic of degrees k and m - k, and the reduction of g is X ^ k.

• Polynomial.Monic.exists_factorization_rootMultiplicity: a monic p over K⟦X⟧ of degree m whose reduction has a root a : K of multiplicity k with k ≤ m factors as p = g * h with g, h monic of degrees k and m - k.

theorem Polynomial.Monic.exists_factorization_rootMultiplicity_zero {K : Type u_1} [Field K] {p : Polynomial (PowerSeries K)} {m k : ℕ} (hp : p.Monic) (hm : p.natDegree = m) (hk : rootMultiplicity 0 (Polynomial.map PowerSeries.constantCoeff p) = k) (hkm : k ≤ m) : ∃ (g : Polynomial (PowerSeries K)) (h : Polynomial (PowerSeries K)), g.Monic ∧ h.Monic ∧ p = g * h ∧ g.natDegree = k ∧ h.natDegree = m - k ∧ Polynomial.map PowerSeries.constantCoeff g = X ^ k

Hensel splitting at zero: a monic p over K⟦X⟧ of degree m whose reduction (coefficientwise PowerSeries.constantCoeff) has 0 as a root of multiplicity k with k ≤ m factors as p = g * h with g, h monic of degrees k and m - k, and g distinguished: its reduction is X ^ k.

theorem Polynomial.Monic.exists_factorization_rootMultiplicity {K : Type u_1} [Field K] {p : Polynomial (PowerSeries K)} {m k : ℕ} {a : K} (hp : p.Monic) (hm : p.natDegree = m) (hk : rootMultiplicity a (Polynomial.map PowerSeries.constantCoeff p) = k) (hkm : k ≤ m) : ∃ (g : Polynomial (PowerSeries K)) (h : Polynomial (PowerSeries K)), g.Monic ∧ h.Monic ∧ p = g * h ∧ g.natDegree = k ∧ h.natDegree = m - k

Hensel splitting at a root: a monic p over K⟦X⟧ of degree m whose reduction (coefficientwise PowerSeries.constantCoeff) has a root a : K of multiplicity k with k ≤ m factors as p = g * h with g, h monic of degrees k and m - k.