Module

Iteration.lean

Nyll.ValuedFieldTheory.Valuation.Henselian.Factorization.Iteration

18 declarations indexed from sourceView source ↗

Module documentation

recursive Hensel iterates

This file records the recursive polynomial iterates used in the proof of Hensel's lemma and the coefficientwise adic estimates needed for the later completion argument.

Imports1

Nyll.ValuedFieldTheory.Valuation.Henselian.Factorization.Step

Imported by10

def

henselFactorization_henselIterate

L26 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_henselIterate

Documentation

the recursive polynomial sequence F_{n+1}=F_n+π^(n+1)c_{n+1} used for either factor in Hensel's iteration.

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_henselIterate {R : Type*} [CommRing R]
    (π : R) (F0 : R[X]) (corr : ℕ → R[X]) : ℕ → R[X]
  | 0 => F0
  | n + 1 =>
      henselFactorization_henselIterate π F0 corr n +
        Polynomial.C (π ^ (n + 1)) * corr (n + 1)

theorem

henselFactorization_henselIterate_zero

L34 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_henselIterate_zero

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_henselIterate_zero
    {R : Type*} [CommRing R] (π : R) (F0 : R[X]) (corr : ℕ → R[X]) :
    henselFactorization_henselIterate π F0 corr 0 = F0

theorem

henselFactorization_henselIterate_succ

L40 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_henselIterate_succ

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_henselIterate_succ
    {R : Type*} [CommRing R] (π : R) (F0 : R[X]) (corr : ℕ → R[X])
    (n : ℕ) :
    henselFactorization_henselIterate π F0 corr (n + 1) =
      henselFactorization_henselIterate π F0 corr n +
        Polynomial.C (π ^ (n + 1)) * corr (n + 1)

theorem

henselFactorization_henselIterate_reduction_of_mem

L50 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_henselIterate_reduction_of_mem

Documentation

every recursive iterate has the same reduction as the initial lift modulo 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_henselIterate_reduction_of_mem
    {R : Type*} [CommRing R] [IsLocalRing R] {π : R}
    (hπ : π ∈ IsLocalRing.maximalIdeal R)
    (F0 : R[X]) (corr : ℕ → R[X]) :
    ∀ n i : ℕ,
      (henselFactorization_henselIterate π F0 corr n - F0).coeff i ∈
        IsLocalRing.maximalIdeal R

theorem

henselFactorization_henselIterate_span_singleton

L74 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_henselIterate_span_singleton

Documentation

every recursive iterate is congruent to its initial lift modulo (π). This is built into the update formula and does not require (π) to be 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_henselIterate_span_singleton
    {R : Type*} [CommRing R] {π : R}
    (F0 : R[X]) (corr : ℕ → R[X]) :
    ∀ n i : ℕ,
      (henselFactorization_henselIterate π F0 corr n - F0).coeff i ∈
        Ideal.span ({π} : Set R)

theorem

henselFactorization_henselIterate_natDegree_le

L97 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_henselIterate_natDegree_le

Documentation

if the initial polynomial and all correction polynomials have degree at most M, then every recursive iterate has degree at most 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_henselIterate_natDegree_le
    {R : Type*} [CommRing R] {π : R} {F0 : R[X]} {corr : ℕ → R[X]} {M : ℕ}
    (hF0 : F0.natDegree ≤ M)
    (hcorr : ∀ n : ℕ, (corr n).natDegree ≤ M) :
    ∀ n : ℕ, (henselFactorization_henselIterate π F0 corr n).natDegree ≤ M

theorem

henselFactorization_henselIterate_eq_of_corr_eq_le

L116 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_henselIterate_eq_of_corr_eq_le

Documentation

an iterate only depends on the correction coefficients up to its own 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_henselIterate_eq_of_corr_eq_le
    {R : Type*} [CommRing R] {π : R} {F0 : R[X]}
    {corr corr' : ℕ → R[X]} :
    ∀ n : ℕ,
      (∀ k : ℕ, k ≤ n → corr k = corr' k) →
        henselFactorization_henselIterate π F0 corr n =
          henselFactorization_henselIterate π F0 corr' n

theorem

henselFactorization_henselIterate_update_of_lt

L140 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_henselIterate_update_of_lt

Documentation

changing a correction coefficient at a later index does not change an earlier Hensel iterate.

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_henselIterate_update_of_lt
    {R : Type*} [CommRing R] (π : R) (F0 : R[X])
    (corr : ℕ → R[X]) {n k : ℕ} (c : R[X]) (h : n < k) :
    henselFactorization_henselIterate π F0 (Function.update corr k c) n =
      henselFactorization_henselIterate π F0 corr n

theorem

henselFactorization_henselIterate_update_next

L158 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_henselIterate_update_next

Documentation

extending the correction sequence at the next index gives the expected next Hensel iterate.

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_henselIterate_update_next
    {R : Type*} [CommRing R] (π : R) (F0 : R[X])
    (corr : ℕ → R[X]) (n : ℕ) (c : R[X]) :
    henselFactorization_henselIterate π F0
        (Function.update corr (n + 1) c) (n + 1) =
      henselFactorization_henselIterate π F0 corr n +
        Polynomial.C (π ^ (n + 1)) * c

theorem

henselFactorization_henselIterate_update_preserves_factor_of_le

L172 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_henselIterate_update_preserves_factor_of_le

Documentation

updating the correction functions at n+1 preserves all factorization invariants already established up to stage n.

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_henselIterate_update_preserves_factor_of_le
    {R : Type*} [CommRing R] {π : R}
    {f g0 h0 : R[X]} (pCorr qCorr : ℕ → R[X])
    {n r : ℕ} (hr : r ≤ n) (p q fn : R[X])
    (hfactor :
      f - henselFactorization_henselIterate π g0 pCorr r *
          henselFactorization_henselIterate π h0 qCorr r =
        Polynomial.C (π ^ (r + 1)) * fn) :
    f - henselFactorization_henselIterate π g0
          (Function.update pCorr (n + 1) p) r *
        henselFactorization_henselIterate π h0
          (Function.update qCorr (n + 1) q) r =
      Polynomial.C (π ^ (r + 1)) * fn

theorem

henselFactorization_henselIterate_update_next_factor

L194 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_henselIterate_update_next_factor

Documentation

the one-step factorization statement rewritten in terms of the updated Hensel iterates.

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_henselIterate_update_next_factor
    {R : Type*} [CommRing R] {π : R}
    {f g0 h0 : R[X]} (pCorr qCorr : ℕ → R[X])
    (n : ℕ) (p q fnNext : R[X])
    (hfactorNext :
      f - (henselFactorization_henselIterate π g0 pCorr n +
            Polynomial.C (π ^ (n + 1)) * p) *
          (henselFactorization_henselIterate π h0 qCorr n +
            Polynomial.C (π ^ (n + 1)) * q) =
        Polynomial.C (π ^ (n + 2)) * fnNext) :
    f - henselFactorization_henselIterate π g0
          (Function.update pCorr (n + 1) p) (n + 1) *
        henselFactorization_henselIterate π h0
          (Function.update qCorr (n + 1) q) (n + 1) =
      Polynomial.C (π ^ (n + 2)) * fnNext

theorem

henselFactorization_update_corr_natDegree_le

L218 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_update_corr_natDegree_le

Documentation

a global correction-degree bound is preserved when one correction coefficient is replaced by another coefficient satisfying the same 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_update_corr_natDegree_le
    {R : Type*} [CommRing R] {corr : ℕ → R[X]} {k M : ℕ} {c : R[X]}
    (hcorr : ∀ r : ℕ, (corr r).natDegree ≤ M)
    (hc : c.natDegree ≤ M) :
    ∀ r : ℕ, ((Function.update corr k c) r).natDegree ≤ M

theorem

henselFactorization_henselIterate_succ_sub_eq

L232 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_henselIterate_succ_sub_eq

Documentation

the increment from step n to step n+1 is exactly the chosen π^(n+1)-multiple.

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_henselIterate_succ_sub_eq
    {R : Type*} [CommRing R] (π : R) (F0 : R[X]) (corr : ℕ → R[X])
    (n : ℕ) :
    henselFactorization_henselIterate π F0 corr (n + 1) -
        henselFactorization_henselIterate π F0 corr n =
      Polynomial.C (π ^ (n + 1)) * corr (n + 1)

theorem

henselFactorization_henselIterate_succ_sub_coeff_mem_span_singleton_pow

L243 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_henselIterate_succ_sub_coeff_mem_span_singleton_pow

Documentation

coefficient form of the increment estimate in the principal ideal (π^(n+1)).

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_henselIterate_succ_sub_coeff_mem_span_singleton_pow
    {R : Type*} [CommRing R] {π : R} (F0 : R[X]) (corr : ℕ → R[X])
    (n i : ℕ) :
    (henselFactorization_henselIterate π F0 corr (n + 1) -
        henselFactorization_henselIterate π F0 corr n).coeff i ∈
      Ideal.span ({π ^ (n + 1)} : Set R)

theorem

henselFactorization_henselIterate_succ_sub_coeff_mem_span_pow

L255 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_henselIterate_succ_sub_coeff_mem_span_pow

Documentation

coefficient form of the increment estimate in the (n+1)-st power of the principal 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_henselIterate_succ_sub_coeff_mem_span_pow
    {R : Type*} [CommRing R] {π : R} (F0 : R[X]) (corr : ℕ → R[X])
    (n i : ℕ) :
    (henselFactorization_henselIterate π F0 corr (n + 1) -
        henselFactorization_henselIterate π F0 corr n).coeff i ∈
      Ideal.span ({π} : Set R) ^ (n + 1)

theorem

henselFactorization_henselIterate_succ_sub_coeff_mem_maximalIdeal_pow_of_mem

L267 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_henselIterate_succ_sub_coeff_mem_maximalIdeal_pow_of_mem

Documentation

coefficient form of the increment estimate in the (n+1)-st power of the maximal ideal, using only π ∈ 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_henselIterate_succ_sub_coeff_mem_maximalIdeal_pow_of_mem
    {R : Type*} [CommRing R] [IsLocalRing R] {π : R}
    (hπ : π ∈ IsLocalRing.maximalIdeal R)
    (F0 : R[X]) (corr : ℕ → R[X]) (n i : ℕ) :
    (henselFactorization_henselIterate π F0 corr (n + 1) -
        henselFactorization_henselIterate π F0 corr n).coeff i ∈
      IsLocalRing.maximalIdeal R ^ (n + 1)

theorem

henselFactorization_henselIterate_sub_coeff_mem_maximalIdeal_pow_of_le_of_mem

L281 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_henselIterate_sub_coeff_mem_maximalIdeal_pow_of_le_of_mem

Documentation

Cauchy-control estimate for two iterates: for m ≤ n, their coefficient difference lies in the (m+1)-st 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_henselIterate_sub_coeff_mem_maximalIdeal_pow_of_le_of_mem
    {R : Type*} [CommRing R] [IsLocalRing R] {π : R}
    (hπ : π ∈ IsLocalRing.maximalIdeal R)
    (F0 : R[X]) (corr : ℕ → R[X]) :
    ∀ {m n : ℕ}, m ≤ n → ∀ i : ℕ,
      (henselFactorization_henselIterate π F0 corr n -
          henselFactorization_henselIterate π F0 corr m).coeff i ∈
        IsLocalRing.maximalIdeal R ^ (m + 1)

theorem

henselFactorization_henselIterate_sub_coeff_mem_span_pow_of_le

L321 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_henselIterate_sub_coeff_mem_span_pow_of_le

Documentation

Cauchy-control estimate for two iterates in the principal-ideal 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_henselIterate_sub_coeff_mem_span_pow_of_le
    {R : Type*} [CommRing R] {π : R}
    (F0 : R[X]) (corr : ℕ → R[X]) :
    ∀ {m n : ℕ}, m ≤ n → ∀ i : ℕ,
      (henselFactorization_henselIterate π F0 corr n -
          henselFactorization_henselIterate π F0 corr m).coeff i ∈
        Ideal.span ({π} : Set R) ^ (m + 1)

Module documentation

recursive Hensel iterates

Declarations