Module

IrreduciblePolynomialBounds.lean

Nyll.ValuedFieldTheory.Valuation.Henselian.IrreduciblePolynomialBounds

28 declarations indexed from sourceView source ↗

Module documentation

reduction input for the coefficient estimate

This file isolates the residue-polynomial input used in the irreducible-polynomial coefficient estimate. For the closed-unit-ball valuation ring attached to a nonarchimedean absolute value, coefficients of value < 1 reduce to zero and coefficients of value 1 reduce to nonzero elements. Hence the first coefficient of value 1 gives the exact initial X-power dividing the reduced polynomial.

Imports2

Nyll.ValuedFieldTheory.Valuation.AbsoluteValue.ValuationSubring
Mathlib.Algebra.Polynomial.Div

Imported by10

def

polynomialCoeffAbsMax

L30 ↗

AlgebraicNumberTheory.Valuations.polynomialCoeffAbsMax

Documentation

The coefficient norm |f| used in irreducible-polynomial lifting: the maximum absolute value of the coefficients of f.

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 polynomialCoeffAbsMax
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ) (f : K[X]) : ℝ

theorem

irreduciblePolynomial_reduction_coeff_eq_zero_of_abs_lt_one

L40 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_reduction_coeff_eq_zero_of_abs_lt_one

Documentation

reduction input: a coefficient of absolute value < 1 reduces to the zero coefficient of the residue polynomial.

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 irreduciblePolynomial_reduction_coeff_eq_zero_of_abs_lt_one
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (F : (absoluteValueValuationSubring v hnonarch)[X])
    {i : ℕ} (hi : v (F.coeff i : K) < 1) :
    (F.map (IsLocalRing.residue
        (absoluteValueValuationSubring v hnonarch))).coeff i =
      0

theorem

irreduciblePolynomial_reduction_coeff_ne_zero_of_abs_eq_one

L55 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_reduction_coeff_ne_zero_of_abs_eq_one

Documentation

reduction input: a coefficient of absolute value 1 reduces to a nonzero coefficient of the residue polynomial.

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 irreduciblePolynomial_reduction_coeff_ne_zero_of_abs_eq_one
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (F : (absoluteValueValuationSubring v hnonarch)[X])
    {i : ℕ} (hi : v (F.coeff i : K) = 1) :
    (F.map (IsLocalRing.residue
        (absoluteValueValuationSubring v hnonarch))).coeff i ≠
      0

theorem

irreduciblePolynomial_reduction_X_pow_dvd_of_initial_abs_lt_one

L70 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_reduction_X_pow_dvd_of_initial_abs_lt_one

Documentation

reduction input: if all coefficients below r have absolute value < 1, then X^r divides the reduced polynomial.

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 irreduciblePolynomial_reduction_X_pow_dvd_of_initial_abs_lt_one
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (F : (absoluteValueValuationSubring v hnonarch)[X])
    {r : ℕ} (hinit : ∀ i : ℕ, i < r → v (F.coeff i : K) < 1) :
    Polynomial.X ^ r ∣
      F.map (IsLocalRing.residue
        (absoluteValueValuationSubring v hnonarch))

theorem

irreduciblePolynomial_reduction_exact_X_pow_of_first_abs_eq_one

L86 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_reduction_exact_X_pow_of_first_abs_eq_one

Documentation

reduction input: if r is the first coefficient with absolute value 1, then the reduced polynomial is divisible by exactly X^r at the origin.

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 irreduciblePolynomial_reduction_exact_X_pow_of_first_abs_eq_one
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (F : (absoluteValueValuationSubring v hnonarch)[X])
    {r : ℕ} (hinit : ∀ i : ℕ, i < r → v (F.coeff i : K) < 1)
    (hr : v (F.coeff r : K) = 1) :
    Polynomial.X ^ r ∣
        F.map (IsLocalRing.residue
          (absoluteValueValuationSubring v hnonarch)) ∧
      ¬ Polynomial.X ^ (r + 1) ∣
        F.map (IsLocalRing.residue
          (absoluteValueValuationSubring v hnonarch))

theorem

irreduciblePolynomial_exists_first_abs_eq_one_coeff

L114 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_exists_first_abs_eq_one_coeff

Documentation

reduction input: from any coefficient of value 1, choose the first such coefficient. Every earlier coefficient then has value < 1 because all coefficients already lie in the closed unit ball.

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 irreduciblePolynomial_exists_first_abs_eq_one_coeff
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (F : (absoluteValueValuationSubring v hnonarch)[X])
    {n : ℕ} (hn : v (F.coeff n : K) = 1) :
    ∃ r : ℕ,
      v (F.coeff r : K) = 1 ∧
        ∀ i : ℕ, i < r → v (F.coeff i : K) < 1

theorem

irreduciblePolynomial_exists_exact_X_pow_reduction_of_abs_eq_one_coeff

L137 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_exists_exact_X_pow_reduction_of_abs_eq_one_coeff

Documentation

reduction input: if some coefficient has value 1, then the reduced polynomial has an exact initial X^r divisor for the first such coefficient r.

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 irreduciblePolynomial_exists_exact_X_pow_reduction_of_abs_eq_one_coeff
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (F : (absoluteValueValuationSubring v hnonarch)[X])
    {n : ℕ} (hn : v (F.coeff n : K) = 1) :
    ∃ r : ℕ,
      v (F.coeff r : K) = 1 ∧
        Polynomial.X ^ r ∣
            F.map (IsLocalRing.residue
              (absoluteValueValuationSubring v hnonarch)) ∧
          ¬ Polynomial.X ^ (r + 1) ∣
            F.map (IsLocalRing.residue
              (absoluteValueValuationSubring v hnonarch))

theorem

irreduciblePolynomial_first_abs_eq_one_index_pos_of_const_abs_lt_one

L158 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_first_abs_eq_one_index_pos_of_const_abs_lt_one

Documentation

reduction input: if the degree-zero coefficient has absolute value < 1, then the first coefficient of value 1 has positive 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 irreduciblePolynomial_first_abs_eq_one_index_pos_of_const_abs_lt_one
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (F : (absoluteValueValuationSubring v hnonarch)[X])
    {r : ℕ} (hconst : v (F.coeff 0 : K) < 1)
    (hr : v (F.coeff r : K) = 1) :
    0 < r

theorem

irreduciblePolynomial_coeff_ne_zero_of_abs_eq_one

L176 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_coeff_ne_zero_of_abs_eq_one

Documentation

A coefficient whose absolute value is 1 is nonzero. This small field-level fact is used repeatedly when passing from coefficient estimates to degree bounds.

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 irreduciblePolynomial_coeff_ne_zero_of_abs_eq_one
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (F : (absoluteValueValuationSubring v hnonarch)[X])
    {i : ℕ} (hi : v (F.coeff i : K) = 1) :
    F.coeff i ≠ 0

theorem

irreduciblePolynomial_abs_eq_one_index_lt_natDegree_of_leading_abs_lt_one

L188 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_abs_eq_one_index_lt_natDegree_of_leading_abs_lt_one

Documentation

reduction input: if the leading coefficient has absolute value < 1, then a coefficient of value 1 occurs strictly before the natural 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 irreduciblePolynomial_abs_eq_one_index_lt_natDegree_of_leading_abs_lt_one
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (F : (absoluteValueValuationSubring v hnonarch)[X])
    {r : ℕ} (hlead : v (F.leadingCoeff : K) < 1)
    (hr : v (F.coeff r : K) = 1) :
    r < F.natDegree

theorem

irreduciblePolynomial_abs_eq_one_index_le_natDegree

L209 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_abs_eq_one_index_le_natDegree

Documentation

finite support input: a coefficient of absolute value 1 can only occur at an index bounded by the natural 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 irreduciblePolynomial_abs_eq_one_index_le_natDegree
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (F : (absoluteValueValuationSubring v hnonarch)[X])
    {i : ℕ} (hi : v (F.coeff i : K) = 1) :
    i ≤ F.natDegree

theorem

irreduciblePolynomial_exists_last_abs_eq_one_coeff

L220 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_exists_last_abs_eq_one_coeff

Documentation

reduction input: from any coefficient of value 1, choose the last such coefficient.

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 irreduciblePolynomial_exists_last_abs_eq_one_coeff
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (F : (absoluteValueValuationSubring v hnonarch)[X])
    {n : ℕ} (hn : v (F.coeff n : K) = 1) :
    ∃ s : ℕ,
      v (F.coeff s : K) = 1 ∧
        ∀ i : ℕ, v (F.coeff i : K) = 1 → i ≤ s

theorem

irreduciblePolynomial_last_abs_eq_one_index_lt_natDegree_of_leading_abs_lt_one

L254 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_last_abs_eq_one_index_lt_natDegree_of_leading_abs_lt_one

Documentation

reduction input: if the leading coefficient has absolute value < 1, then the last coefficient of value 1 occurs strictly before the natural 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 irreduciblePolynomial_last_abs_eq_one_index_lt_natDegree_of_leading_abs_lt_one
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (F : (absoluteValueValuationSubring v hnonarch)[X])
    {s : ℕ} (hlead : v (F.leadingCoeff : K) < 1)
    (hs : v (F.coeff s : K) = 1) :
    s < F.natDegree

theorem

irreduciblePolynomial_reduction_natDegree_eq_last_abs_eq_one

L266 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_reduction_natDegree_eq_last_abs_eq_one

Documentation

reduction input: the last coefficient of value 1 is the natural degree of the reduced polynomial.

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 irreduciblePolynomial_reduction_natDegree_eq_last_abs_eq_one
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (F : (absoluteValueValuationSubring v hnonarch)[X])
    {s : ℕ} (hs : v (F.coeff s : K) = 1)
    (hlast : ∀ i : ℕ, v (F.coeff i : K) = 1 → i ≤ s) :
    (F.map (IsLocalRing.residue
      (absoluteValueValuationSubring v hnonarch))).natDegree =
      s

theorem

irreduciblePolynomial_reduction_eq_X_pow_mul_divByMonic_of_X_pow_dvd

L291 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_reduction_eq_X_pow_mul_divByMonic_of_X_pow_dvd

Documentation

reduction input: exact X^r divisibility rewrites the reduced polynomial as X^r times its monic quotient.

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 irreduciblePolynomial_reduction_eq_X_pow_mul_divByMonic_of_X_pow_dvd
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (F : (absoluteValueValuationSubring v hnonarch)[X])
    {r : ℕ}
    (hdiv : Polynomial.X ^ r ∣
      F.map (IsLocalRing.residue
        (absoluteValueValuationSubring v hnonarch))) :
    F.map (IsLocalRing.residue
        (absoluteValueValuationSubring v hnonarch)) =
      Polynomial.X ^ r *
        (F.map (IsLocalRing.residue
          (absoluteValueValuationSubring v hnonarch)) /ₘ
            Polynomial.X ^ r)

theorem

irreduciblePolynomial_reduction_divByMonic_X_pow_coeff_zero_ne_zero

L320 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_reduction_divByMonic_X_pow_coeff_zero_ne_zero

Documentation

reduction input: exact nondivisibility by X^(r+1) says that the monic quotient by X^r has nonzero degree-zero coefficient.

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 irreduciblePolynomial_reduction_divByMonic_X_pow_coeff_zero_ne_zero
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (F : (absoluteValueValuationSubring v hnonarch)[X])
    {r : ℕ}
    (hdiv : Polynomial.X ^ r ∣
      F.map (IsLocalRing.residue
        (absoluteValueValuationSubring v hnonarch)))
    (hnotdiv : ¬ Polynomial.X ^ (r + 1) ∣
      F.map (IsLocalRing.residue
        (absoluteValueValuationSubring v hnonarch))) :
    ((F.map (IsLocalRing.residue
        (absoluteValueValuationSubring v hnonarch)) /ₘ
          Polynomial.X ^ r).coeff 0) ≠ 0

theorem

irreduciblePolynomial_reduction_X_pow_isCoprime_divByMonic_of_coeff_zero_ne_zero

L358 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_reduction_X_pow_isCoprime_divByMonic_of_coeff_zero_ne_zero

Documentation

Hensel input: if the quotient after removing the exact initial X^r factor has nonzero degree-zero coefficient, then it is coprime to X^r.

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 irreduciblePolynomial_reduction_X_pow_isCoprime_divByMonic_of_coeff_zero_ne_zero
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (F : (absoluteValueValuationSubring v hnonarch)[X])
    {r : ℕ}
    (hQ0 :
      ((F.map (IsLocalRing.residue
        (absoluteValueValuationSubring v hnonarch)) /ₘ
          Polynomial.X ^ r).coeff 0) ≠ 0) :
    IsCoprime (Polynomial.X ^ r)
      (F.map (IsLocalRing.residue
        (absoluteValueValuationSubring v hnonarch)) /ₘ
          Polynomial.X ^ r)

theorem

irreduciblePolynomial_reduction_X_pow_isCoprime_divByMonic_of_exact

L398 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_reduction_X_pow_isCoprime_divByMonic_of_exact

Documentation

Hensel input: exact X^r divisibility of the reduction supplies the coprime factor pair X^r and the remaining quotient.

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 irreduciblePolynomial_reduction_X_pow_isCoprime_divByMonic_of_exact
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (F : (absoluteValueValuationSubring v hnonarch)[X])
    {r : ℕ}
    (hdiv : Polynomial.X ^ r ∣
      F.map (IsLocalRing.residue
        (absoluteValueValuationSubring v hnonarch)))
    (hnotdiv : ¬ Polynomial.X ^ (r + 1) ∣
      F.map (IsLocalRing.residue
        (absoluteValueValuationSubring v hnonarch))) :
    IsCoprime (Polynomial.X ^ r)
      (F.map (IsLocalRing.residue
        (absoluteValueValuationSubring v hnonarch)) /ₘ
          Polynomial.X ^ r)

theorem

irreduciblePolynomial_reduction_divByMonic_X_pow_natDegree

L421 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_reduction_divByMonic_X_pow_natDegree

Documentation

reduction input: after dividing the reduced polynomial by X^r, the monic quotient has natural degree s - r.

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 irreduciblePolynomial_reduction_divByMonic_X_pow_natDegree
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (F : (absoluteValueValuationSubring v hnonarch)[X])
    {r s : ℕ}
    (hnatDegree :
      (F.map (IsLocalRing.residue
        (absoluteValueValuationSubring v hnonarch))).natDegree =
        s) :
    (F.map (IsLocalRing.residue
        (absoluteValueValuationSubring v hnonarch)) /ₘ
          Polynomial.X ^ r).natDegree =
      s - r

theorem

irreduciblePolynomial_exists_nontrivial_exact_X_pow_reduction

L442 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_exists_nontrivial_exact_X_pow_reduction

Documentation

reduction input: under the endpoint inequalities used in the proof, the first coefficient of value 1 gives a nontrivial exact initial X^r divisor with 0 < r < natDegree.

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 irreduciblePolynomial_exists_nontrivial_exact_X_pow_reduction
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (F : (absoluteValueValuationSubring v hnonarch)[X])
    (hconst : v (F.coeff 0 : K) < 1)
    (hlead : v (F.leadingCoeff : K) < 1)
    {n : ℕ} (hn : v (F.coeff n : K) = 1) :
    ∃ r : ℕ,
      0 < r ∧ r < F.natDegree ∧
        v (F.coeff r : K) = 1 ∧
          Polynomial.X ^ r ∣
              F.map (IsLocalRing.residue
                (absoluteValueValuationSubring v hnonarch)) ∧
            ¬ Polynomial.X ^ (r + 1) ∣
              F.map (IsLocalRing.residue
                (absoluteValueValuationSubring v hnonarch))

theorem

irreduciblePolynomial_exists_hensel_reduction_factor_input

L471 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_exists_hensel_reduction_factor_input

Documentation

Hensel input: under the endpoint inequalities used in the proof, the reduction has a nontrivial monic factor X^r, the remaining quotient, and these two factors are coprime.

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 irreduciblePolynomial_exists_hensel_reduction_factor_input
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (F : (absoluteValueValuationSubring v hnonarch)[X])
    (hconst : v (F.coeff 0 : K) < 1)
    (hlead : v (F.leadingCoeff : K) < 1)
    {n : ℕ} (hn : v (F.coeff n : K) = 1) :
    ∃ r : ℕ,
      0 < r ∧ r < F.natDegree ∧
        F.map (IsLocalRing.residue
            (absoluteValueValuationSubring v hnonarch)) =
          Polynomial.X ^ r *
            (F.map (IsLocalRing.residue
              (absoluteValueValuationSubring v hnonarch)) /ₘ
                Polynomial.X ^ r) ∧
          (Polynomial.X ^ r :
            (IsLocalRing.ResidueField
              (absoluteValueValuationSubring v hnonarch))[X]).natDegree =
            r ∧
            IsCoprime (Polynomial.X ^ r)
              (F.map (IsLocalRing.residue
                (absoluteValueValuationSubring v hnonarch)) /ₘ
                  Polynomial.X ^ r) ∧
              ((F.map (IsLocalRing.residue
                (absoluteValueValuationSubring v hnonarch)) /ₘ
                  Polynomial.X ^ r).coeff 0) ≠ 0

theorem

irreduciblePolynomial_exists_hensel_reduction_factor_input_of_field_coeffs

L513 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_exists_hensel_reduction_factor_input_of_field_coeffs

Documentation

field-polynomial input: once a field polynomial has been normalized so that every coefficient lies in the closed unit ball and one coefficient has value 1, the endpoint inequalities produce the same Hensel reduction factor data after choosing a degree-preserving valuation-ring lift.

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 irreduciblePolynomial_exists_hensel_reduction_factor_input_of_field_coeffs
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (f : K[X])
    (hfcoeff : ∀ i : ℕ, v (f.coeff i) ≤ 1)
    (hconst : v (f.coeff 0) < 1)
    (hlead : v f.leadingCoeff < 1)
    {n : ℕ} (hn : v (f.coeff n) = 1) :
    ∃ F : (absoluteValueValuationSubring v hnonarch)[X],
      ∃ r : ℕ,
        F.map (algebraMap
            (absoluteValueValuationSubring v hnonarch) K) =
          f ∧
        F.natDegree = f.natDegree ∧
          0 < r ∧ r < F.natDegree ∧
            F.map (IsLocalRing.residue
                (absoluteValueValuationSubring v hnonarch)) =
              Polynomial.X ^ r *
                (F.map (IsLocalRing.residue
                  (absoluteValueValuationSubring v hnonarch)) /ₘ
                    Polynomial.X ^ r) ∧
              (Polynomial.X ^ r :
                (IsLocalRing.ResidueField
                  (absoluteValueValuationSubring v hnonarch))[X]).natDegree =
                r ∧
                IsCoprime (Polynomial.X ^ r)
                  (F.map (IsLocalRing.residue
                    (absoluteValueValuationSubring v hnonarch)) /ₘ
                      Polynomial.X ^ r) ∧
                  ((F.map (IsLocalRing.residue
                    (absoluteValueValuationSubring v hnonarch)) /ₘ
                      Polynomial.X ^ r).coeff 0) ≠ 0

theorem

irreduciblePolynomial_exists_coeff_abs_max_of_ne_zero

L568 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_exists_coeff_abs_max_of_ne_zero

Documentation

normalization source: a nonzero polynomial has a positive maximum among the absolute values of its coefficients, attained within the finite coefficient range up to natDegree.

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 irreduciblePolynomial_exists_coeff_abs_max_of_ne_zero
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    {f : K[X]} (hf : f ≠ 0) :
    ∃ m : ℝ, ∃ n : ℕ,
      0 < m ∧ n ≤ f.natDegree ∧ v (f.coeff n) = m ∧
        ∀ i : ℕ, v (f.coeff i) ≤ m

theorem

irreduciblePolynomial_scale_by_max_coeff_abs_data

L618 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_scale_by_max_coeff_abs_data

Documentation

normalization source: dividing a nonzero polynomial by a coefficient whose absolute value is the positive coefficient maximum preserves degree, puts every coefficient in the closed unit ball, and makes that chosen coefficient have value 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 · full declaration

theorem irreduciblePolynomial_scale_by_max_coeff_abs_data
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    {f : K[X]} {m : ℝ} {n : ℕ}
    (hmpos : 0 < m)
    (hnmax : v (f.coeff n) = m)
    (hbound : ∀ i : ℕ, v (f.coeff i) ≤ m) :
    let g : K[X] := Polynomial.C (f.coeff n)⁻¹ * f
    g.natDegree = f.natDegree ∧
      (∀ i : ℕ, v (g.coeff i) = m⁻¹ * v (f.coeff i)) ∧
        (∀ i : ℕ, v (g.coeff i) ≤ 1) ∧
          v (g.coeff n) = 1 := by
  let g : K[X] := Polynomial.C (f.coeff n)⁻¹ * f
  have hmne : m ≠ 0 := ne_of_gt hmpos
  have hn_ne : f.coeff n ≠ 0 := by
    intro hzero
    have h0m : (0 : ℝ) = m := by
      simpa [hzero] using hnmax
    exact hmne h0m.symm
  have hdegree : g.natDegree = f.natDegree := by
    dsimp [g]
    exact Polynomial.natDegree_C_mul (p := f) (a0 := inv_ne_zero hn_ne)
  have hcoeff_abs : ∀ i : ℕ, v (g.coeff i) = m⁻¹ * v (f.coeff i) := by
    intro i
    dsimp [g]
    calc
      v ((Polynomial.C (f.coeff n)⁻¹ * f).coeff i) =
          v ((f.coeff n)⁻¹ * f.coeff i) := by
            rw [Polynomial.coeff_C_mul]
      _ = v ((f.coeff n)⁻¹) * v (f.coeff i) := by
            rw [v.map_mul]
      _ = m⁻¹ * v (f.coeff i) := by
            rw [map_inv₀, hnmax]
  have hcoeff_le : ∀ i : ℕ, v (g.coeff i) ≤ 1 := by
    intro i
    rw [hcoeff_abs i]
    calc
      m⁻¹ * v (f.coeff i) ≤ m⁻¹ * m :=
        mul_le_mul_of_nonneg_left (hbound i) (inv_nonneg.mpr hmpos.le)
      _ = 1 := inv_mul_cancel₀ hmne
  have hn_one : v (g.coeff n) = 1 := by
    rw [hcoeff_abs n, hnmax, inv_mul_cancel₀ hmne]
  exact ⟨hdegree, hcoeff_abs, hcoeff_le, hn_one⟩

theorem

irreduciblePolynomial_exists_normalized_scale_of_ne_zero

L664 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_exists_normalized_scale_of_ne_zero

Documentation

normalization source: every nonzero field polynomial has a scaled polynomial with coefficient maximum 1, obtained by dividing by a coefficient that attains the original positive maximum.

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 irreduciblePolynomial_exists_normalized_scale_of_ne_zero
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    {f : K[X]} (hf : f ≠ 0) :
    ∃ m : ℝ, ∃ n : ℕ, ∃ g : K[X],
      0 < m ∧ n ≤ f.natDegree ∧
        v (f.coeff n) = m ∧
          (∀ i : ℕ, v (f.coeff i) ≤ m) ∧
            g = Polynomial.C (f.coeff n)⁻¹ * f ∧
              g.natDegree = f.natDegree ∧
                (∀ i : ℕ, v (g.coeff i) = m⁻¹ * v (f.coeff i)) ∧
                  (∀ i : ℕ, v (g.coeff i) ≤ 1) ∧
                    v (g.coeff n) = 1

theorem

irreduciblePolynomial_normalized_scale_endpoint_abs_lt_one

L691 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_normalized_scale_endpoint_abs_lt_one

Documentation

normalization source: if the original constant and leading coefficients are strictly smaller than the coefficient maximum, then after scaling by a maximum coefficient they are strictly inside the open unit ball.

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 irreduciblePolynomial_normalized_scale_endpoint_abs_lt_one
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    {f g : K[X]} {m : ℝ}
    (hmpos : 0 < m)
    (hdegree : g.natDegree = f.natDegree)
    (hcoeff_abs : ∀ i : ℕ, v (g.coeff i) = m⁻¹ * v (f.coeff i))
    (hconst : v (f.coeff 0) < m)
    (hlead : v f.leadingCoeff < m) :
    v (g.coeff 0) < 1 ∧ v g.leadingCoeff < 1

theorem

irreduciblePolynomial_normalized_scale_hensel_reduction_factor_input

L721 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_normalized_scale_hensel_reduction_factor_input

Documentation

normalized Hensel input: after scaling by a coefficient that attains the positive coefficient maximum, strict endpoint bounds below that maximum give the exact Hensel reduction factor input for the scaled polynomial.

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 irreduciblePolynomial_normalized_scale_hensel_reduction_factor_input
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    {f : K[X]} {m : ℝ} {n : ℕ}
    (hmpos : 0 < m)
    (hnmax : v (f.coeff n) = m)
    (hbound : ∀ i : ℕ, v (f.coeff i) ≤ m)
    (hconst : v (f.coeff 0) < m)
    (hlead : v f.leadingCoeff < m) :
    let g : K[X] := Polynomial.C (f.coeff n)⁻¹ * f
    ∃ F : (absoluteValueValuationSubring v hnonarch)[X],
      ∃ r : ℕ,
        F.map (algebraMap
            (absoluteValueValuationSubring v hnonarch) K) =
          g ∧
        F.natDegree = g.natDegree ∧
          0 < r ∧ r < F.natDegree ∧
            F.map (IsLocalRing.residue
                (absoluteValueValuationSubring v hnonarch)) =
              Polynomial.X ^ r *
                (F.map (IsLocalRing.residue
                  (absoluteValueValuationSubring v hnonarch)) /ₘ
                    Polynomial.X ^ r) ∧
              (Polynomial.X ^ r :
                (IsLocalRing.ResidueField
                  (absoluteValueValuationSubring v hnonarch))[X]).natDegree =
                r ∧
                IsCoprime (Polynomial.X ^ r)
                  (F.map (IsLocalRing.residue
                    (absoluteValueValuationSubring v hnonarch)) /ₘ
                      Polynomial.X ^ r) ∧
                  ((F.map (IsLocalRing.residue
                    (absoluteValueValuationSubring v hnonarch)) /ₘ
                      Polynomial.X ^ r).coeff 0) ≠ 0 := by
  let g : K[X] := Polynomial.C (f.coeff n)⁻¹ * f
  rcases irreduciblePolynomial_scale_by_max_coeff_abs_data
      v hmpos hnmax hbound with
    ⟨hdegree, hcoeff_abs, hcoeff_le, hn_one⟩
  rcases irreduciblePolynomial_normalized_scale_endpoint_abs_lt_one
      v hmpos hdegree hcoeff_abs hconst hlead with
    ⟨hconstg, hleadg⟩
  exact
    irreduciblePolynomial_exists_hensel_reduction_factor_input_of_field_coeffs
      v hnonarch g hcoeff_le hconstg hleadg hn_one

theorem

irreduciblePolynomial_exists_first_last_abs_eq_one_coeff

L769 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_exists_first_last_abs_eq_one_coeff

Documentation

reduction input: under the endpoint inequalities, choose the first and last coefficients of value 1; the first gives the exact initial X^r divisor and the last lies before the natural 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 irreduciblePolynomial_exists_first_last_abs_eq_one_coeff
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (F : (absoluteValueValuationSubring v hnonarch)[X])
    (hconst : v (F.coeff 0 : K) < 1)
    (hlead : v (F.leadingCoeff : K) < 1)
    {n : ℕ} (hn : v (F.coeff n : K) = 1) :
    ∃ r s : ℕ,
      0 < r ∧ r ≤ s ∧ s < F.natDegree ∧
        v (F.coeff r : K) = 1 ∧
          v (F.coeff s : K) = 1 ∧
            (∀ i : ℕ, i < r → v (F.coeff i : K) < 1) ∧
              (∀ i : ℕ, v (F.coeff i : K) = 1 → i ≤ s) ∧
                Polynomial.X ^ r ∣
                    F.map (IsLocalRing.residue
                      (absoluteValueValuationSubring
                        v hnonarch)) ∧
                  ¬ Polynomial.X ^ (r + 1) ∣
                      F.map (IsLocalRing.residue
                        (absoluteValueValuationSubring
                          v hnonarch)) ∧
                    (F.map (IsLocalRing.residue
                      (absoluteValueValuationSubring
                        v hnonarch))).natDegree = s

Module documentation

reduction input for the coefficient estimate

Declarations