Module

InfiniteApproximation.lean

Nyll.ValuedFieldTheory.Valuation.Henselian.Factorization.InfiniteApproximation

22 declarations indexed from sourceView source ↗

Module documentation

compatible Hensel prefixes

This file turns the finite Hensel-prefix construction into a recursive family of compatible prefixes. The completion/limit argument is kept for the next layer.

Imports1

Nyll.ValuedFieldTheory.Valuation.Henselian.Factorization.FiniteApproximation

Imported by11

structure

HenselFactorizationFinitePrefixState

L27 ↗

AlgebraicNumberTheory.Valuations.HenselFactorizationFinitePrefixState

Documentation

the data carried by a finite Hensel prefix at stage N. The fields are exactly the invariants needed to extend the prefix one more step and later pass to the complete limit.

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 · full declaration

structure HenselFactorizationFinitePrefixState
    {R : Type*} [CommRing R] [IsLocalRing R] (π : R)
    (f g0 h0 : R[X]) (m d N : ℕ) where
  /-- The polynomial corrections for the first factor at each stage. -/
  pCorr : ℕ → R[X]
  /-- The polynomial corrections for the second factor at each stage. -/
  qCorr : ℕ → R[X]
  /-- The residual error polynomial at the current stage. -/
  fErr : R[X]
  /-- Every prefix through the current stage factors the error by the corresponding power of `π`. -/
  prefixFactor :
    ∀ r : ℕ, r ≤ N →
      ∃ fr : R[X],
        f - henselFactorization_henselIterate π g0 pCorr r *
            henselFactorization_henselIterate π h0 qCorr r =
          Polynomial.C (π ^ (r + 1)) * fr
  /-- Each correction for the first factor has degree at most `m`. -/
  pCorrDeg : ∀ r : ℕ, (pCorr r).natDegree ≤ m
  /-- Each correction for the second factor has degree at most `d - m`. -/
  qCorrDeg : ∀ r : ℕ, (qCorr r).natDegree ≤ d - m
  /-- At stage `N`, the factorization error is `π ^ (N + 1)` times `fErr`. -/
  factor :
    f - henselFactorization_henselIterate π g0 pCorr N *
        henselFactorization_henselIterate π h0 qCorr N =
      Polynomial.C (π ^ (N + 1)) * fErr
  /-- The first approximate factor at stage `N` has degree at most `m`. -/
  gDeg : (henselFactorization_henselIterate π g0 pCorr N).natDegree ≤ m
  /-- The second approximate factor at stage `N` has degree at most `d - m`. -/
  hDeg : (henselFactorization_henselIterate π h0 qCorr N).natDegree ≤ d - m
  /-- The first approximate factor remains congruent to `g0` modulo the maximal ideal. -/
  gRed :
    ∀ i : ℕ,
      (henselFactorization_henselIterate π g0 pCorr N - g0).coeff i ∈
        IsLocalRing.maximalIdeal R
  /-- The second approximate factor remains congruent to `h0` modulo the maximal ideal. -/
  hRed :
    ∀ i : ℕ,
      (henselFactorization_henselIterate π h0 qCorr N - h0).coeff i ∈
        IsLocalRing.maximalIdeal R

def

henselFactorization_initialPrefixState_of_factor

L69 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_initialPrefixState_of_factor

Documentation

the stage 0 prefix state from a displayed finite-minimum factor of the initial error.

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

def henselFactorization_initialPrefixState_of_factor
    {R : Type*} [CommRing R] [IsLocalRing R]
    {π : R} {f g0 h0 f1 : R[X]} {m d : ℕ}
    (hfactor0 : f - g0 * h0 = Polynomial.C π * f1)
    (hg0nat : g0.natDegree = m)
    (hh0deg : h0.natDegree ≤ d - m) :
    HenselFactorizationFinitePrefixState π f g0 h0 m d 0

def

henselFactorization_chosenNextPrefixState_of_mem_span

L106 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_chosenNextPrefixState_of_mem_span

Documentation

Choose an extension of a prefix state by one Hensel correction in the displayed-factor form.

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

def henselFactorization_chosenNextPrefixState_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)
    (hh0deg : h0.natDegree ≤ d - m)
    (hbezFactor : a * g0 + b * h0 - 1 = Polynomial.C π * e)
    (hmd : m ≤ d)
    (s : HenselFactorizationFinitePrefixState π f g0 h0 m d N) :
    HenselFactorizationFinitePrefixState π f g0 h0 m d (N + 1)

theorem

henselFactorization_chosenNextPrefixState_pCorr_of_ne_of_mem_span

L195 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_chosenNextPrefixState_pCorr_of_ne_of_mem_span

Documentation

in the displayed-factor prefix extension the p correction changes only at the newly constructed index.

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_chosenNextPrefixState_pCorr_of_ne_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 r : ℕ}
    (hf : f.natDegree ≤ d)
    (hg0map : g0.map (IsLocalRing.residue R) = gbar)
    (hg0nat : g0.natDegree = m)
    (hgbar_nat : gbar.natDegree = m)
    (hglead : gbar.leadingCoeff ≠ 0)
    (hh0deg : h0.natDegree ≤ d - m)
    (hbezFactor : a * g0 + b * h0 - 1 = Polynomial.C π * e)
    (hmd : m ≤ d)
    (s : HenselFactorizationFinitePrefixState π f g0 h0 m d N)
    (hr : r ≠ N + 1) :
    (henselFactorization_chosenNextPrefixState_of_mem_span
        (π := π) hπne hπmem
        (f := f) (g0 := g0) (h0 := h0) (a := a) (b := b) (e := e)
        (gbar := gbar) (m := m) (d := d) (N := N)
        hf hg0map hg0nat hgbar_nat hglead hh0deg hbezFactor hmd s).pCorr r =
      s.pCorr r

theorem

henselFactorization_chosenNextPrefixState_qCorr_of_ne_of_mem_span

L222 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_chosenNextPrefixState_qCorr_of_ne_of_mem_span

Documentation

in the displayed-factor prefix extension the q correction changes only at the newly constructed index.

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_chosenNextPrefixState_qCorr_of_ne_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 r : ℕ}
    (hf : f.natDegree ≤ d)
    (hg0map : g0.map (IsLocalRing.residue R) = gbar)
    (hg0nat : g0.natDegree = m)
    (hgbar_nat : gbar.natDegree = m)
    (hglead : gbar.leadingCoeff ≠ 0)
    (hh0deg : h0.natDegree ≤ d - m)
    (hbezFactor : a * g0 + b * h0 - 1 = Polynomial.C π * e)
    (hmd : m ≤ d)
    (s : HenselFactorizationFinitePrefixState π f g0 h0 m d N)
    (hr : r ≠ N + 1) :
    (henselFactorization_chosenNextPrefixState_of_mem_span
        (π := π) hπne hπmem
        (f := f) (g0 := g0) (h0 := h0) (a := a) (b := b) (e := e)
        (gbar := gbar) (m := m) (d := d) (N := N)
        hf hg0map hg0nat hgbar_nat hglead hh0deg hbezFactor hmd s).qCorr r =
      s.qCorr r

def

henselFactorization_prefixStateSeq_of_mem_span

L249 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_prefixStateSeq_of_mem_span

Documentation

recursively chosen compatible finite Hensel prefixes in the displayed-factor displayed-factor form.

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 · full declaration

def henselFactorization_prefixStateSeq_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 f1 e : R[X]}
    {gbar : (IsLocalRing.ResidueField R)[X]} {m d : ℕ}
    (hf : f.natDegree ≤ d)
    (hg0map : g0.map (IsLocalRing.residue R) = gbar)
    (hg0nat : g0.natDegree = m)
    (hgbar_nat : gbar.natDegree = m)
    (hglead : gbar.leadingCoeff ≠ 0)
    (hh0deg : h0.natDegree ≤ d - m)
    (hfactor0 : f - g0 * h0 = Polynomial.C π * f1)
    (hbezFactor : a * g0 + b * h0 - 1 = Polynomial.C π * e)
    (hmd : m ≤ d) :
    (N : ℕ) → HenselFactorizationFinitePrefixState π f g0 h0 m d N
  | 0 =>
      henselFactorization_initialPrefixState_of_factor
        (π := π) (f := f) (g0 := g0) (h0 := h0)
        (f1 := f1) (m := m) (d := d)
        hfactor0 hg0nat hh0deg
  | N + 1 =>
      henselFactorization_chosenNextPrefixState_of_mem_span
        (π := π) hπne hπmem
        (f := f) (g0 := g0) (h0 := h0) (a := a) (b := b) (e := e)
        (gbar := gbar) (m := m) (d := d) (N := N)
        hf hg0map hg0nat hgbar_nat hglead hh0deg hbezFactor hmd
        (henselFactorization_prefixStateSeq_of_mem_span
          (π := π) (f := f) (g0 := g0) (h0 := h0)
          (a := a) (b := b) (f1 := f1) (e := e)
          (gbar := gbar) (m := m) (d := d)
          hπne hπmem hf hg0map hg0nat hgbar_nat hglead hh0deg
          hfactor0 hbezFactor hmd N)

theorem

henselFactorization_prefixStateSeq_pCorr_eq_of_le_of_mem_span

L286 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_prefixStateSeq_pCorr_eq_of_le_of_mem_span

Documentation

coherence of the displayed-factor p-corrections: later prefix states agree with earlier ones at every already constructed index.

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_prefixStateSeq_pCorr_eq_of_le_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 f1 e : R[X]}
    {gbar : (IsLocalRing.ResidueField R)[X]} {m d : ℕ}
    (hf : f.natDegree ≤ d)
    (hg0map : g0.map (IsLocalRing.residue R) = gbar)
    (hg0nat : g0.natDegree = m)
    (hgbar_nat : gbar.natDegree = m)
    (hglead : gbar.leadingCoeff ≠ 0)
    (hh0deg : h0.natDegree ≤ d - m)
    (hfactor0 : f - g0 * h0 = Polynomial.C π * f1)
    (hbezFactor : a * g0 + b * h0 - 1 = Polynomial.C π * e)
    (hmd : m ≤ d) :
    ∀ {M N : ℕ}, M ≤ N →
      (henselFactorization_prefixStateSeq_of_mem_span
          (π := π) (f := f) (g0 := g0) (h0 := h0)
          (a := a) (b := b) (f1 := f1) (e := e)
          (gbar := gbar) (m := m) (d := d)
          hπne hπmem hf hg0map hg0nat hgbar_nat hglead hh0deg
          hfactor0 hbezFactor hmd N).pCorr M =
        (henselFactorization_prefixStateSeq_of_mem_span
          (π := π) (f := f) (g0 := g0) (h0 := h0)
          (a := a) (b := b) (f1 := f1) (e := e)
          (gbar := gbar) (m := m) (d := d)
          hπne hπmem hf hg0map hg0nat hgbar_nat hglead hh0deg
          hfactor0 hbezFactor hmd M).pCorr M

theorem

henselFactorization_prefixStateSeq_qCorr_eq_of_le_of_mem_span

L364 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_prefixStateSeq_qCorr_eq_of_le_of_mem_span

Documentation

coherence of the displayed-factor q-corrections: later prefix states agree with earlier ones at every already constructed index.

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_prefixStateSeq_qCorr_eq_of_le_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 f1 e : R[X]}
    {gbar : (IsLocalRing.ResidueField R)[X]} {m d : ℕ}
    (hf : f.natDegree ≤ d)
    (hg0map : g0.map (IsLocalRing.residue R) = gbar)
    (hg0nat : g0.natDegree = m)
    (hgbar_nat : gbar.natDegree = m)
    (hglead : gbar.leadingCoeff ≠ 0)
    (hh0deg : h0.natDegree ≤ d - m)
    (hfactor0 : f - g0 * h0 = Polynomial.C π * f1)
    (hbezFactor : a * g0 + b * h0 - 1 = Polynomial.C π * e)
    (hmd : m ≤ d) :
    ∀ {M N : ℕ}, M ≤ N →
      (henselFactorization_prefixStateSeq_of_mem_span
          (π := π) (f := f) (g0 := g0) (h0 := h0)
          (a := a) (b := b) (f1 := f1) (e := e)
          (gbar := gbar) (m := m) (d := d)
          hπne hπmem hf hg0map hg0nat hgbar_nat hglead hh0deg
          hfactor0 hbezFactor hmd N).qCorr M =
        (henselFactorization_prefixStateSeq_of_mem_span
          (π := π) (f := f) (g0 := g0) (h0 := h0)
          (a := a) (b := b) (f1 := f1) (e := e)
          (gbar := gbar) (m := m) (d := d)
          hπne hπmem hf hg0map hg0nat hgbar_nat hglead hh0deg
          hfactor0 hbezFactor hmd M).qCorr M

def

henselFactorization_infinitePCorr_of_mem_span

L441 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_infinitePCorr_of_mem_span

Documentation

the infinite p-correction sequence from the displayed-factor displayed-factor prefix construction.

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

def henselFactorization_infinitePCorr_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 f1 e : R[X]}
    {gbar : (IsLocalRing.ResidueField R)[X]} {m d : ℕ}
    (hf : f.natDegree ≤ d)
    (hg0map : g0.map (IsLocalRing.residue R) = gbar)
    (hg0nat : g0.natDegree = m)
    (hgbar_nat : gbar.natDegree = m)
    (hglead : gbar.leadingCoeff ≠ 0)
    (hh0deg : h0.natDegree ≤ d - m)
    (hfactor0 : f - g0 * h0 = Polynomial.C π * f1)
    (hbezFactor : a * g0 + b * h0 - 1 = Polynomial.C π * e)
    (hmd : m ≤ d) (n : ℕ) : R[X]

def

henselFactorization_infiniteQCorr_of_mem_span

L465 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_infiniteQCorr_of_mem_span

Documentation

the infinite q-correction sequence from the displayed-factor displayed-factor prefix construction.

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

def henselFactorization_infiniteQCorr_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 f1 e : R[X]}
    {gbar : (IsLocalRing.ResidueField R)[X]} {m d : ℕ}
    (hf : f.natDegree ≤ d)
    (hg0map : g0.map (IsLocalRing.residue R) = gbar)
    (hg0nat : g0.natDegree = m)
    (hgbar_nat : gbar.natDegree = m)
    (hglead : gbar.leadingCoeff ≠ 0)
    (hh0deg : h0.natDegree ≤ d - m)
    (hfactor0 : f - g0 * h0 = Polynomial.C π * f1)
    (hbezFactor : a * g0 + b * h0 - 1 = Polynomial.C π * e)
    (hmd : m ≤ d) (n : ℕ) : R[X]

theorem

henselFactorization_infinitePCorr_natDegree_le_of_mem_span

L489 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_infinitePCorr_natDegree_le_of_mem_span

Documentation

the displayed-factor infinite p-corrections retain the stated degree bound.

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_infinitePCorr_natDegree_le_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 f1 e : R[X]}
    {gbar : (IsLocalRing.ResidueField R)[X]} {m d : ℕ}
    (hf : f.natDegree ≤ d)
    (hg0map : g0.map (IsLocalRing.residue R) = gbar)
    (hg0nat : g0.natDegree = m)
    (hgbar_nat : gbar.natDegree = m)
    (hglead : gbar.leadingCoeff ≠ 0)
    (hh0deg : h0.natDegree ≤ d - m)
    (hfactor0 : f - g0 * h0 = Polynomial.C π * f1)
    (hbezFactor : a * g0 + b * h0 - 1 = Polynomial.C π * e)
    (hmd : m ≤ d) :
    ∀ n : ℕ,
      (henselFactorization_infinitePCorr_of_mem_span
        (π := π) hπne hπmem
        (f := f) (g0 := g0) (h0 := h0)
        (a := a) (b := b) (f1 := f1) (e := e)
        (gbar := gbar) (m := m) (d := d)
        hf hg0map hg0nat hgbar_nat hglead hh0deg
        hfactor0 hbezFactor hmd n).natDegree ≤ m

theorem

henselFactorization_infiniteQCorr_natDegree_le_of_mem_span

L524 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_infiniteQCorr_natDegree_le_of_mem_span

Documentation

the displayed-factor infinite q-corrections retain the stated degree bound.

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_infiniteQCorr_natDegree_le_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 f1 e : R[X]}
    {gbar : (IsLocalRing.ResidueField R)[X]} {m d : ℕ}
    (hf : f.natDegree ≤ d)
    (hg0map : g0.map (IsLocalRing.residue R) = gbar)
    (hg0nat : g0.natDegree = m)
    (hgbar_nat : gbar.natDegree = m)
    (hglead : gbar.leadingCoeff ≠ 0)
    (hh0deg : h0.natDegree ≤ d - m)
    (hfactor0 : f - g0 * h0 = Polynomial.C π * f1)
    (hbezFactor : a * g0 + b * h0 - 1 = Polynomial.C π * e)
    (hmd : m ≤ d) :
    ∀ n : ℕ,
      (henselFactorization_infiniteQCorr_of_mem_span
        (π := π) hπne hπmem
        (f := f) (g0 := g0) (h0 := h0)
        (a := a) (b := b) (f1 := f1) (e := e)
        (gbar := gbar) (m := m) (d := d)
        hf hg0map hg0nat hgbar_nat hglead hh0deg
        hfactor0 hbezFactor hmd n).natDegree ≤ d - m

theorem

henselFactorization_prefixStateSeq_pCorr_eq_infinite_of_le_of_mem_span

L560 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_prefixStateSeq_pCorr_eq_infinite_of_le_of_mem_span

Documentation

a displayed-factor finite prefix state's p-correction agrees with the extracted infinite p-correction at every constructed index.

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_prefixStateSeq_pCorr_eq_infinite_of_le_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 f1 e : R[X]}
    {gbar : (IsLocalRing.ResidueField R)[X]} {m d : ℕ}
    (hf : f.natDegree ≤ d)
    (hg0map : g0.map (IsLocalRing.residue R) = gbar)
    (hg0nat : g0.natDegree = m)
    (hgbar_nat : gbar.natDegree = m)
    (hglead : gbar.leadingCoeff ≠ 0)
    (hh0deg : h0.natDegree ≤ d - m)
    (hfactor0 : f - g0 * h0 = Polynomial.C π * f1)
    (hbezFactor : a * g0 + b * h0 - 1 = Polynomial.C π * e)
    (hmd : m ≤ d) :
    ∀ {r N : ℕ}, r ≤ N →
      (henselFactorization_prefixStateSeq_of_mem_span
          (π := π) (f := f) (g0 := g0) (h0 := h0)
          (a := a) (b := b) (f1 := f1) (e := e)
          (gbar := gbar) (m := m) (d := d)
          hπne hπmem hf hg0map hg0nat hgbar_nat hglead hh0deg
          hfactor0 hbezFactor hmd N).pCorr r =
        henselFactorization_infinitePCorr_of_mem_span
          (π := π) hπne hπmem
          (f := f) (g0 := g0) (h0 := h0)
          (a := a) (b := b) (f1 := f1) (e := e)
          (gbar := gbar) (m := m) (d := d)
          hf hg0map hg0nat hgbar_nat hglead hh0deg
          hfactor0 hbezFactor hmd r

theorem

henselFactorization_prefixStateSeq_qCorr_eq_infinite_of_le_of_mem_span

L601 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_prefixStateSeq_qCorr_eq_infinite_of_le_of_mem_span

Documentation

a displayed-factor finite prefix state's q-correction agrees with the extracted infinite q-correction at every constructed index.

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_prefixStateSeq_qCorr_eq_infinite_of_le_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 f1 e : R[X]}
    {gbar : (IsLocalRing.ResidueField R)[X]} {m d : ℕ}
    (hf : f.natDegree ≤ d)
    (hg0map : g0.map (IsLocalRing.residue R) = gbar)
    (hg0nat : g0.natDegree = m)
    (hgbar_nat : gbar.natDegree = m)
    (hglead : gbar.leadingCoeff ≠ 0)
    (hh0deg : h0.natDegree ≤ d - m)
    (hfactor0 : f - g0 * h0 = Polynomial.C π * f1)
    (hbezFactor : a * g0 + b * h0 - 1 = Polynomial.C π * e)
    (hmd : m ≤ d) :
    ∀ {r N : ℕ}, r ≤ N →
      (henselFactorization_prefixStateSeq_of_mem_span
          (π := π) (f := f) (g0 := g0) (h0 := h0)
          (a := a) (b := b) (f1 := f1) (e := e)
          (gbar := gbar) (m := m) (d := d)
          hπne hπmem hf hg0map hg0nat hgbar_nat hglead hh0deg
          hfactor0 hbezFactor hmd N).qCorr r =
        henselFactorization_infiniteQCorr_of_mem_span
          (π := π) hπne hπmem
          (f := f) (g0 := g0) (h0 := h0)
          (a := a) (b := b) (f1 := f1) (e := e)
          (gbar := gbar) (m := m) (d := d)
          hf hg0map hg0nat hgbar_nat hglead hh0deg
          hfactor0 hbezFactor hmd r

theorem

henselFactorization_infiniteCorr_factor_prefix_of_mem_span

L642 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_infiniteCorr_factor_prefix_of_mem_span

Documentation

every finite displayed-factor factorization invariant transfers from the coherent prefix states to the extracted infinite correction sequences.

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_infiniteCorr_factor_prefix_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 f1 e : R[X]}
    {gbar : (IsLocalRing.ResidueField R)[X]} {m d : ℕ}
    (hf : f.natDegree ≤ d)
    (hg0map : g0.map (IsLocalRing.residue R) = gbar)
    (hg0nat : g0.natDegree = m)
    (hgbar_nat : gbar.natDegree = m)
    (hglead : gbar.leadingCoeff ≠ 0)
    (hh0deg : h0.natDegree ≤ d - m)
    (hfactor0 : f - g0 * h0 = Polynomial.C π * f1)
    (hbezFactor : a * g0 + b * h0 - 1 = Polynomial.C π * e)
    (hmd : m ≤ d) :
    ∀ N : ℕ,
      ∃ fN : R[X],
        f - henselFactorization_henselIterate π g0
              (henselFactorization_infinitePCorr_of_mem_span
                (π := π) hπne hπmem
                (f := f) (g0 := g0) (h0 := h0)
                (a := a) (b := b) (f1 := f1) (e := e)
                (gbar := gbar) (m := m) (d := d)
                hf hg0map hg0nat hgbar_nat hglead hh0deg
                hfactor0 hbezFactor hmd) N *
            henselFactorization_henselIterate π h0
              (henselFactorization_infiniteQCorr_of_mem_span
                (π := π) hπne hπmem
                (f := f) (g0 := g0) (h0 := h0)
                (a := a) (b := b) (f1 := f1) (e := e)
                (gbar := gbar) (m := m) (d := d)
                hf hg0map hg0nat hgbar_nat hglead hh0deg
                hfactor0 hbezFactor hmd) N =
          Polynomial.C (π ^ (N + 1)) * fN

theorem

henselFactorization_infiniteCorr_error_coeff_mem_maximalIdeal_pow_of_mem_span

L729 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_infiniteCorr_error_coeff_mem_maximalIdeal_pow_of_mem_span

Documentation

the factorization error of the displayed-factor infinite approximants is coefficientwise in the corresponding high power of 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_infiniteCorr_error_coeff_mem_maximalIdeal_pow_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 f1 e : R[X]}
    {gbar : (IsLocalRing.ResidueField R)[X]} {m d : ℕ}
    (hf : f.natDegree ≤ d)
    (hg0map : g0.map (IsLocalRing.residue R) = gbar)
    (hg0nat : g0.natDegree = m)
    (hgbar_nat : gbar.natDegree = m)
    (hglead : gbar.leadingCoeff ≠ 0)
    (hh0deg : h0.natDegree ≤ d - m)
    (hfactor0 : f - g0 * h0 = Polynomial.C π * f1)
    (hbezFactor : a * g0 + b * h0 - 1 = Polynomial.C π * e)
    (hmd : m ≤ d) :
    ∀ N i : ℕ,
      (f - henselFactorization_henselIterate π g0
            (henselFactorization_infinitePCorr_of_mem_span
              (π := π) hπne hπmem
              (f := f) (g0 := g0) (h0 := h0)
              (a := a) (b := b) (f1 := f1) (e := e)
              (gbar := gbar) (m := m) (d := d)
              hf hg0map hg0nat hgbar_nat hglead hh0deg
              hfactor0 hbezFactor hmd) N *
          henselFactorization_henselIterate π h0
            (henselFactorization_infiniteQCorr_of_mem_span
              (π := π) hπne hπmem
              (f := f) (g0 := g0) (h0 := h0)
              (a := a) (b := b) (f1 := f1) (e := e)
              (gbar := gbar) (m := m) (d := d)
              hf hg0map hg0nat hgbar_nat hglead hh0deg
              hfactor0 hbezFactor hmd) N).coeff i ∈
        IsLocalRing.maximalIdeal R ^ (N + 1)

theorem

henselFactorization_infiniteGIter_natDegree_le_of_mem_span

L776 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_infiniteGIter_natDegree_le_of_mem_span

Documentation

the displayed-factor g-approximants keep the construction degree bound.

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_infiniteGIter_natDegree_le_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 f1 e : R[X]}
    {gbar : (IsLocalRing.ResidueField R)[X]} {m d : ℕ}
    (hf : f.natDegree ≤ d)
    (hg0map : g0.map (IsLocalRing.residue R) = gbar)
    (hg0nat : g0.natDegree = m)
    (hgbar_nat : gbar.natDegree = m)
    (hglead : gbar.leadingCoeff ≠ 0)
    (hh0deg : h0.natDegree ≤ d - m)
    (hfactor0 : f - g0 * h0 = Polynomial.C π * f1)
    (hbezFactor : a * g0 + b * h0 - 1 = Polynomial.C π * e)
    (hmd : m ≤ d) :
    ∀ N : ℕ,
      (henselFactorization_henselIterate π g0
        (henselFactorization_infinitePCorr_of_mem_span
          (π := π) hπne hπmem
          (f := f) (g0 := g0) (h0 := h0)
          (a := a) (b := b) (f1 := f1) (e := e)
          (gbar := gbar) (m := m) (d := d)
          hf hg0map hg0nat hgbar_nat hglead hh0deg
          hfactor0 hbezFactor hmd)
        N).natDegree ≤ m

theorem

henselFactorization_infiniteHIter_natDegree_le_of_mem_span

L822 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_infiniteHIter_natDegree_le_of_mem_span

Documentation

the displayed-factor h-approximants keep the construction degree bound.

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_infiniteHIter_natDegree_le_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 f1 e : R[X]}
    {gbar : (IsLocalRing.ResidueField R)[X]} {m d : ℕ}
    (hf : f.natDegree ≤ d)
    (hg0map : g0.map (IsLocalRing.residue R) = gbar)
    (hg0nat : g0.natDegree = m)
    (hgbar_nat : gbar.natDegree = m)
    (hglead : gbar.leadingCoeff ≠ 0)
    (hh0deg : h0.natDegree ≤ d - m)
    (hfactor0 : f - g0 * h0 = Polynomial.C π * f1)
    (hbezFactor : a * g0 + b * h0 - 1 = Polynomial.C π * e)
    (hmd : m ≤ d) :
    ∀ N : ℕ,
      (henselFactorization_henselIterate π h0
        (henselFactorization_infiniteQCorr_of_mem_span
          (π := π) hπne hπmem
          (f := f) (g0 := g0) (h0 := h0)
          (a := a) (b := b) (f1 := f1) (e := e)
          (gbar := gbar) (m := m) (d := d)
          hf hg0map hg0nat hgbar_nat hglead hh0deg
          hfactor0 hbezFactor hmd)
        N).natDegree ≤ d - m

theorem

henselFactorization_infiniteGIter_reduction_of_mem_span

L868 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_infiniteGIter_reduction_of_mem_span

Documentation

the displayed-factor infinite g-approximants keep the original residual class of g0.

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_infiniteGIter_reduction_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 f1 e : R[X]}
    {gbar : (IsLocalRing.ResidueField R)[X]} {m d : ℕ}
    (hf : f.natDegree ≤ d)
    (hg0map : g0.map (IsLocalRing.residue R) = gbar)
    (hg0nat : g0.natDegree = m)
    (hgbar_nat : gbar.natDegree = m)
    (hglead : gbar.leadingCoeff ≠ 0)
    (hh0deg : h0.natDegree ≤ d - m)
    (hfactor0 : f - g0 * h0 = Polynomial.C π * f1)
    (hbezFactor : a * g0 + b * h0 - 1 = Polynomial.C π * e)
    (hmd : m ≤ d) :
    ∀ N i : ℕ,
      (henselFactorization_henselIterate π g0
        (henselFactorization_infinitePCorr_of_mem_span
          (π := π) hπne hπmem
          (f := f) (g0 := g0) (h0 := h0)
          (a := a) (b := b) (f1 := f1) (e := e)
          (gbar := gbar) (m := m) (d := d)
          hf hg0map hg0nat hgbar_nat hglead hh0deg
          hfactor0 hbezFactor hmd)
        N - g0).coeff i ∈
        IsLocalRing.maximalIdeal R

theorem

henselFactorization_infiniteHIter_reduction_of_mem_span

L906 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_infiniteHIter_reduction_of_mem_span

Documentation

the displayed-factor infinite h-approximants keep the original residual class of h0.

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_infiniteHIter_reduction_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 f1 e : R[X]}
    {gbar : (IsLocalRing.ResidueField R)[X]} {m d : ℕ}
    (hf : f.natDegree ≤ d)
    (hg0map : g0.map (IsLocalRing.residue R) = gbar)
    (hg0nat : g0.natDegree = m)
    (hgbar_nat : gbar.natDegree = m)
    (hglead : gbar.leadingCoeff ≠ 0)
    (hh0deg : h0.natDegree ≤ d - m)
    (hfactor0 : f - g0 * h0 = Polynomial.C π * f1)
    (hbezFactor : a * g0 + b * h0 - 1 = Polynomial.C π * e)
    (hmd : m ≤ d) :
    ∀ N i : ℕ,
      (henselFactorization_henselIterate π h0
        (henselFactorization_infiniteQCorr_of_mem_span
          (π := π) hπne hπmem
          (f := f) (g0 := g0) (h0 := h0)
          (a := a) (b := b) (f1 := f1) (e := e)
          (gbar := gbar) (m := m) (d := d)
          hf hg0map hg0nat hgbar_nat hglead hh0deg
          hfactor0 hbezFactor hmd)
        N - h0).coeff i ∈
        IsLocalRing.maximalIdeal R

theorem

henselFactorization_infiniteGIter_sub_coeff_mem_maximalIdeal_pow_of_le_of_mem_span

L944 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_infiniteGIter_sub_coeff_mem_maximalIdeal_pow_of_le_of_mem_span

Documentation

coefficientwise Cauchy estimate for the displayed-factor infinite g-approximants.

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_infiniteGIter_sub_coeff_mem_maximalIdeal_pow_of_le_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 f1 e : R[X]}
    {gbar : (IsLocalRing.ResidueField R)[X]} {m d : ℕ}
    (hf : f.natDegree ≤ d)
    (hg0map : g0.map (IsLocalRing.residue R) = gbar)
    (hg0nat : g0.natDegree = m)
    (hgbar_nat : gbar.natDegree = m)
    (hglead : gbar.leadingCoeff ≠ 0)
    (hh0deg : h0.natDegree ≤ d - m)
    (hfactor0 : f - g0 * h0 = Polynomial.C π * f1)
    (hbezFactor : a * g0 + b * h0 - 1 = Polynomial.C π * e)
    (hmd : m ≤ d) :
    ∀ {M N : ℕ}, M ≤ N → ∀ i : ℕ,
      (henselFactorization_henselIterate π g0
          (henselFactorization_infinitePCorr_of_mem_span
            (π := π) hπne hπmem
            (f := f) (g0 := g0) (h0 := h0)
            (a := a) (b := b) (f1 := f1) (e := e)
            (gbar := gbar) (m := m) (d := d)
            hf hg0map hg0nat hgbar_nat hglead hh0deg
            hfactor0 hbezFactor hmd)
          N -
        henselFactorization_henselIterate π g0
          (henselFactorization_infinitePCorr_of_mem_span
            (π := π) hπne hπmem
            (f := f) (g0 := g0) (h0 := h0)
            (a := a) (b := b) (f1 := f1) (e := e)
            (gbar := gbar) (m := m) (d := d)
            hf hg0map hg0nat hgbar_nat hglead hh0deg
            hfactor0 hbezFactor hmd)
          M).coeff i ∈
        IsLocalRing.maximalIdeal R ^ (M + 1)

theorem

henselFactorization_infiniteHIter_sub_coeff_mem_maximalIdeal_pow_of_le_of_mem_span

L991 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_infiniteHIter_sub_coeff_mem_maximalIdeal_pow_of_le_of_mem_span

Documentation

coefficientwise Cauchy estimate for the displayed-factor infinite h-approximants.

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_infiniteHIter_sub_coeff_mem_maximalIdeal_pow_of_le_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 f1 e : R[X]}
    {gbar : (IsLocalRing.ResidueField R)[X]} {m d : ℕ}
    (hf : f.natDegree ≤ d)
    (hg0map : g0.map (IsLocalRing.residue R) = gbar)
    (hg0nat : g0.natDegree = m)
    (hgbar_nat : gbar.natDegree = m)
    (hglead : gbar.leadingCoeff ≠ 0)
    (hh0deg : h0.natDegree ≤ d - m)
    (hfactor0 : f - g0 * h0 = Polynomial.C π * f1)
    (hbezFactor : a * g0 + b * h0 - 1 = Polynomial.C π * e)
    (hmd : m ≤ d) :
    ∀ {M N : ℕ}, M ≤ N → ∀ i : ℕ,
      (henselFactorization_henselIterate π h0
          (henselFactorization_infiniteQCorr_of_mem_span
            (π := π) hπne hπmem
            (f := f) (g0 := g0) (h0 := h0)
            (a := a) (b := b) (f1 := f1) (e := e)
            (gbar := gbar) (m := m) (d := d)
            hf hg0map hg0nat hgbar_nat hglead hh0deg
            hfactor0 hbezFactor hmd)
          N -
        henselFactorization_henselIterate π h0
          (henselFactorization_infiniteQCorr_of_mem_span
            (π := π) hπne hπmem
            (f := f) (g0 := g0) (h0 := h0)
            (a := a) (b := b) (f1 := f1) (e := e)
            (gbar := gbar) (m := m) (d := d)
            hf hg0map hg0nat hgbar_nat hglead hh0deg
            hfactor0 hbezFactor hmd)
          M).coeff i ∈
        IsLocalRing.maximalIdeal R ^ (M + 1)

Module documentation

compatible Hensel prefixes

Declarations