Square-free divisors of integer binary forms

Let F ∈ ℤ[X₀, X₁] be a binary form and let L be an algebraically closed field of characteristic zero. If F(X, 1) has r distinct zeros in L, then F has a divisor G ∈ ℤ[X₀, X₁] which is a binary form of degree r without squared linear factors over L: the homogenization of the radical of F(X, 1) in ℤ[X].

Results on binary forms without squared linear factors, such as the Thue–Roth inequality MvPolynomial.IsHomogeneous.exists_pos_mul_max_abs_rpow_le_abs_eval, thus apply to a divisor of an arbitrary integer binary form. If F(X, 1) has at least three distinct complex zeros, the divisor has degree at least 3; since G(x, y) divides F(x, y), solutions of the Thue equation F(x, y) = m ≠ 0 are solutions of G(x, y) = m' for one of the finitely many divisors m' of m.

Main results

• Polynomial.roots_toFinset_map_radical, Polynomial.separable_map_radical: the radical of a polynomial has the same zeros as the polynomial, and is separable over a perfect fraction field.
• MvPolynomial.IsHomogeneous.exists_dvd_isHomogeneous_not_sq_dvd: an integer binary form has a divisor which is a binary form without squared linear factors over L, of degree the number of distinct zeros of F(X, 1) in L.

References

• J.-H. Evertse, Diophantine Approximation, lecture notes (2019), ch. 6, Corollary 6.4.

theorem Polynomial.roots_toFinset_map_radical {R : Type u_1} {S : Type u_2} [CommRing R] [IsDomain R] [NormalizationMonoid R] [UniqueFactorizationMonoid R] [CommRing S] [IsDomain S] [DecidableEq S] {φ : R →+* S} (hφ : Function.Injective ⇑φ) (f : Polynomial R) : (map φ (UniqueFactorizationMonoid.radical f)).roots.toFinset = (map φ f).roots.toFinset

After an injective map to a domain, the radical of a polynomial over a unique factorization domain has the same zeros as the polynomial itself, since radical f ∣ f ∣ radical f ^ n.

theorem Polynomial.separable_map_radical {R : Type u_1} (K : Type u_2) (L : Type u_3) [CommRing R] [IsDomain R] [NormalizedGCDMonoid R] [UniqueFactorizationMonoid R] [Field K] [Algebra R K] [IsFractionRing R K] [PerfectField K] [Field L] [Algebra R L] [Algebra K L] [IsScalarTower R K L] (f : Polynomial R) : (map (algebraMap R L) (UniqueFactorizationMonoid.radical f)).Separable

The radical of a polynomial over a unique factorization domain R whose fraction field K is perfect is separable over every field extension of K.

theorem MvPolynomial.IsHomogeneous.exists_dvd_isHomogeneous_not_sq_dvd {F : MvPolynomial (Fin 2) ℤ} {d : ℕ} (hF : F.IsHomogeneous d) (L : Type u_1) [Field L] [CharZero L] [IsAlgClosed L] [DecidableEq L] : ∃ (G : MvPolynomial (Fin 2) ℤ), G ∣ F ∧ G.IsHomogeneous (Polynomial.map (Int.castRingHom L) ((MvPolynomial.aeval ![Polynomial.X, 1]) F)).roots.toFinset.card ∧ ∀ (a b : L), (a, b) ≠ (0, 0) → ¬(C a * X 0 + C b * X 1) ^ 2 ∣ (map (Int.castRingHom L)) G

Square-free divisors of integer binary forms (Evertse, proof of Corollary 6.4). Let F ∈ ℤ[X₀, X₁] be a binary form and L an algebraically closed field of characteristic zero. Then F is divisible by a binary form G ∈ ℤ[X₀, X₁] whose degree is the number of distinct zeros of F(X, 1) in L, and which has no squared linear factor (a X₀ + b X₁) ^ 2 over L.