Root counts at prime powers

Reduction modulo a prime is injective on roots whose derivative is nonzero modulo that prime. In particular separable reduction gives a bound independent of the exponent of the prime power.

noncomputable def NairTenenbaum.rootsReduce (Q : Polynomial ℤ) {m n : ℕ} (hmn : m ∣ n) : ResidueRoots Q n → ResidueRoots Q m

Reduction of a root to a divisor of its modulus.

Equations

• NairTenenbaum.rootsReduce Q hmn a = ⟨(ZMod.castHom hmn (ZMod m)) ↑a, ⋯⟩

theorem NairTenenbaum.rootCount_eq_zero_of_dvd {Q : Polynomial ℤ} {m n : ℕ} (hm : m ≠ 0) (hmn : m ∣ n) (hQ : rootCount Q m = 0) : rootCount Q n = 0

A congruence with no roots remains root-free at every multiple of its modulus.

theorem NairTenenbaum.rootsReduce_injective_of_simple {Q : Polynomial ℤ} {p ν : ℕ} (hp : Nat.Prime p) (hν : ν ≠ 0) (hsimple : ∀ (a : ResidueRoots Q p), Polynomial.eval₂ (Int.castRingHom (ZMod p)) (↑a) (Polynomial.derivative Q) ≠ 0) : Function.Injective (rootsReduce Q ⋯)

Uniqueness of a simple root above its residue modulo p.

theorem NairTenenbaum.rootCount_prime_pow_le_of_simple {Q : Polynomial ℤ} {p ν : ℕ} (hp : Nat.Prime p) (hν : ν ≠ 0) (hsimple : ∀ (a : ResidueRoots Q p), Polynomial.eval₂ (Int.castRingHom (ZMod p)) (↑a) (Polynomial.derivative Q) ≠ 0) : rootCount Q (p ^ ν) ≤ rootCount Q p

theorem NairTenenbaum.rootCount_prime_pow_le {Q : Polynomial ℤ} {p ν : ℕ} (hp : Nat.Prime p) (hν : ν ≠ 0) (hsep : (Polynomial.map (Int.castRingHom (ZMod p)) Q).Separable) : rootCount Q (p ^ ν) ≤ rootCount Q p

The prime-power root bound for a polynomial with separable reduction.