NYLL
Module

NormFormulaCoefficients.lean

Nyll.ValuedFieldTheory.Valuation.AbsoluteValue.AlgebraicExtension.NormFormulaCoefficients
5 declarations indexed from sourceView source ↗

Module documentation

coefficient bound from primitive Hensel factorization

This file reuses the algebraic normalization and irreducibility obstruction from the irreducible-polynomial coefficient bounds. The factor lift is supplied directly by the factorization form of Hensel's lemma in the primitive factorization definition, so no completeness or separatedness hypothesis is needed.

Imports2
Imported by9

Declarations

theorem

normFormula_hensel_reduction_factor_input_not_irreducible_of_henselFactorization

L31 ↗
AlgebraicNumberTheory.Valuations.normFormula_hensel_reduction_factor_input_not_irreducible_of_henselFactorization
Documentation

The normalized residual factor input from the irreducible-polynomial coefficient bounds contradicts irreducibility as soon as the valuation ring satisfies the construction's factorization form of Hensel's lemma.

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 normFormula_hensel_reduction_factor_input_not_irreducible_of_henselFactorization
    {K : Type*} [Field K]
    (v : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hv : ValuationTheory.DiscreteValuationField.HenselFactorizationProperty
      (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

normFormula_normalized_scale_not_irreducible_of_henselFactorization

L79 ↗
AlgebraicNumberTheory.Valuations.normFormula_normalized_scale_not_irreducible_of_henselFactorization
Documentation

Scaling by a coefficient of positive maximum value and applying the construction Hensel factorization contradicts irreducibility when both endpoint values are strictly below that 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 · full declaration
theorem normFormula_normalized_scale_not_irreducible_of_henselFactorization
    {K : Type*} [Field K]
    (v : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hv : ValuationTheory.DiscreteValuationField.HenselFactorizationProperty
      (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
    normFormula_hensel_reduction_factor_input_not_irreducible_of_henselFactorization
      v hnonarch hv F hrpos hrlt hfactor hnatDegree hcoprime hQ0
      hFmap hFdegree
theorem

normFormula_coeff_max_le_endpoint_max_of_irreducible_of_henselFactorization

L103 ↗
AlgebraicNumberTheory.Valuations.normFormula_coeff_max_le_endpoint_max_of_irreducible_of_henselFactorization
Documentation

Under primitive Hensel factorization, a positive coefficient maximum of an irreducible polynomial is bounded by the larger endpoint value.

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 normFormula_coeff_max_le_endpoint_max_of_irreducible_of_henselFactorization
    {K : Type*} [Field K]
    (v : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hv : ValuationTheory.DiscreteValuationField.HenselFactorizationProperty
      (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

normFormula_coeff_abs_le_endpoint_max_of_irreducible_of_henselFactorization

L133 ↗
AlgebraicNumberTheory.Valuations.normFormula_coeff_abs_le_endpoint_max_of_irreducible_of_henselFactorization
Documentation

the finite norm-formula theorem coefficient source: primitive Hensel factorization alone bounds every coefficient of an irreducible polynomial by its two endpoint 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 normFormula_coeff_abs_le_endpoint_max_of_irreducible_of_henselFactorization
    {K : Type*} [Field K]
    (v : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hv : ValuationTheory.DiscreteValuationField.HenselFactorizationProperty
      (absoluteValueValuationSubring v hnonarch))
    {f : K[X]} (hirr : Irreducible f) :
    ∀ i : ℕ, v (f.coeff i) ≤ max (v (f.coeff 0)) (v f.leadingCoeff)
theorem

normFormula_monic_coeff_abs_le_one_of_const_abs_le_one_of_henselFactorization

L151 ↗
AlgebraicNumberTheory.Valuations.normFormula_monic_coeff_abs_le_one_of_const_abs_le_one_of_henselFactorization
Documentation

the finite norm-formula theorem monic specialization: if the constant coefficient of an irreducible monic polynomial lies in the closed unit ball, then every coefficient lies there.

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 normFormula_monic_coeff_abs_le_one_of_const_abs_le_one_of_henselFactorization
    {K : Type*} [Field K]
    (v : AbsoluteValue K ℝ) (hnonarch : LubinTate.Valuations.NonarchimedeanAbsoluteValue v)
    (hv : ValuationTheory.DiscreteValuationField.HenselFactorizationProperty
      (absoluteValueValuationSubring v hnonarch))
    {f : K[X]} (hirr : Irreducible f)
    (hmonic : f.Monic)
    (hconst : v (f.coeff 0) ≤ 1) :
    ∀ i : ℕ, v (f.coeff i) ≤ 1

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