p-adic valuations of polynomials

StructureDilatation of a p-adic polynomial at a point#✓fully proved

Let \(p\) be a prime, \(f \in \mathbb{Z}_p[X]\) and \(x_0 \in \mathbb{Z}_p\). Dilatation data for \(f\) at \(x_0\) consist of a natural number \(e\) and a polynomial \(g \in \mathbb{Z}_p[X]\) such that \(g(X) = p^{-e} f(x_0 + pX)\) as polynomials over \(\mathbb{Q}_p\), and the reduction of \(g\) modulo \(p\) is nonzero.

structure PadicPolynomialDilatation (p : ℕ) [Fact p.Prime]
    (f : Polynomial (PadicInt p)) (x0 : PadicInt p) where
  exp : ℕ
  poly : Polynomial (PadicInt p)
  dilat_eq :
    Polynomial.map (algebraMap (PadicInt p) (Padic p)) poly =
      Polynomial.C (((p : Padic p) ^ exp)⁻¹) *
        Polynomial.map (algebraMap (PadicInt p) (Padic p))
          (f.comp (Polynomial.C x0 + Polynomial.C (p : PadicInt p) * Polynomial.X))
  red_ne_zero : Polynomial.map PadicInt.toZMod poly ≠ 0

Used by 2

Used byExistence of dilatations of p-adic polynomials · Dilatation of the constant polynomial one at zero

DefinitionDilatation of the constant polynomial one at zero#✓fully proved

For every prime \(p\), the exponent \(e = 0\) and the polynomial \(g = 1\) form dilatation data for the constant polynomial \(1 \in \mathbb{Z}_p[X]\) at the point \(x_0 = 0\).

noncomputable def padicPolynomialDilatation_one_zero (p : ℕ) [Fact p.Prime] :
    PadicPolynomialDilatation p 1 0 where
  exp := 0
  poly := 1
  dilat_eq := by
    simp only [Polynomial.one_comp, Polynomial.map_one, pow_zero, inv_one,
      Polynomial.C_1, mul_one]
  red_ne_zero := by
    simp only [Polynomial.map_one]
    exact one_ne_zero

Uses 1

Statement usesDilatation of a p-adic polynomial at a point

TheoremExistence of dilatations of p-adic polynomials#✓fully proved

Let \(p\) be a prime and let \(f \in \mathbb{Z}_p[X]\) have nonzero reduction modulo \(p\). Then for every \(x_0 \in \mathbb{Z}_p\) there are a natural number \(e\) and a polynomial \(g \in \mathbb{Z}_p[X]\) with nonzero reduction modulo \(p\) such that \(g(X) = p^{-e} f(x_0 + pX)\) as polynomials over \(\mathbb{Q}_p\); that is, dilatation data for \(f\) at \(x_0\) exist.

theorem padicPolynomialDilatation_exists (p : ℕ) [Fact p.Prime]
    (f : Polynomial (PadicInt p)) (x0 : PadicInt p)
    (hf : Polynomial.map PadicInt.toZMod f ≠ 0) :
    Nonempty (PadicPolynomialDilatation p f x0)

Uses 1

Statement usesDilatation of a p-adic polynomial at a point

DefinitionThe \(p\)-adic valuation of an integer polynomial#✓fully proved

Let \(p\) be a prime and let \(f \in \mathbb{Z}[X]\) be a nonzero polynomial, with \(a_n\) the coefficient of \(X^n\) in \(f\). Writing \(v_p(a)\) for the \(p\)-adic valuation of an integer \(a\), the \(p\)-adic valuation of \(f\) is the natural number \(v_p(f) = \min \{ v_p(a_n) : a_n \neq 0 \}\).

@[nolint unusedArguments]
def padicValuation (p : ℕ) (_hp : Nat.Prime p) (f : Polynomial ℤ) (hf : f ≠ 0) : ℕ :=
  (f.support.image (fun n => padicValInt p (f.coeff n))).min'
    ((support_nonempty.mpr hf).image fun n => padicValInt p (f.coeff n))

Used by 3

Used byLower bounds for the valuation of a polynomial · The valuation of a nonzero constant polynomial · The valuation of a polynomial is at most that of each nonzero coefficient

TheoremThe valuation of a polynomial is at most that of each nonzero coefficient#✓fully proved

Let \(p\) be a prime, write \(v_p(a)\) for the \(p\)-adic valuation of an integer \(a\), let \(f \in \mathbb{Z}[X]\) be a nonzero polynomial with \(a_n\) the coefficient of \(X^n\) in \(f\), and let \(v_p(f) = \min \{ v_p(a_n) : a_n \neq 0 \}\) be its \(p\)-adic valuation. If \(a_n \neq 0\), then \(v_p(f) \le v_p(a_n)\).

theorem padicValuation_le_coeff {p : ℕ} {hp : Nat.Prime p} {f : Polynomial ℤ} {hf : f ≠ 0}
    {n : ℕ} (hn : n ∈ f.support) :
    padicValuation p hp f hf ≤ padicValInt p (f.coeff n)

Uses 1 · Used by 1

Statement usesThe \(p\)-adic valuation of an integer polynomial

Used byThe valuation of a nonzero constant polynomial

TheoremLower bounds for the valuation of a polynomial#✓fully proved

Let \(p\) be a prime, write \(v_p(a)\) for the \(p\)-adic valuation of an integer \(a\), let \(f \in \mathbb{Z}[X]\) be a nonzero polynomial with \(a_n\) the coefficient of \(X^n\) in \(f\), and let \(v_p(f) = \min \{ v_p(a_n) : a_n \neq 0 \}\) be its \(p\)-adic valuation. If \(k\) is a natural number with \(k \le v_p(a_n)\) for every \(n\) with \(a_n \neq 0\), then \(k \le v_p(f)\).

theorem le_padicValuation {p : ℕ} {hp : Nat.Prime p} {f : Polynomial ℤ} {hf : f ≠ 0}
    {k : ℕ} (hk : ∀ n ∈ f.support, k ≤ padicValInt p (f.coeff n)) :
    k ≤ padicValuation p hp f hf

Uses 1 · Used by 1

Statement usesThe \(p\)-adic valuation of an integer polynomial

Used byThe valuation of a nonzero constant polynomial

TheoremThe valuation of a nonzero constant polynomial#✓fully proved

Let \(p\) be a prime and let \(a\) be a nonzero integer. The \(p\)-adic valuation of the constant polynomial \(a \in \mathbb{Z}[X]\), the minimum of the \(p\)-adic valuations of its nonzero coefficients, equals the \(p\)-adic valuation \(v_p(a)\) of the integer \(a\).

@[simp]
theorem padicValuation_C (p : ℕ) (hp : Nat.Prime p) (a : ℤ) (ha : a ≠ 0) :
    padicValuation p hp (C a) (C_ne_zero.mpr ha) = padicValInt p a

Uses 3

Statement usesThe \(p\)-adic valuation of an integer polynomial

Proof usesLower bounds for the valuation of a polynomial · The valuation of a polynomial is at most that of each nonzero coefficient

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.