NYLL
Module

WeakLimits.lean

Nyll.ValuedFieldTheory.Valuation.Henselian.Factorization.WeakLimits
5 declarations indexed from sourceView source ↗

Module documentation

maximal-ideal limit from displayed factors

This file carries the displayed C π factors from the infinite Hensel prefixes through the maximal-ideal complete-limit argument.

Imports2
Imported by10

Declarations

theorem

henselFactorization_infiniteG_coeff_adicCoeffCauchy_of_mem_span

L26 ↗
AlgebraicNumberTheory.Valuations.henselFactorization_infiniteG_coeff_adicCoeffCauchy_of_mem_span
Documentation

each coefficient sequence of the displayed-factor infinite g-approximants is adic Cauchy for the maximal-ideal 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 · full declaration
theorem henselFactorization_infiniteG_coeff_adicCoeffCauchy_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 (IsLocalRing.maximalIdeal 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
    (IsLocalRing.maximalIdeal 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_infiniteGIter_sub_coeff_mem_maximalIdeal_pow_of_le_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_limitPolynomial_of_mem_span

L77 ↗
AlgebraicNumberTheory.Valuations.henselFactorization_exists_infiniteG_limitPolynomial_of_mem_span
Documentation

the displayed-factor infinite g-approximants have a bounded polynomial limit obtained from their coefficientwise adic limits.

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_limitPolynomial_of_mem_span
    {R : Type*} [CommRing R] [IsLocalRing R] [NoZeroDivisors R]
    [IsPrecomplete (IsLocalRing.maximalIdeal R) 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 ∈
          IsLocalRing.maximalIdeal R ^ n
theorem

henselFactorization_infiniteH_coeff_adicCoeffCauchy_of_mem_span

L136 ↗
AlgebraicNumberTheory.Valuations.henselFactorization_infiniteH_coeff_adicCoeffCauchy_of_mem_span
Documentation

each coefficient sequence of the displayed-factor infinite h-approximants is adic Cauchy for the maximal-ideal 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 · full declaration
theorem henselFactorization_infiniteH_coeff_adicCoeffCauchy_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 (IsLocalRing.maximalIdeal 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
    (IsLocalRing.maximalIdeal 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_infiniteHIter_sub_coeff_mem_maximalIdeal_pow_of_le_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_limitPolynomial_of_mem_span

L187 ↗
AlgebraicNumberTheory.Valuations.henselFactorization_exists_infiniteH_limitPolynomial_of_mem_span
Documentation

the displayed-factor infinite h-approximants have a bounded polynomial limit obtained from their coefficientwise adic limits.

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_limitPolynomial_of_mem_span
    {R : Type*} [CommRing R] [IsLocalRing R] [NoZeroDivisors R]
    [IsPrecomplete (IsLocalRing.maximalIdeal R) 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 ∈
          IsLocalRing.maximalIdeal R ^ n
theorem

henselFactorization_exists_limit_factorization_of_mem_span

L246 ↗
AlgebraicNumberTheory.Valuations.henselFactorization_exists_limit_factorization_of_mem_span
Documentation

complete-limit factorization from displayed initial principal-element errors, without assuming maximalIdeal ≤ (π).

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
    {R : Type*} [CommRing R] [IsLocalRing R] [NoZeroDivisors R]
    [IsPrecomplete (IsLocalRing.maximalIdeal R) R]
    [IsHausdorff (IsLocalRing.maximalIdeal R) 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

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.