Monic polynomials with prescribed reductions

A finite family of monic polynomials of the same degree, over pairwise coprime residue rings, lifts simultaneously to a monic integer polynomial of that degree. In particular, one can prescribe reductions modulo 2, 3, and 5 independently. This is the coefficient-gluing step in the three-prime construction of polynomials with symmetric Galois group.

The Chinese remainder equivalence is Mathlib's ZMod.prodEquivPi. The lifted coefficients are assembled by TauCeti.Polynomial.monicOfCoeff, which fixes the leading term to be X ^ n. No primality or nonzero-degree hypothesis is needed.

theorem TauCeti.exists_monic_int_polynomial_map_zmod_eq {ι : Type u_1} [Finite ι] (m : ι → ℕ) (hcop : Pairwise fun (i j : ι) => (m i).Coprime (m j)) (n : ℕ) (g : (i : ι) → Polynomial (ZMod (m i))) (hmonic : ∀ (i : ι), (g i).Monic) (hdegree : ∀ (i : ι), (g i).natDegree = n) : ∃ (f : Polynomial ℤ), f.Monic ∧ f.natDegree = n ∧ ∀ (i : ι), Polynomial.map (Int.castRingHom (ZMod (m i))) f = g i

Monic polynomials of a common degree over pairwise coprime residue rings have a simultaneous monic lift to ℤ of the same degree. The index type may be empty, and the moduli need not be prime.

theorem TauCeti.exists_monic_int_polynomial_map_two_three_five_eq (n : ℕ) (g2 : Polynomial (ZMod 2)) (g3 : Polynomial (ZMod 3)) (g5 : Polynomial (ZMod 5)) (h2 : g2.Monic) (h3 : g3.Monic) (h5 : g5.Monic) (d2 : g2.natDegree = n) (d3 : g3.natDegree = n) (d5 : g5.natDegree = n) : ∃ (f : Polynomial ℤ), f.Monic ∧ f.natDegree = n ∧ Polynomial.map (Int.castRingHom (ZMod 2)) f = g2 ∧ Polynomial.map (Int.castRingHom (ZMod 3)) f = g3 ∧ Polynomial.map (Int.castRingHom (ZMod 5)) f = g5

Prescribed monic reductions modulo 2, 3, and 5 lift to one monic integer polynomial of the same degree.