Reducing the roots of an integer polynomial modulo a prime

Let f be a monic integer polynomial which splits in a number field M and is squarefree modulo a prime p. The roots of f in M are algebraic integers, so any ring homomorphism ρ : 𝓞 M →+* k to a domain k over 𝔽_p can be applied to them. Their images are all the roots of f mod p in k, counted with multiplicity, and these are distinct because f mod p is squarefree over the perfect field 𝔽_p. So f mod p splits in k, and reduction along ρ is a bijection between the root sets.

Main results

• TauCeti.NumberField.splits_and_exists_rootSet_equiv_of_squarefree_map_zmod: f mod p splits in k, and reduction along ρ is a bijection from the roots of f in M onto the roots of f mod p in k.

theorem TauCeti.NumberField.splits_and_exists_rootSet_equiv_of_squarefree_map_zmod {M : Type u_1} [Field M] [NumberField M] {f : Polynomial ℤ} {p : ℕ} [Fact (Nat.Prime p)] (hf : f.Monic) (hsq : Squarefree (Polynomial.map (Int.castRingHom (ZMod p)) f)) (hsplit : (Polynomial.map (algebraMap ℚ M) (Polynomial.map (Int.castRingHom ℚ) f)).Splits) {k : Type u_2} [CommRing k] [IsDomain k] [Algebra (ZMod p) k] (ρ : NumberField.RingOfIntegers M →+* k) : (Polynomial.map (algebraMap (ZMod p) k) (Polynomial.map (Int.castRingHom (ZMod p)) f)).Splits ∧ ∃ (e : ↑((Polynomial.map (Int.castRingHom ℚ) f).rootSet M) ≃ ↑((Polynomial.map (Int.castRingHom (ZMod p)) f).rootSet k)), ∀ (x : ↑((Polynomial.map (Int.castRingHom ℚ) f).rootSet M)) (y : NumberField.RingOfIntegers M), (algebraMap (NumberField.RingOfIntegers M) M) y = ↑x → ↑(e x) = ρ y

Reducing the roots of f modulo a prime. Let f be monic, split in M, and squarefree modulo p, and let ρ : 𝓞 M →+* k be a ring homomorphism to a domain k over 𝔽_p. Then f mod p splits in k, and reduction along ρ is a bijection from the roots of f in M onto the roots of f mod p in k.