NYLL
Module

DegreeBounds.lean

Nyll.ValuedFieldTheory.Valuation.Henselian.Factorization.DegreeBounds
7 declarations indexed from sourceView source ↗

Module documentation

degree bounds for the error factors

This file supplies the degree estimates for the polynomials f_n appearing in the coefficientwise Hensel iteration.

Imports1
Imported by10

Declarations

theorem

henselFactorization_map_natDegree_le_of_natDegree_le

L25 ↗
AlgebraicNumberTheory.Valuations.henselFactorization_map_natDegree_le_of_natDegree_le
Documentation

a natural-degree bound survives reduction of coefficients.

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_map_natDegree_le_of_natDegree_le
    {R k : Type*} [CommRing R] [CommRing k] (φ : R →+* k)
    {P : R[X]} {d : ℕ} (hP : P.natDegree ≤ d) :
    (P.map φ).natDegree ≤ d
theorem

henselFactorization_natDegree_eq_of_residue_eq_of_le

L33 ↗
AlgebraicNumberTheory.Valuations.henselFactorization_natDegree_eq_of_residue_eq_of_le
Documentation

exact degree is recovered from a bounded lift whose reduction has nonzero leading coefficient in the prescribed degree.

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_natDegree_eq_of_residue_eq_of_le
    {R : Type*} [CommRing R] [IsLocalRing R]
    {P : R[X]} {gbar : (IsLocalRing.ResidueField R)[X]} {m : ℕ}
    (hP : P.natDegree ≤ m)
    (hmap : P.map (IsLocalRing.residue R) = gbar)
    (hgbar_nat : gbar.natDegree = m)
    (hglead : gbar.leadingCoeff ≠ 0) :
    P.natDegree = m
theorem

henselFactorization_residual_right_natDegree_le

L58 ↗
AlgebraicNumberTheory.Valuations.henselFactorization_residual_right_natDegree_le
Documentation

the stated degree bound for the second residual factor: if fbar = gbar*hbar, deg fbar≤d, and deg gbar=m with gbar≠0, then deg hbar≤d-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_residual_right_natDegree_le
    {k : Type*} [Field k] {fbar gbar hbar : k[X]} {m d : ℕ}
    (hfbar : fbar = gbar * hbar)
    (hf : fbar.natDegree ≤ d)
    (hgbar_nat : gbar.natDegree = m)
    (hglead : gbar.leadingCoeff ≠ 0) :
    hbar.natDegree ≤ d - m
theorem

henselFactorization_error_natDegree_le

L76 ↗
AlgebraicNumberTheory.Valuations.henselFactorization_error_natDegree_le
Documentation

if deg f ≤ d, deg g ≤ m, and deg h ≤ d-m, then deg(f-gh)≤d.

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_error_natDegree_le
    {R : Type*} [CommRing R] {f g h : R[X]} {d m : ℕ}
    (hf : f.natDegree ≤ d) (hg : g.natDegree ≤ m)
    (hh : h.natDegree ≤ d - m) (hmd : m ≤ d) :
    (f - g * h).natDegree ≤ d
theorem

henselFactorization_factor_natDegree_le_of_constant_mul_eq

L92 ↗
AlgebraicNumberTheory.Valuations.henselFactorization_factor_natDegree_le_of_constant_mul_eq
Documentation

if P=C(a)Q with a≠0, then a degree bound on P is a degree bound on Q.

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_factor_natDegree_le_of_constant_mul_eq
    {R : Type*} [CommRing R] [NoZeroDivisors R] {a : R} (ha : a ≠ 0)
    {P Q : R[X]} {d : ℕ}
    (hP : P.natDegree ≤ d) (hfactor : P = Polynomial.C a * Q) :
    Q.natDegree ≤ d
theorem

henselFactorization_error_factor_natDegree_le

L103 ↗
AlgebraicNumberTheory.Valuations.henselFactorization_error_factor_natDegree_le
Documentation

degree bound for the next error factor f_n from the current factorization 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
theorem henselFactorization_error_factor_natDegree_le
    {R : Type*} [CommRing R] [NoZeroDivisors R] {π : R} {n : ℕ}
    (hπn : π ^ n ≠ 0)
    {f g h fn : R[X]} {d m : ℕ}
    (hf : f.natDegree ≤ d) (hg : g.natDegree ≤ m)
    (hh : h.natDegree ≤ d - m) (hmd : m ≤ d)
    (hfactor : f - g * h = Polynomial.C (π ^ n) * fn) :
    fn.natDegree ≤ d
theorem

henselFactorization_error_factor_residue_natDegree_le

L118 ↗
AlgebraicNumberTheory.Valuations.henselFactorization_error_factor_residue_natDegree_le
Documentation

residue-degree bound for the next error factor f_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_error_factor_residue_natDegree_le
    {R : Type*} [CommRing R] [IsLocalRing R] [NoZeroDivisors R]
    {π : R} {n : ℕ} (hπn : π ^ n ≠ 0)
    {f g h fn : R[X]} {d m : ℕ}
    (hf : f.natDegree ≤ d) (hg : g.natDegree ≤ m)
    (hh : h.natDegree ≤ d - m) (hmd : m ≤ d)
    (hfactor : f - g * h = Polynomial.C (π ^ n) * fn) :
    (fn.map (IsLocalRing.residue R)).natDegree ≤ d

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