Polynomial systems after arithmetic-progression substitution

noncomputable def NairTenenbaum.rationalAffineEquiv (q : ℕ) (a : ℤ) (hq : q ≠ 0) : Polynomial ℚ ≃ₐ[ℚ] Polynomial ℚ

Over the rationals an affine substitution with nonzero slope is an algebra automorphism, so it preserves irreducible factors and their nonassociation.

Equations

• NairTenenbaum.rationalAffineEquiv q a hq = Polynomial.algEquivCMulXAddC ↑q ↑a

theorem NairTenenbaum.rationalAffineEquiv_map (q : ℕ) (a : ℤ) (hq : q ≠ 0) (Q : Polynomial ℤ) : (rationalAffineEquiv q a hq) (Polynomial.map (Int.castRingHom ℚ) Q) = Polynomial.map (Int.castRingHom ℚ) (Q.comp (affinePolynomial q a))

@[simp]

theorem NairTenenbaum.natDegree_affinePolynomial {q : ℕ} (hq : q ≠ 0) (a : ℤ) : (affinePolynomial q a).natDegree = 1

noncomputable def NairTenenbaum.PolynomialSystem.affine {k r : ℕ} (P : PolynomialSystem k r) (q : ℕ) (a : ℤ) (hq : q ≠ 0) (hqa : q.Coprime (Polynomial.eval a P.total).natAbs) : PolynomialSystem k r

The substituted polynomial family, with all factorization hypotheses proved from the original family and the progression's coprimality condition.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NairTenenbaum.PolynomialSystem.affine_total {k r : ℕ} (P : PolynomialSystem k r) (q : ℕ) (a : ℤ) (hq : q ≠ 0) (hqa : q.Coprime (Polynomial.eval a P.total).natAbs) : (P.affine q a hq hqa).total = P.total.comp (affinePolynomial q a)

@[simp]

theorem NairTenenbaum.PolynomialSystem.affine_radical {k r : ℕ} (P : PolynomialSystem k r) (q : ℕ) (a : ℤ) (hq : q ≠ 0) (hqa : q.Coprime (Polynomial.eval a P.total).natAbs) : (P.affine q a hq hqa).radical = P.radical.comp (affinePolynomial q a)

theorem NairTenenbaum.PolynomialSystem.affine_degree {k r : ℕ} (P : PolynomialSystem k r) (q : ℕ) (a : ℤ) (hq : q ≠ 0) (hqa : q.Coprime (Polynomial.eval a P.total).natAbs) : (P.affine q a hq hqa).total.natDegree = P.total.natDegree

theorem NairTenenbaum.PolynomialSystem.affine_factor_rootCount {k r : ℕ} (P : PolynomialSystem k r) (q : ℕ) (a : ℤ) (hq : q ≠ 0) (hqa : q.Coprime (Polynomial.eval a P.total).natAbs) (i : Fin r) (n : ℕ) : rootCount ((P.affine q a hq hqa).R i) n = if q.Coprime n then rootCount (P.R i) n else 0

The transformed irreducible root counts vanish precisely on the moduli excluded by the progression; on coprime moduli they are unchanged.