instance
completeDVR_henselianLocalRing
{A : Type u_1}
[CommRing A]
[IsDomain A]
[IsDiscreteValuationRing A]
[IsAdicComplete (IsLocalRing.maximalIdeal A) A]
:
theorem
hensel_simple_root_lift
{A : Type u_1}
[CommRing A]
[IsDomain A]
[IsDiscreteValuationRing A]
[IsAdicComplete (IsLocalRing.maximalIdeal A) A]
(f : Polynomial A)
(hf : f.Monic)
(a_bar : IsLocalRing.ResidueField A)
(hroot : (Polynomial.aeval a_bar) f = 0)
(hsimple : (Polynomial.aeval a_bar) (Polynomial.derivative f) ≠ 0)
:
∃ (a : A), f.IsRoot a ∧ (IsLocalRing.residue A) a = a_bar
theorem
hensel_newton
{A : Type u_1}
[CommRing A]
[IsDomain A]
[IsDiscreteValuationRing A]
[IsAdicComplete (IsLocalRing.maximalIdeal A) A]
(f : Polynomial A)
(a₀ : A)
(h₁ : Polynomial.eval a₀ f ∈ IsLocalRing.maximalIdeal A)
(h₂ : IsUnit (Polynomial.eval a₀ (Polynomial.derivative f)))
:
∃ (a : A), f.IsRoot a ∧ a - a₀ ∈ IsLocalRing.maximalIdeal A
theorem
hensel_newton_valuation
{A : Type u_1}
[CommRing A]
[IsDomain A]
[IsDiscreteValuationRing A]
[IsAdicComplete (IsLocalRing.maximalIdeal A) A]
(f : Polynomial A)
(a₀ : A)
(hval :
(IsDiscreteValuationRing.addVal A) (Polynomial.eval a₀ f) > 2 * (IsDiscreteValuationRing.addVal A) (Polynomial.eval a₀ (Polynomial.derivative f)))
:
∃ (a : A), f.IsRoot a ∧ a - a₀ ∈ IsLocalRing.maximalIdeal A
theorem
isUnit_one_add_mul_of_mem_maximalIdeal
{A : Type u_1}
[CommRing A]
[IsDomain A]
[IsDiscreteValuationRing A]
{c b : A}
(hb : b ∈ IsLocalRing.maximalIdeal A)
:
theorem
addVal_add_eq_of_lt
{A : Type u_1}
[CommRing A]
[IsDomain A]
[IsDiscreteValuationRing A]
{a b : A}
(h : (IsDiscreteValuationRing.addVal A) a < (IsDiscreteValuationRing.addVal A) b)
:
theorem
addVal_eval_sub_ge
{A : Type u_1}
[CommRing A]
[IsDomain A]
[IsDiscreteValuationRing A]
(p : Polynomial A)
(a a₀ : A)
:
(IsDiscreteValuationRing.addVal A) (a - a₀) ≤ (IsDiscreteValuationRing.addVal A) (Polynomial.eval a p - Polynomial.eval a₀ p)
theorem
hensel_newton_derivative_stability
{A : Type u_1}
[CommRing A]
[IsDomain A]
[IsDiscreteValuationRing A]
[IsAdicComplete (IsLocalRing.maximalIdeal A) A]
(f : Polynomial A)
(a a₀ : A)
(hva :
(IsDiscreteValuationRing.addVal A) (Polynomial.eval a₀ (Polynomial.derivative f)) < (IsDiscreteValuationRing.addVal A) (a - a₀))
:
theorem
hensel_newton_root_unique
{A : Type u_1}
[CommRing A]
[IsDomain A]
[IsDiscreteValuationRing A]
(f : Polynomial A)
(a a' a₀ : A)
(hfa : f.IsRoot a)
(hfa' : f.IsRoot a')
(hva :
(IsDiscreteValuationRing.addVal A) (Polynomial.eval a₀ (Polynomial.derivative f)) < (IsDiscreteValuationRing.addVal A) (a - a₀))
(hva' :
(IsDiscreteValuationRing.addVal A) (Polynomial.eval a₀ (Polynomial.derivative f)) < (IsDiscreteValuationRing.addVal A) (a' - a₀))
:
theorem
addVal_lt_addVal_mul_of_mem_maximalIdeal
{A : Type u_1}
[CommRing A]
[IsDomain A]
[IsDiscreteValuationRing A]
{d q : A}
(hd : d ≠ 0)
(hq : q ∈ IsLocalRing.maximalIdeal A)
(_hq0 : q ≠ 0)
:
theorem
hensel_newton_valuation_full
{A : Type u_1}
[CommRing A]
[IsDomain A]
[IsDiscreteValuationRing A]
[IsAdicComplete (IsLocalRing.maximalIdeal A) A]
(f : Polynomial A)
(a₀ : A)
(hval :
(IsDiscreteValuationRing.addVal A) (Polynomial.eval a₀ f) > 2 * (IsDiscreteValuationRing.addVal A) (Polynomial.eval a₀ (Polynomial.derivative f)))
:
∃ (a : A),
f.IsRoot a ∧ a - a₀ ∈ IsLocalRing.maximalIdeal A ∧ (IsDiscreteValuationRing.addVal A) (a - a₀) + 2 * (IsDiscreteValuationRing.addVal A) (Polynomial.eval a₀ (Polynomial.derivative f)) ≥ (IsDiscreteValuationRing.addVal A) (Polynomial.eval a₀ f) ∧ (∀ (a' : A),
f.IsRoot a' →
(IsDiscreteValuationRing.addVal A) (Polynomial.eval a₀ (Polynomial.derivative f)) < (IsDiscreteValuationRing.addVal A) (a' - a₀) →
a' = a) ∧ (IsDiscreteValuationRing.addVal A) (Polynomial.eval a (Polynomial.derivative f)) = (IsDiscreteValuationRing.addVal A) (Polynomial.eval a₀ (Polynomial.derivative f))