Constructing the polynomial factorization data

The union of the normalized integral factors of the original polynomials provides a finite common factor family. Primitivity follows from the no-fixed-prime condition; Gauss's lemma therefore supplies the rational irreducibility and nonassociation required by PolynomialSystem.

theorem NairTenenbaum.exists_sign_mul_normalizedFactors (Q : Polynomial ℤ) (hQ : Q ≠ 0) : ∃ (s : ℤ), s.natAbs = 1 ∧ Q = Polynomial.C s * (UniqueFactorizationMonoid.normalizedFactors Q).prod

Factoring a nonzero integral polynomial leaves only a unit sign.

theorem NairTenenbaum.not_associated_map_of_normalized {P Q : Polynomial ℤ} (hP : P.IsPrimitive) (hQ : Q.IsPrimitive) (hnP : normalize P = P) (hnQ : normalize Q = Q) (hne : P ≠ Q) : ¬Associated (Polynomial.map (Int.castRingHom ℚ) P) (Polynomial.map (Int.castRingHom ℚ) Q)

Distinct normalized primitive integral polynomials cannot become associated after extension of scalars to the rationals.

theorem NairTenenbaum.exists_polynomialSystem {k : ℕ} (Q : Fin k → Polynomial ℤ) (hfixed : NoFixedPrimeDivisor (∏ j : Fin k, Q j)) : ∃ (r : ℕ) (P : PolynomialSystem k r), P.Q = Q

Every admissible polynomial family has all the data required by the analytic theorems. Constant unit polynomials and empty families are included.

noncomputable def NairTenenbaum.familySystem {k : ℕ} (Q : Fin k → Polynomial ℤ) (hfixed : NoFixedPrimeDivisor (∏ j : Fin k, Q j)) : (r : ℕ) × PolynomialSystem k r

A selected common factorization of the original polynomial family.

Equations

• NairTenenbaum.familySystem Q hfixed = ⟨Classical.choose ⋯, Classical.choose ⋯⟩

@[simp]

theorem NairTenenbaum.familySystem_Q {k : ℕ} (Q : Fin k → Polynomial ℤ) (hfixed : NoFixedPrimeDivisor (∏ j : Fin k, Q j)) : (familySystem Q hfixed).snd.Q = Q

@[simp]

theorem NairTenenbaum.familySystem_total {k : ℕ} (Q : Fin k → Polynomial ℤ) (hfixed : NoFixedPrimeDivisor (∏ j : Fin k, Q j)) : (familySystem Q hfixed).snd.total = ∏ j : Fin k, Q j