Module

PrincipalLimits.lean

Nyll.ValuedFieldTheory.Valuation.Henselian.Factorization.PrincipalLimits

6 declarations indexed from sourceView source ↗

Module documentation

principal-ideal limit route

This file keeps the Hensel limit step in the filtration generated by the chosen chosen element π. This is the route needed for complete valued fields whose maximal ideal is not assumed principal or adically separated.

Imports2

Imported by10

theorem

henselFactorization_infiniteG_coeff_spanAdicCoeffCauchy_of_mem_span

L27 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_infiniteG_coeff_spanAdicCoeffCauchy_of_mem_span

Documentation

displayed-factor infinite g-approximants are Cauchy for the principal-ideal filtration generated by the chosen π.

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

theorem henselFactorization_infiniteG_coeff_spanAdicCoeffCauchy_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) (i : ℕ) :
    henselFactorization_adicCoeffCauchy (Ideal.span ({π} : Set R))
      (fun 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).coeff i) := by
  exact henselFactorization_coeff_adicCoeffCauchy_of_sub_coeff_mem
    (Ideal.span ({π} : Set R))
    (Pseq := fun 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)
    (by
      intro M N hMN i
      exact henselFactorization_henselIterate_sub_coeff_mem_span_pow_of_le
        (π := π) 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)
        hMN i)
    i

theorem

henselFactorization_exists_infiniteG_spanLimitPolynomial_of_mem_span

L81 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_exists_infiniteG_spanLimitPolynomial_of_mem_span

Documentation

principal-filtration polynomial limit 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_exists_infiniteG_spanLimitPolynomial_of_mem_span
    {R : Type*} [CommRing R] [IsLocalRing R] [NoZeroDivisors R]
    {π : R} [IsPrecomplete (Ideal.span ({π} : Set 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) :
    ∃ G : R[X], G.natDegree ≤ 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 - G).coeff i ∈
          Ideal.span ({π} : Set R) ^ n

theorem

henselFactorization_infiniteH_coeff_spanAdicCoeffCauchy_of_mem_span

L140 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_infiniteH_coeff_spanAdicCoeffCauchy_of_mem_span

Documentation

displayed-factor infinite h-approximants are Cauchy for the principal-ideal filtration generated by the chosen π.

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

theorem henselFactorization_infiniteH_coeff_spanAdicCoeffCauchy_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) (i : ℕ) :
    henselFactorization_adicCoeffCauchy (Ideal.span ({π} : Set R))
      (fun 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) := by
  exact henselFactorization_coeff_adicCoeffCauchy_of_sub_coeff_mem
    (Ideal.span ({π} : Set R))
    (Pseq := fun 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)
    (by
      intro M N hMN i
      exact henselFactorization_henselIterate_sub_coeff_mem_span_pow_of_le
        (π := π) 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)
        hMN i)
    i

theorem

henselFactorization_exists_infiniteH_spanLimitPolynomial_of_mem_span

L194 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_exists_infiniteH_spanLimitPolynomial_of_mem_span

Documentation

principal-filtration polynomial limit 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_exists_infiniteH_spanLimitPolynomial_of_mem_span
    {R : Type*} [CommRing R] [IsLocalRing R] [NoZeroDivisors R]
    {π : R} [IsPrecomplete (Ideal.span ({π} : Set 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) :
    ∃ H : R[X], H.natDegree ≤ d - 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 - H).coeff i ∈
          Ideal.span ({π} : Set R) ^ n

theorem

henselFactorization_infiniteCorr_error_coeff_mem_span_pow_of_mem_span

L253 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_infiniteCorr_error_coeff_mem_span_pow_of_mem_span

Documentation

displayed-factor error estimate in the principal filtration generated by π.

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_span_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 ∈
        Ideal.span ({π} : Set R) ^ (N + 1)

theorem

henselFactorization_exists_limit_factorization_of_mem_span_principal

L300 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_exists_limit_factorization_of_mem_span_principal

Documentation

complete-limit factorization from displayed initial principal-element errors, using the π-adic principal filtration.

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_limit_factorization_of_mem_span_principal
    {R : Type*} [CommRing R] [IsLocalRing R] [NoZeroDivisors R]
    {π : R} [IsPrecomplete (Ideal.span ({π} : Set R)) R]
    [IsHausdorff (Ideal.span ({π} : Set R)) R]
    (hπne : π ≠ 0)
    (hπmem : π ∈ IsLocalRing.maximalIdeal R)
    {f g0 h0 a b f1 e : R[X]}
    {gbar hbar : (IsLocalRing.ResidueField R)[X]} {m d : ℕ}
    (hf : f.natDegree ≤ d)
    (hg0map : g0.map (IsLocalRing.residue R) = gbar)
    (hh0map : h0.map (IsLocalRing.residue R) = hbar)
    (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) :
    ∃ G H : R[X],
      G.natDegree ≤ m ∧ H.natDegree ≤ d - m ∧ f = G * H ∧
        G.map (IsLocalRing.residue R) = gbar ∧
        H.map (IsLocalRing.residue R) = hbar

Module documentation

principal-ideal limit route

Declarations

henselFactorization_infiniteG_coeff_spanAdicCoeffCauchy_of_mem_span

henselFactorization_exists_infiniteG_spanLimitPolynomial_of_mem_span

henselFactorization_infiniteH_coeff_spanAdicCoeffCauchy_of_mem_span

henselFactorization_exists_infiniteH_spanLimitPolynomial_of_mem_span

henselFactorization_infiniteCorr_error_coeff_mem_span_pow_of_mem_span

henselFactorization_exists_limit_factorization_of_mem_span_principal