Module

IrreduciblePolynomialLifting.lean

Nyll.ValuedFieldTheory.Valuation.Henselian.IrreduciblePolynomialLifting

12 declarations indexed from sourceView source ↗

Module documentation

Hensel obstruction to irreducibility

This file applies the explicit Hensel lemma from the coefficientwise Hensel construction to the normalized residue input constructed by the coefficient-bound lemmas. The result here is the core contradiction for irreducible-polynomial lifting: a nontrivial factorization of the reduction gives a nontrivial factorization over the complete valuation ring, hence the mapped field polynomial is not irreducible.

Imports2

Imported by10

theorem

irreduciblePolynomial_not_irreducible_of_field_factor_natDegree_lt

L29 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_not_irreducible_of_field_factor_natDegree_lt

Documentation

algebraic obstruction: a field polynomial with a factor of positive degree strictly smaller than its own degree is not irreducible.

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_not_irreducible_of_field_factor_natDegree_lt
    {K : Type*} [Field K] {f g h : K[X]}
    (hfactor : f = g * h)
    (hgpos : 0 < g.natDegree)
    (hglt : g.natDegree < f.natDegree) :
    ¬ Irreducible f

theorem

irreduciblePolynomial_not_irreducible_of_valuation_factorization

L52 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_not_irreducible_of_valuation_factorization

Documentation

transport obstruction: a nontrivial factorization over the closed-unit-ball valuation ring maps to a nontrivial field factorization.

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_not_irreducible_of_valuation_factorization
    {K : Type*} [Field K]
    (v : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    {F G H : (absoluteValueValuationSubring v hnonarch)[X]}
    {f : K[X]} {r : ℕ}
    (hFmap : F.map (algebraMap
        (absoluteValueValuationSubring v hnonarch) K) = f)
    (hFdegree : F.natDegree = f.natDegree)
    (hfactor : F = G * H)
    (hGdegree : G.natDegree = r)
    (hrpos : 0 < r)
    (hrlt : r < F.natDegree) :
    ¬ Irreducible f

theorem

irreduciblePolynomial_polynomial_ne_zero_of_eq_X_pow_mul_of_coeff_zero_ne_zero

L93 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_polynomial_ne_zero_of_eq_X_pow_mul_of_coeff_zero_ne_zero

Documentation

The common nonvanishing step in the three irreducible-polynomial lifting Hensel routes: if a polynomial is X ^ r times a polynomial with nonzero constant coefficient, then it is nonzero.

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_polynomial_ne_zero_of_eq_X_pow_mul_of_coeff_zero_ne_zero
    {k : Type*} [Field k] {P Q : k[X]} {r : ℕ}
    (hfactor : P = Polynomial.X ^ r * Q)
    (hQ0 : Q.coeff 0 ≠ 0) :
    P ≠ 0

theorem

irreduciblePolynomial_hensel_reduction_factor_input_not_irreducible

L109 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_hensel_reduction_factor_input_not_irreducible

Documentation

Hensel obstruction: the normalized X^r residue factor input from the residue-polynomial coefficient bounds, together with the adic completeness and separatedness needed by the coefficientwise Hensel construction, contradicts irreducibility of the mapped field 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_hensel_reduction_factor_input_not_irreducible
    {K : Type*} [Field K]
    (v : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    [IsPrecomplete (IsLocalRing.maximalIdeal
      (absoluteValueValuationSubring v hnonarch))
      (absoluteValueValuationSubring v hnonarch)]
    [IsHausdorff (IsLocalRing.maximalIdeal
      (absoluteValueValuationSubring v hnonarch))
      (absoluteValueValuationSubring v hnonarch)]
    (F : (absoluteValueValuationSubring v hnonarch)[X])
    {r : ℕ}
    (hrpos : 0 < r) (hrlt : r < F.natDegree)
    (hfactor :
      F.map (IsLocalRing.residue
          (absoluteValueValuationSubring v hnonarch)) =
        Polynomial.X ^ r *
          (F.map (IsLocalRing.residue
            (absoluteValueValuationSubring v hnonarch)) /ₘ
              Polynomial.X ^ r))
    (hnatDegree : (Polynomial.X ^ r :
        (IsLocalRing.ResidueField
          (absoluteValueValuationSubring v hnonarch))[X]).natDegree =
        r)
    (hcoprime : IsCoprime (Polynomial.X ^ r)
      (F.map (IsLocalRing.residue
        (absoluteValueValuationSubring v hnonarch)) /ₘ
          Polynomial.X ^ r))
    (hQ0 : ((F.map (IsLocalRing.residue
        (absoluteValueValuationSubring v hnonarch)) /ₘ
          Polynomial.X ^ r).coeff 0) ≠ 0)
    {f : K[X]}
    (hFmap : F.map (algebraMap
        (absoluteValueValuationSubring v hnonarch) K) = f)
    (hFdegree : F.natDegree = f.natDegree) :
    ¬ Irreducible f

theorem

irreduciblePolynomial_field_coeffs_hensel_input_not_irreducible

L164 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_field_coeffs_hensel_input_not_irreducible

Documentation

coefficient form: if a field polynomial already has all coefficients in the closed unit ball, with both endpoints in the open unit ball and some coefficient on the unit sphere, then Hensel's lemma contradicts irreducibility.

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_field_coeffs_hensel_input_not_irreducible
    {K : Type*} [Field K]
    (v : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    [IsPrecomplete (IsLocalRing.maximalIdeal
      (absoluteValueValuationSubring v hnonarch))
      (absoluteValueValuationSubring v hnonarch)]
    [IsHausdorff (IsLocalRing.maximalIdeal
      (absoluteValueValuationSubring v hnonarch))
      (absoluteValueValuationSubring v hnonarch)]
    (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) :
    ¬ Irreducible f

theorem

irreduciblePolynomial_normalized_scale_hensel_input_not_irreducible

L189 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_normalized_scale_hensel_input_not_irreducible

Documentation

normalized-scale obstruction: after dividing by a coefficient whose absolute value is the positive coefficient maximum, strict endpoint inequalities force the scaled polynomial to be reducible.

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_input_not_irreducible
    {K : Type*} [Field K]
    (v : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    [IsPrecomplete (IsLocalRing.maximalIdeal
      (absoluteValueValuationSubring v hnonarch))
      (absoluteValueValuationSubring v hnonarch)]
    [IsHausdorff (IsLocalRing.maximalIdeal
      (absoluteValueValuationSubring v hnonarch))
      (absoluteValueValuationSubring v hnonarch)]
    {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
    ¬ Irreducible g := by
  let g : K[X] := Polynomial.C (f.coeff n)⁻¹ * f
  rcases irreduciblePolynomial_normalized_scale_hensel_reduction_factor_input
      v hnonarch hmpos hnmax hbound hconst hlead with
    ⟨F, r, hFmap, hFdegree, hrpos, hrlt, hfactor, hnatDegree, hcoprime, hQ0⟩
  exact irreduciblePolynomial_hensel_reduction_factor_input_not_irreducible
    v hnonarch F hrpos hrlt hfactor hnatDegree hcoprime hQ0
    hFmap hFdegree

theorem

irreduciblePolynomial_irreducible_normalized_scale_of_irreducible

L216 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_irreducible_normalized_scale_of_irreducible

Documentation

scalar normalization preserves irreducibility: multiplying by the inverse of a nonzero coefficient is multiplication by a unit.

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_irreducible_normalized_scale_of_irreducible
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    {f : K[X]} {m : ℝ} {n : ℕ}
    (hmpos : 0 < m)
    (hnmax : v (f.coeff n) = m)
    (hirr : Irreducible f) :
    Irreducible (Polynomial.C (f.coeff n)⁻¹ * f)

theorem

irreduciblePolynomial_not_both_endpoint_abs_lt_coeff_max_of_irreducible

L237 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_not_both_endpoint_abs_lt_coeff_max_of_irreducible

Documentation

endpoint contradiction: for an irreducible polynomial, the positive maximum of the coefficient absolute values cannot be strictly larger than both endpoint absolute values.

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_not_both_endpoint_abs_lt_coeff_max_of_irreducible
    {K : Type*} [Field K]
    (v : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    [IsPrecomplete (IsLocalRing.maximalIdeal
      (absoluteValueValuationSubring v hnonarch))
      (absoluteValueValuationSubring v hnonarch)]
    [IsHausdorff (IsLocalRing.maximalIdeal
      (absoluteValueValuationSubring v hnonarch))
      (absoluteValueValuationSubring v hnonarch)]
    {f : K[X]} {m : ℝ} {n : ℕ}
    (hirr : Irreducible f)
    (hmpos : 0 < m)
    (hnmax : v (f.coeff n) = m)
    (hbound : ∀ i : ℕ, v (f.coeff i) ≤ m) :
    ¬ (v (f.coeff 0) < m ∧ v f.leadingCoeff < m)

theorem

irreduciblePolynomial_coeff_max_le_endpoint_max_of_irreducible

L265 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_coeff_max_le_endpoint_max_of_irreducible

Documentation

coefficient maximum estimate for a chosen positive coefficient 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_coeff_max_le_endpoint_max_of_irreducible
    {K : Type*} [Field K]
    (v : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    [IsPrecomplete (IsLocalRing.maximalIdeal
      (absoluteValueValuationSubring v hnonarch))
      (absoluteValueValuationSubring v hnonarch)]
    [IsHausdorff (IsLocalRing.maximalIdeal
      (absoluteValueValuationSubring v hnonarch))
      (absoluteValueValuationSubring v hnonarch)]
    {f : K[X]} {m : ℝ} {n : ℕ}
    (hirr : Irreducible f)
    (hmpos : 0 < m)
    (hnmax : v (f.coeff n) = m)
    (hbound : ∀ i : ℕ, v (f.coeff i) ≤ m) :
    m ≤ max (v (f.coeff 0)) (v f.leadingCoeff)

theorem

irreduciblePolynomial_coeff_abs_le_endpoint_max_of_irreducible

L293 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_coeff_abs_le_endpoint_max_of_irreducible

Documentation

coefficient estimate: every coefficient of an irreducible polynomial is bounded by the larger of the degree-zero and leading 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 irreduciblePolynomial_coeff_abs_le_endpoint_max_of_irreducible
    {K : Type*} [Field K]
    (v : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    [IsPrecomplete (IsLocalRing.maximalIdeal
      (absoluteValueValuationSubring v hnonarch))
      (absoluteValueValuationSubring v hnonarch)]
    [IsHausdorff (IsLocalRing.maximalIdeal
      (absoluteValueValuationSubring v hnonarch))
      (absoluteValueValuationSubring v hnonarch)]
    {f : K[X]} (hirr : Irreducible f) :
    ∀ i : ℕ, v (f.coeff i) ≤ max (v (f.coeff 0)) (v f.leadingCoeff)

theorem

irreduciblePolynomial_monic_coeff_abs_le_one_of_const_abs_le_one_of_irreducible

L316 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_monic_coeff_abs_le_one_of_const_abs_le_one_of_irreducible

Documentation

monic consequence: if an irreducible monic polynomial has degree-zero coefficient in the closed unit ball, then every coefficient lies 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_monic_coeff_abs_le_one_of_const_abs_le_one_of_irreducible
    {K : Type*} [Field K]
    (v : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    [IsPrecomplete (IsLocalRing.maximalIdeal
      (absoluteValueValuationSubring v hnonarch))
      (absoluteValueValuationSubring v hnonarch)]
    [IsHausdorff (IsLocalRing.maximalIdeal
      (absoluteValueValuationSubring v hnonarch))
      (absoluteValueValuationSubring v hnonarch)]
    {f : K[X]} (hirr : Irreducible f)
    (hmonic : f.Monic)
    (hconst : v (f.coeff 0) ≤ 1) :
    ∀ i : ℕ, v (f.coeff i) ≤ 1

theorem

irreduciblePolynomial_exists_valuation_lift_of_monic_const_abs_le_one_of_irreducible

L343 ↗

AlgebraicNumberTheory.Valuations.irreduciblePolynomial_exists_valuation_lift_of_monic_const_abs_le_one_of_irreducible

Documentation

monic lift consequence: the preceding coefficient bound gives a degree-preserving lift to the closed-unit-ball valuation ring.

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_valuation_lift_of_monic_const_abs_le_one_of_irreducible
    {K : Type*} [Field K]
    (v : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    [IsPrecomplete (IsLocalRing.maximalIdeal
      (absoluteValueValuationSubring v hnonarch))
      (absoluteValueValuationSubring v hnonarch)]
    [IsHausdorff (IsLocalRing.maximalIdeal
      (absoluteValueValuationSubring v hnonarch))
      (absoluteValueValuationSubring v hnonarch)]
    {f : K[X]} (hirr : Irreducible f)
    (hmonic : f.Monic)
    (hconst : v (f.coeff 0) ≤ 1) :
    ∃ F : (absoluteValueValuationSubring v hnonarch)[X],
      F.map (algebraMap
          (absoluteValueValuationSubring v hnonarch) K) = f ∧
        F.natDegree = f.natDegree

Module documentation

Hensel obstruction to irreducibility

Declarations