Module

PolynomialImageInfinite.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.PolynomialImageInfinite

6 declarations indexed from sourceView source ↗

Module documentation

Infinite additive quotients from a discrete valuation

The valuation argument underlying Proposition 2.4 of Bary-Soroker--Nguyen, On the embedding problem for Galois groups (arXiv:1008.1879), specializes here to discrete valuations. At sufficiently large values the leading term of a monic polynomial dominates. Uniformizer powers whose value exponents are not divisible by the degree then give infinitely many distinct additive classes. No characteristic or completeness assumption is needed for that argument. The final theorem applies it to the Artin--Schreier polynomial.

Imports10

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.Normalized
Mathlib.Algebra.Polynomial.Eval.Degree
Mathlib.Algebra.Order.GroupWithZero.Canonical
Mathlib.GroupTheory.QuotientGroup.Defs
Mathlib.Tactic.Linarith
Mathlib.Tactic.Ring
Mathlib.Tactic.Convert
Mathlib.Data.Finset.Lattice.Fold
Mathlib.Algebra.CharP.Frobenius
Lean.Elab.Tactic.Omega

Imported by2

theorem

valuation_monic_eval_eq_of_coeff_lt

L35 ↗

ValuationTheory.DiscreteValuationField.valuation_monic_eval_eq_of_coeff_lt

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Polynomial
namespace ValuationTheory.DiscreteValuationField
universe u v

Lean source · statement

theorem valuation_monic_eval_eq_of_coeff_lt
    {K : Type u} [Field K] {Γ : Type v} [LinearOrderedCommGroupWithZero Γ]
    (w : _root_.Valuation K Γ) (f : K[X]) (hf : f.Monic)
    (B : Γ) (hB : 1 ≤ B)
    (hcoeff : ∀ i ∈ Finset.range (f.natDegree + 1), w (f.coeff i) ≤ B)
    (x : K) (hx : B < w x) : w (f.eval x) = w x ^ f.natDegree

theorem

valuation_eval_le_of_coeff_le

L60 ↗

ValuationTheory.DiscreteValuationField.valuation_eval_le_of_coeff_le

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Polynomial
namespace ValuationTheory.DiscreteValuationField
universe u v

Lean source · statement

theorem valuation_eval_le_of_coeff_le
    {K : Type u} [Field K] {Γ : Type v} [LinearOrderedCommGroupWithZero Γ]
    (w : _root_.Valuation K Γ) (f : K[X])
    (B : Γ) (hB : 1 ≤ B)
    (hcoeff : ∀ i ∈ Finset.range (f.natDegree + 1), w (f.coeff i) ≤ B)
    (x : K) (hx : w x ≤ B) : w (f.eval x) ≤ B ^ (f.natDegree + 1)

theorem

exists_coefficient_bound

L76 ↗

ValuationTheory.DiscreteValuationField.exists_coefficient_bound

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Polynomial
namespace ValuationTheory.DiscreteValuationField
universe u v

Lean source · statement

theorem exists_coefficient_bound
    {K : Type u} [Field K] (w : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    (f : K[X]) :
    ∃ M : ℕ, ∀ i ∈ Finset.range (f.natDegree + 1),
      w (f.coeff i) ≤ WithZero.exp (M : ℤ)

theorem

exists_sequence_sub_not_mem_polynomial_range

L90 ↗

ValuationTheory.DiscreteValuationField.DVF.exists_sequence_sub_not_mem_polynomial_range

Documentation

Every monic polynomial of degree greater than one has infinitely many pairwise distinct additive image classes over a discretely valued field.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Polynomial
namespace ValuationTheory.DiscreteValuationField
universe u v

Lean source · statement

theorem DVF.exists_sequence_sub_not_mem_polynomial_range
    {K : Type u} [Field K] (D : DVF.{u, v} K)
    (f : K[X]) (hf : f.Monic) (hd : 1 < f.natDegree) :
    ∃ a : ℕ → K, ∀ i j : ℕ, i ≠ j → a i - a j ∉ Set.range f.eval

theorem

infinite_quotient_range_of_monic_polynomial

L159 ↗

ValuationTheory.DiscreteValuationField.DVF.infinite_quotient_range_of_monic_polynomial

Documentation

The quotient by the image of an additive monic polynomial of degree at least two is infinite over every discretely valued field.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Polynomial
namespace ValuationTheory.DiscreteValuationField
universe u v

Lean source · statement

theorem DVF.infinite_quotient_range_of_monic_polynomial
    {K : Type u} [Field K] (D : DVF.{u, v} K)
    (f : K[X]) (hf : f.Monic) (hd : 1 < f.natDegree)
    (F : K →+ K) (hF : ∀ x : K, F x = f.eval x) :
    Infinite (K ⧸ F.range)

theorem

infinite_artinSchreier_quotient

L174 ↗

ValuationTheory.DiscreteValuationField.DVF.infinite_artinSchreier_quotient

Documentation

The Artin--Schreier quotient of a discretely valued field is infinite.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Polynomial
namespace ValuationTheory.DiscreteValuationField
universe u v

Lean source · statement

theorem DVF.infinite_artinSchreier_quotient
    {K : Type u} [Field K] (D : DVF.{u, v} K)
    (p : ℕ) [Fact p.Prime] [CharP K p] :
    Infinite (K ⧸ ((frobenius K p).toAddMonoidHom - AddMonoidHom.id K).range)

Module documentation

Infinite additive quotients from a discrete valuation

Declarations

valuation_monic_eval_eq_of_coeff_lt

valuation_eval_le_of_coeff_le

exists_coefficient_bound

exists_sequence_sub_not_mem_polynomial_range

infinite_quotient_range_of_monic_polynomial

infinite_artinSchreier_quotient