AlgebraicNumberTheory.Valuations.henselFactorization_extend_finite_prefix_one_step_of_mem_span
extend a finite Hensel prefix by one step in the displayed-factor principal-element form. The current iterates are automatically congruent to the initial lifts modulo (π), so the extension uses only π ∈ m and the displayed Bezout-error factor.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped Polynomial
namespace AlgebraicNumberTheory
namespace ValuationsLean source · statement
theorem henselFactorization_extend_finite_prefix_one_step_of_mem_span
{R : Type*} [CommRing R] [IsLocalRing R] [NoZeroDivisors R]
{π : R} (hπne : π ≠ 0)
(hπmem : π ∈ IsLocalRing.maximalIdeal R)
{f g0 h0 a b e : R[X]}
{gbar : (IsLocalRing.ResidueField R)[X]} {m d n : ℕ}
(hf : f.natDegree ≤ d)
(hg0map : g0.map (IsLocalRing.residue R) = gbar)
(hg0nat : g0.natDegree = m)
(hgbar_nat : gbar.natDegree = m)
(hglead : gbar.leadingCoeff ≠ 0)
(hh0 : h0.natDegree ≤ d - m)
(hbezFactor : a * g0 + b * h0 - 1 = Polynomial.C π * e)
(hmd : m ≤ d)
(pCorr qCorr : ℕ → R[X])
(hprefix :
∀ r : ℕ, r ≤ n →
∃ fr : R[X],
f - henselFactorization_henselIterate π g0 pCorr r *
henselFactorization_henselIterate π h0 qCorr r =
Polynomial.C (π ^ (r + 1)) * fr)
{fn : R[X]}
(hfactor :
f - henselFactorization_henselIterate π g0 pCorr n *
henselFactorization_henselIterate π h0 qCorr n =
Polynomial.C (π ^ (n + 1)) * fn)
(hgDeg : (henselFactorization_henselIterate π g0 pCorr n).natDegree ≤ m)
(hhDeg : (henselFactorization_henselIterate π h0 qCorr n).natDegree ≤ d - m) :
∃ p q fnNext : R[X],
p.natDegree ≤ m ∧ q.natDegree ≤ d - m ∧
(∀ r : ℕ, r ≤ n →
∃ fr : R[X],
f - henselFactorization_henselIterate π g0
(Function.update pCorr (n + 1) p) r *
henselFactorization_henselIterate π h0
(Function.update qCorr (n + 1) q) r =
Polynomial.C (π ^ (r + 1)) * fr) ∧
f - henselFactorization_henselIterate π g0
(Function.update pCorr (n + 1) p) (n + 1) *
henselFactorization_henselIterate π h0
(Function.update qCorr (n + 1) q) (n + 1) =
Polynomial.C (π ^ (n + 2)) * fnNext ∧
(henselFactorization_henselIterate π g0
(Function.update pCorr (n + 1) p) (n + 1)).natDegree ≤ m ∧
(henselFactorization_henselIterate π h0
(Function.update qCorr (n + 1) q) (n + 1)).natDegree ≤
d - m ∧
(∀ i : ℕ,
(henselFactorization_henselIterate π g0
(Function.update pCorr (n + 1) p) (n + 1) -
g0).coeff i ∈ IsLocalRing.maximalIdeal R) ∧
(∀ i : ℕ,
(henselFactorization_henselIterate π h0
(Function.update qCorr (n + 1) q) (n + 1) -
h0).coeff i ∈ IsLocalRing.maximalIdeal R)