Module

Step.lean

Nyll.ValuedFieldTheory.Valuation.Henselian.Factorization.Step

10 declarations indexed from sourceView source ↗

Module documentation

one Hensel iteration step

This file packages the algebraic correction, degree truncation, and π-power update into the single step used recursively in the proof of Hensel's lemma.

Imports2

Imported by10

theorem

henselFactorization_update_sub_eq_initial_error_add

L27 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_update_sub_eq_initial_error_add

Documentation

Algebraic splitting of an update by a π^n-multiple around the initial lift.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped Polynomial
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem henselFactorization_update_sub_eq_initial_error_add
    {R : Type*} [CommRing R] {π : R} {n : ℕ} {g g0 p : R[X]} :
    g + Polynomial.C (π ^ n) * p - g0 =
      (g - g0) + Polynomial.C (π ^ n) * p

theorem

henselFactorization_update_preserves_reduction_of_mem

L35 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_update_preserves_reduction_of_mem

Documentation

adding a π^n-multiple preserves the reduction modulo the maximal ideal once n ≥ 1 and π itself lies in the maximal ideal.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped Polynomial
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem henselFactorization_update_preserves_reduction_of_mem
    {R : Type*} [CommRing R] [IsLocalRing R] {π : R} {n : ℕ} (hn : 1 ≤ n)
    (hπ : π ∈ IsLocalRing.maximalIdeal R)
    {g g0 p : R[X]}
    (hg : ∀ i : ℕ, (g - g0).coeff i ∈ IsLocalRing.maximalIdeal R) :
    ∀ i : ℕ,
      (g + Polynomial.C (π ^ n) * p - g0).coeff i ∈
        IsLocalRing.maximalIdeal R

theorem

henselFactorization_update_preserves_span_singleton

L58 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_update_preserves_span_singleton

Documentation

adding a π^n-multiple preserves congruence modulo (π) once n ≥ 1. This is the inductive congruence needed for the displayed-factor one-step update.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped Polynomial
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem henselFactorization_update_preserves_span_singleton
    {R : Type*} [CommRing R] {π : R} {n : ℕ} (hn : 1 ≤ n)
    {g g0 p : R[X]}
    (hg : ∀ i : ℕ, (g - g0).coeff i ∈ Ideal.span ({π} : Set R)) :
    ∀ i : ℕ,
      (g + Polynomial.C (π ^ n) * p - g0).coeff i ∈
        Ideal.span ({π} : Set R)

theorem

henselFactorization_one_step_update_from_division_data_of_mem_le

L75 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_one_step_update_from_division_data_of_mem_le

Documentation

one recursive Hensel step from the division data, with the two uses of the principal element separated: π ∈ m preserves reductions, and m ≤ (π) reads the correction congruence modulo (π).

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped Polynomial
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem henselFactorization_one_step_update_from_division_data_of_mem_le
    {R : Type*} [CommRing R] [IsLocalRing R] {π : R} {n : ℕ} (hn : 1 ≤ n)
    (hπmem : π ∈ IsLocalRing.maximalIdeal R)
    (hπle : IsLocalRing.maximalIdeal R ≤ Ideal.span ({π} : Set R))
    {f g0 h0 g h fn a b qdiv p : R[X]} {m d : ℕ}
    (hfactor : f - g * h = Polynomial.C (π ^ n) * fn)
    (hg : ∀ i : ℕ, (g - g0).coeff i ∈ IsLocalRing.maximalIdeal R)
    (hh : ∀ i : ℕ, (h - h0).coeff i ∈ IsLocalRing.maximalIdeal R)
    (hgdeg : (g0.map (IsLocalRing.residue R)).natDegree = m)
    (hgnonzero : g0.map (IsLocalRing.residue R) ≠ 0)
    (hbez : (a * g0 + b * h0).map (IsLocalRing.residue R) = 1)
    (hdiv : b * fn = g0 * qdiv + p)
    (hfn : (fn.map (IsLocalRing.residue R)).natDegree ≤ d)
    (hh0 : (h0.map (IsLocalRing.residue R)).natDegree ≤ d - m)
    (hp : (p.map (IsLocalRing.residue R)).natDegree ≤ m)
    (hmd : m ≤ d) :
    (henselFactorization_lowPart (d - m) (a * fn + h0 * qdiv)).natDegree ≤ d - m ∧
      (∀ i : ℕ,
        (g + Polynomial.C (π ^ n) * p - g0).coeff i ∈
          IsLocalRing.maximalIdeal R) ∧
        (∀ i : ℕ,
          (h + Polynomial.C (π ^ n) *
              henselFactorization_lowPart (d - m) (a * fn + h0 * qdiv) - h0).coeff i ∈
            IsLocalRing.maximalIdeal R) ∧
          ∃ fnNext : R[X],
            f - (g + Polynomial.C (π ^ n) * p) *
                (h + Polynomial.C (π ^ n) *
                  henselFactorization_lowPart (d - m) (a * fn + h0 * qdiv)) =
              Polynomial.C (π ^ (n + 1)) * fnNext

theorem

henselFactorization_one_step_update_from_division_data_of_mem_span

L131 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_one_step_update_from_division_data_of_mem_span

Documentation

displayed-factor one recursive Hensel step from the division data. The congruence modulo (π) is produced from the displayed Bezout-error factor, and the update needs only π ∈ m, not m ≤ (π).

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped Polynomial
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem henselFactorization_one_step_update_from_division_data_of_mem_span
    {R : Type*} [CommRing R] [IsLocalRing R] {π : R} {n : ℕ} (hn : 1 ≤ n)
    (hπmem : π ∈ IsLocalRing.maximalIdeal R)
    {f g0 h0 g h fn a b qdiv p e : R[X]} {m d : ℕ}
    (hfactor : f - g * h = Polynomial.C (π ^ n) * fn)
    (hg : ∀ i : ℕ, (g - g0).coeff i ∈ Ideal.span ({π} : Set R))
    (hh : ∀ i : ℕ, (h - h0).coeff i ∈ Ideal.span ({π} : Set R))
    (hgunit : IsUnit g0.leadingCoeff)
    (hg0nat : g0.natDegree = m)
    (hbezFactor : a * g0 + b * h0 - 1 = Polynomial.C π * e)
    (hdiv : b * fn = g0 * qdiv + p)
    (hfn : fn.natDegree ≤ d)
    (hh0 : h0.natDegree ≤ d - m)
    (hp : p.natDegree ≤ m)
    (hmd : m ≤ d) :
    (henselFactorization_lowPart (d - m) (a * fn + h0 * qdiv)).natDegree ≤ d - m ∧
      (∀ i : ℕ,
        (g + Polynomial.C (π ^ n) * p - g0).coeff i ∈
          Ideal.span ({π} : Set R)) ∧
        (∀ i : ℕ,
          (h + Polynomial.C (π ^ n) *
              henselFactorization_lowPart (d - m) (a * fn + h0 * qdiv) - h0).coeff i ∈
            Ideal.span ({π} : Set R)) ∧
          (∀ i : ℕ,
            (g + Polynomial.C (π ^ n) * p - g0).coeff i ∈
              IsLocalRing.maximalIdeal R) ∧
            (∀ i : ℕ,
              (h + Polynomial.C (π ^ n) *
                  henselFactorization_lowPart (d - m) (a * fn + h0 * qdiv) - h0).coeff i ∈
                IsLocalRing.maximalIdeal R) ∧
              ∃ fnNext : R[X],
                f - (g + Polynomial.C (π ^ n) * p) *
                    (h + Polynomial.C (π ^ n) *
                      henselFactorization_lowPart (d - m) (a * fn + h0 * qdiv)) =
                  Polynomial.C (π ^ (n + 1)) * fnNext

theorem

henselFactorization_one_step_update_from_division_degree_lt_of_mem_le

L203 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_one_step_update_from_division_degree_lt_of_mem_le

Documentation

one recursive Hensel step from the actual division remainder estimate, with the principal-element assumptions separated.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped Polynomial
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem henselFactorization_one_step_update_from_division_degree_lt_of_mem_le
    {R : Type*} [CommRing R] [IsLocalRing R] {π : R} {n : ℕ} (hn : 1 ≤ n)
    (hπmem : π ∈ IsLocalRing.maximalIdeal R)
    (hπle : IsLocalRing.maximalIdeal R ≤ Ideal.span ({π} : Set R))
    {f g0 h0 g h fn a b qdiv p : R[X]} {m d : ℕ}
    (hfactor : f - g * h = Polynomial.C (π ^ n) * fn)
    (hg : ∀ i : ℕ, (g - g0).coeff i ∈ IsLocalRing.maximalIdeal R)
    (hh : ∀ i : ℕ, (h - h0).coeff i ∈ IsLocalRing.maximalIdeal R)
    (hgdeg : (g0.map (IsLocalRing.residue R)).natDegree = m)
    (hg0nat : g0.natDegree = m)
    (hgnonzero : g0.map (IsLocalRing.residue R) ≠ 0)
    (hbez : (a * g0 + b * h0).map (IsLocalRing.residue R) = 1)
    (hdiv : b * fn = g0 * qdiv + p)
    (hpdeg : p.degree < g0.degree)
    (hfn : (fn.map (IsLocalRing.residue R)).natDegree ≤ d)
    (hh0 : (h0.map (IsLocalRing.residue R)).natDegree ≤ d - m)
    (hmd : m ≤ d) :
    (henselFactorization_lowPart (d - m) (a * fn + h0 * qdiv)).natDegree ≤ d - m ∧
      (∀ i : ℕ,
        (g + Polynomial.C (π ^ n) * p - g0).coeff i ∈
          IsLocalRing.maximalIdeal R) ∧
        (∀ i : ℕ,
          (h + Polynomial.C (π ^ n) *
              henselFactorization_lowPart (d - m) (a * fn + h0 * qdiv) - h0).coeff i ∈
            IsLocalRing.maximalIdeal R) ∧
          ∃ fnNext : R[X],
            f - (g + Polynomial.C (π ^ n) * p) *
                (h + Polynomial.C (π ^ n) *
                  henselFactorization_lowPart (d - m) (a * fn + h0 * qdiv)) =
              Polynomial.C (π ^ (n + 1)) * fnNext

theorem

henselFactorization_exists_one_step_update_of_mem_le

L241 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_exists_one_step_update_of_mem_le

Documentation

existence of one recursive Hensel step from the current error factor, with the principal-element assumptions separated.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped Polynomial
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem henselFactorization_exists_one_step_update_of_mem_le
    {R : Type*} [CommRing R] [IsLocalRing R] [NoZeroDivisors R]
    {π : R} {n : ℕ} (hn : 1 ≤ n) (hπn : π ^ n ≠ 0)
    (hπmem : π ∈ IsLocalRing.maximalIdeal R)
    (hπle : IsLocalRing.maximalIdeal R ≤ Ideal.span ({π} : Set R))
    {f g0 h0 g h fn a b : R[X]}
    {gbar : (IsLocalRing.ResidueField R)[X]} {m d : ℕ}
    (hf : f.natDegree ≤ d)
    (hg : ∀ i : ℕ, (g - g0).coeff i ∈ IsLocalRing.maximalIdeal R)
    (hh : ∀ i : ℕ, (h - h0).coeff i ∈ IsLocalRing.maximalIdeal R)
    (hgdeg : g.natDegree ≤ m)
    (hhdeg : h.natDegree ≤ d - m)
    (hg0map : g0.map (IsLocalRing.residue R) = gbar)
    (hg0nat : g0.natDegree = m)
    (hgbar_nat : gbar.natDegree = m)
    (hglead : gbar.leadingCoeff ≠ 0)
    (hh0 : (h0.map (IsLocalRing.residue R)).natDegree ≤ d - m)
    (hbez : (a * g0 + b * h0).map (IsLocalRing.residue R) = 1)
    (hfactor : f - g * h = Polynomial.C (π ^ n) * fn)
    (hmd : m ≤ d) :
    ∃ p q fnNext : R[X],
      p.natDegree ≤ m ∧ q.natDegree ≤ d - m ∧
        (∀ i : ℕ,
          (g + Polynomial.C (π ^ n) * p - g0).coeff i ∈
            IsLocalRing.maximalIdeal R) ∧
          (∀ i : ℕ,
            (h + Polynomial.C (π ^ n) * q - h0).coeff i ∈
              IsLocalRing.maximalIdeal R) ∧
            f - (g + Polynomial.C (π ^ n) * p) *
                (h + Polynomial.C (π ^ n) * q) =
              Polynomial.C (π ^ (n + 1)) * fnNext

theorem

henselFactorization_exists_one_step_update_of_mem_span

L302 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_exists_one_step_update_of_mem_span

Documentation

existence of one recursive Hensel step from the current error factor in the displayed-factor principal-element form. The chosen π only has to lie in the maximal ideal; the needed congruence modulo (π) is carried as an invariant and is produced from the displayed finite-minimum 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 Valuations

Lean source · statement

theorem henselFactorization_exists_one_step_update_of_mem_span
    {R : Type*} [CommRing R] [IsLocalRing R] [NoZeroDivisors R]
    {π : R} {n : ℕ} (hn : 1 ≤ n) (hπn : π ^ n ≠ 0)
    (hπmem : π ∈ IsLocalRing.maximalIdeal R)
    {f g0 h0 g h fn a b e : R[X]}
    {gbar : (IsLocalRing.ResidueField R)[X]} {m d : ℕ}
    (hf : f.natDegree ≤ d)
    (hg : ∀ i : ℕ, (g - g0).coeff i ∈ Ideal.span ({π} : Set R))
    (hh : ∀ i : ℕ, (h - h0).coeff i ∈ Ideal.span ({π} : Set R))
    (hgdeg : g.natDegree ≤ m)
    (hhdeg : h.natDegree ≤ d - m)
    (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)
    (hfactor : f - g * h = Polynomial.C (π ^ n) * fn)
    (hmd : m ≤ d) :
    ∃ p q fnNext : R[X],
      p.natDegree ≤ m ∧ q.natDegree ≤ d - m ∧
        (∀ i : ℕ,
          (g + Polynomial.C (π ^ n) * p - g0).coeff i ∈
            Ideal.span ({π} : Set R)) ∧
          (∀ i : ℕ,
            (h + Polynomial.C (π ^ n) * q - h0).coeff i ∈
              Ideal.span ({π} : Set R)) ∧
            (∀ i : ℕ,
              (g + Polynomial.C (π ^ n) * p - g0).coeff i ∈
                IsLocalRing.maximalIdeal R) ∧
              (∀ i : ℕ,
                (h + Polynomial.C (π ^ n) * q - h0).coeff i ∈
                  IsLocalRing.maximalIdeal R) ∧
                f - (g + Polynomial.C (π ^ n) * p) *
                    (h + Polynomial.C (π ^ n) * q) =
                  Polynomial.C (π ^ (n + 1)) * fnNext

theorem

henselFactorization_exists_one_step_update_with_degree_bounds_of_mem_span

L362 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_exists_one_step_update_with_degree_bounds_of_mem_span

Documentation

displayed-factor one-step existence with the degree invariants for the next approximants included.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped Polynomial
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem henselFactorization_exists_one_step_update_with_degree_bounds_of_mem_span
    {R : Type*} [CommRing R] [IsLocalRing R] [NoZeroDivisors R]
    {π : R} {n : ℕ} (hn : 1 ≤ n) (hπn : π ^ n ≠ 0)
    (hπmem : π ∈ IsLocalRing.maximalIdeal R)
    {f g0 h0 g h fn a b e : R[X]}
    {gbar : (IsLocalRing.ResidueField R)[X]} {m d : ℕ}
    (hf : f.natDegree ≤ d)
    (hg : ∀ i : ℕ, (g - g0).coeff i ∈ Ideal.span ({π} : Set R))
    (hh : ∀ i : ℕ, (h - h0).coeff i ∈ Ideal.span ({π} : Set R))
    (hgdeg : g.natDegree ≤ m)
    (hhdeg : h.natDegree ≤ d - m)
    (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)
    (hfactor : f - g * h = Polynomial.C (π ^ n) * fn)
    (hmd : m ≤ d) :
    ∃ p q fnNext : R[X],
      p.natDegree ≤ m ∧ q.natDegree ≤ d - m ∧
        (g + Polynomial.C (π ^ n) * p).natDegree ≤ m ∧
          (h + Polynomial.C (π ^ n) * q).natDegree ≤ d - m ∧
            (∀ i : ℕ,
              (g + Polynomial.C (π ^ n) * p - g0).coeff i ∈
                Ideal.span ({π} : Set R)) ∧
              (∀ i : ℕ,
                (h + Polynomial.C (π ^ n) * q - h0).coeff i ∈
                  Ideal.span ({π} : Set R)) ∧
                (∀ i : ℕ,
                  (g + Polynomial.C (π ^ n) * p - g0).coeff i ∈
                    IsLocalRing.maximalIdeal R) ∧
                  (∀ i : ℕ,
                    (h + Polynomial.C (π ^ n) * q - h0).coeff i ∈
                      IsLocalRing.maximalIdeal R) ∧
                    f - (g + Polynomial.C (π ^ n) * p) *
                        (h + Polynomial.C (π ^ n) * q) =
                      Polynomial.C (π ^ (n + 1)) * fnNext

theorem

henselFactorization_exists_one_step_update_with_degree_bounds_of_mem_le

L421 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_exists_one_step_update_with_degree_bounds_of_mem_le

Documentation

existence of one recursive Hensel step with the degree invariants for the next approximants included, with the principal-element assumptions separated.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped Polynomial
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem henselFactorization_exists_one_step_update_with_degree_bounds_of_mem_le
    {R : Type*} [CommRing R] [IsLocalRing R] [NoZeroDivisors R]
    {π : R} {n : ℕ} (hn : 1 ≤ n) (hπn : π ^ n ≠ 0)
    (hπmem : π ∈ IsLocalRing.maximalIdeal R)
    (hπle : IsLocalRing.maximalIdeal R ≤ Ideal.span ({π} : Set R))
    {f g0 h0 g h fn a b : R[X]}
    {gbar : (IsLocalRing.ResidueField R)[X]} {m d : ℕ}
    (hf : f.natDegree ≤ d)
    (hg : ∀ i : ℕ, (g - g0).coeff i ∈ IsLocalRing.maximalIdeal R)
    (hh : ∀ i : ℕ, (h - h0).coeff i ∈ IsLocalRing.maximalIdeal R)
    (hgdeg : g.natDegree ≤ m)
    (hhdeg : h.natDegree ≤ d - m)
    (hg0map : g0.map (IsLocalRing.residue R) = gbar)
    (hg0nat : g0.natDegree = m)
    (hgbar_nat : gbar.natDegree = m)
    (hglead : gbar.leadingCoeff ≠ 0)
    (hh0 : (h0.map (IsLocalRing.residue R)).natDegree ≤ d - m)
    (hbez : (a * g0 + b * h0).map (IsLocalRing.residue R) = 1)
    (hfactor : f - g * h = Polynomial.C (π ^ n) * fn)
    (hmd : m ≤ d) :
    ∃ p q fnNext : R[X],
      p.natDegree ≤ m ∧ q.natDegree ≤ d - m ∧
        (g + Polynomial.C (π ^ n) * p).natDegree ≤ m ∧
          (h + Polynomial.C (π ^ n) * q).natDegree ≤ d - m ∧
            (∀ i : ℕ,
              (g + Polynomial.C (π ^ n) * p - g0).coeff i ∈
                IsLocalRing.maximalIdeal R) ∧
              (∀ i : ℕ,
                (h + Polynomial.C (π ^ n) * q - h0).coeff i ∈
                  IsLocalRing.maximalIdeal R) ∧
                f - (g + Polynomial.C (π ^ n) * p) *
                    (h + Polynomial.C (π ^ n) * q) =
                  Polynomial.C (π ^ (n + 1)) * fnNext

Module documentation

one Hensel iteration step

Declarations