Divisibility of integers by powers of a prime, read in a domain

Let p be a prime number and R an integral domain in which the image of p is nonzero and not a unit, for instance a discrete valuation ring with uniformiser p such as ℤ_[p] or the localisation of ℤ at p. Then the cast ℤ → R reflects divisibility by powers of p: (p : R) ^ n ∣ (x : R) exactly when p ^ n ∣ x in ℤ. Divisibility conditions on integral Weierstrass coefficients can therefore be checked over ℤ, by computation, and read over R.

The proof peels off one factor of p at a time: if p does not divide an integer y, then p and y are coprime in ℤ, so (p : R) ∣ (y : R) would make (p : R) divide 1.

If moreover every element of R is congruent to an integer modulo p, as when R has residue field 𝔽_p, then roots modulo p in R of an integer polynomial are read in ZMod p, where they can be found by a finite search.

Main results

• Nat.Prime.pow_dvd_intCast_iff: (p : R) ^ n ∣ (x : R) ↔ (p : ℤ) ^ n ∣ x.
• Nat.Prime.exists_dvd_eval_map_iff: an integer polynomial has a root modulo p in R exactly when it has a root in ZMod p.
• Nat.Prime.not_dvd_eval_map_of_forall_ne_zero: an integer polynomial with no root in ZMod p has no root modulo p in R.

theorem Nat.Prime.pow_dvd_intCast_iff {p : ℕ} (hp : Prime p) {R : Type u_1} [CommRing R] [IsDomain R] (h₀ : ↑p ≠ 0) (hu : ¬IsUnit ↑p) (n : ℕ) (x : ℤ) : ↑p ^ n ∣ ↑x ↔ ↑p ^ n ∣ x

Over a domain in which a prime p is a nonzero nonunit, divisibility of integers by powers of p can be read in ℤ. This is the general form of PadicInt.pow_p_dvd_int_iff.

theorem Nat.Prime.exists_dvd_eval_map_iff {p : ℕ} (hp : Prime p) {R : Type u_1} [CommRing R] [IsDomain R] (h₀ : ↑p ≠ 0) (hu : ¬IsUnit ↑p) (hR : ∀ (x : R), ∃ (n : ℤ), ↑p ∣ x - ↑n) (f : Polynomial ℤ) : (∃ (s : R), ↑p ∣ Polynomial.eval s (Polynomial.map (Int.castRingHom R) f)) ↔ ∃ (x : ZMod p), Polynomial.eval x (Polynomial.map (Int.castRingHom (ZMod p)) f) = 0

Roots modulo p of an integer polynomial are read in ZMod p over a domain R in which the prime p is a nonzero nonunit and every element is congruent to an integer modulo p, for instance a discrete valuation ring with uniformiser p and residue field 𝔽_p.

theorem Nat.Prime.not_dvd_eval_map_of_forall_ne_zero {p : ℕ} (hp : Prime p) {R : Type u_1} [CommRing R] [IsDomain R] (h₀ : ↑p ≠ 0) (hu : ¬IsUnit ↑p) (hR : ∀ (x : R), ∃ (n : ℤ), ↑p ∣ x - ↑n) {f : Polynomial ℤ} (hf : ∀ (x : ZMod p), Polynomial.eval x (Polynomial.map (Int.castRingHom (ZMod p)) f) ≠ 0) (s : R) : ¬↑p ∣ Polynomial.eval s (Polynomial.map (Int.castRingHom R) f)

An integer polynomial with no root in ZMod p has no root modulo p over a domain R as in Nat.Prime.exists_dvd_eval_map_iff. The hypothesis on ZMod p is a finite search.