The factorization data for irreducible pairwise coprime families

noncomputable def NairTenenbaum.PolynomialSystem.ofIrreducible {k : ℕ} (Q : Fin k → Polynomial ℤ) (hQ : ∀ (j : Fin k), Irreducible (Polynomial.map (Int.castRingHom ℚ) (Q j))) (hcoprime : ∀ (i j : Fin k), i ≠ j → IsCoprime (Polynomial.map (Int.castRingHom ℚ) (Q i)) (Polynomial.map (Int.castRingHom ℚ) (Q j))) (hfixed : NoFixedPrimeDivisor (∏ j : Fin k, Q j)) : PolynomialSystem k k

For an irreducible pairwise coprime family, the original polynomials already provide all factorization data, with the identity exponent matrix.

Equations

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

@[simp]

theorem NairTenenbaum.PolynomialSystem.ofIrreducible_total {k : ℕ} (Q : Fin k → Polynomial ℤ) (hQ : ∀ (j : Fin k), Irreducible (Polynomial.map (Int.castRingHom ℚ) (Q j))) (hcoprime : ∀ (i j : Fin k), i ≠ j → IsCoprime (Polynomial.map (Int.castRingHom ℚ) (Q i)) (Polynomial.map (Int.castRingHom ℚ) (Q j))) (hfixed : NoFixedPrimeDivisor (∏ j : Fin k, Q j)) : (ofIrreducible Q hQ hcoprime hfixed).total = ∏ j : Fin k, Q j

theorem NairTenenbaum.NoFixedPrimeDivisor.isPrimitive {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) : Q.IsPrimitive

A fixed content prime would make the polynomial identically zero modulo that prime. Thus the no-fixed-prime condition supplies primitivity.

theorem NairTenenbaum.NoFixedPrimeDivisor.irreducible_map {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) (hI : Irreducible Q) : Irreducible (Polynomial.map (Int.castRingHom ℚ) Q)

Gauss's lemma transfers the paper's integral irreducibility hypothesis to the rational factorization interface.

noncomputable def NairTenenbaum.irreducibleBadDiscriminant {k : ℕ} (Q : Fin k → Polynomial ℤ) : ℕ

Restricted discriminant of an irreducible family, expressed directly in terms of the product polynomial.

Equations

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

@[simp]

theorem NairTenenbaum.PolynomialSystem.ofIrreducible_badDiscriminant {k : ℕ} (Q : Fin k → Polynomial ℤ) (hQ : ∀ (j : Fin k), Irreducible (Polynomial.map (Int.castRingHom ℚ) (Q j))) (hcoprime : ∀ (i j : Fin k), i ≠ j → IsCoprime (Polynomial.map (Int.castRingHom ℚ) (Q i)) (Polynomial.map (Int.castRingHom ℚ) (Q j))) (hfixed : NoFixedPrimeDivisor (∏ j : Fin k, Q j)) : (ofIrreducible Q hQ hcoprime hfixed).badDiscriminant = irreducibleBadDiscriminant Q