Binary homogenization of a product of linear factors

Mathlib's Polynomial.homogenize p n is the binary form Y ^ n p(X / Y) of degree n, with X the variable 0 and Y the variable 1. This file computes it on a product of linear factors: the homogenization of ∏ (X - a) is ∏ (X - a Y). Consequently, a polynomial with as many roots as its degree, p = c ∏ (X - a), has degree-(natDegree p) homogenization F(x, y) = c ∏ (x - a y) at every point (x, y), including the points with y = 0.

More generally, the homogenization of degree n ≥ natDegree p of such a p is c X₁ ^ (n - natDegree p) ∏ (X₀ - a X₁); since every binary form F of degree n is the homogenization of its dehomogenization F(X, 1), of degree at most n, this factors binary forms over an algebraically closed field into linear forms. If F has no squared linear factor, then X₁ occurs at most once and the roots of F(X, 1) are simple, so the linear factors are pairwise non-proportional. Conversely, the homogenization of degree natDegree p of a squarefree polynomial p has no squared linear factor.

This factorisation is the starting point of Liouville- and Roth-type lower bounds for binary forms at integer points.

The file also records the value of the homogenization of degree n at a point (a, b): the sum of the terms p_k a ^ k b ^ (n - k), which is p(a / b) b ^ n when b ≠ 0 and natDegree p ≤ n. Substituting linear polynomials a X + b and c X + d for the two variables, this is the action p ↦ (c X + d) ^ n p((a X + b) / (c X + d)) of a Möbius transformation on polynomials of degree at most n.

Homogenization also turns integral normalization into a change of variables. If p has degree d ≥ 1 and leading coefficient a, and F and G are the homogenizations of p and of the monic polynomial p.integralNormalization, then G(a x, y) = a ^ (d - 1) F(x, y). Over a domain, (x, y) ↦ (a x, y) therefore matches the solutions of the Thue equation F(x, y) = m with the solutions (x', y) of G(x', y) = a ^ (d - 1) m with a ∣ x'. This reduces Thue equations to the monic case: for p ∈ ℤ[X] the roots of the monic G(X, 1) are algebraic integers, namely the roots of F(X, 1) multiplied by a.

Main results

• Polynomial.homogenize_multiset_prod_X_sub_C: homogenize (∏ (X - a)) (card s) = ∏ (X - a Y).
• Polynomial.eval_homogenize_natDegree_of_card_roots: if p has natDegree p roots, then F(x) = leadingCoeff p * ∏_{a ∈ roots p} (x 0 - a x 1).
• Polynomial.sub_mul_dvd_eval_homogenize: for any root a of p and n ≥ natDegree p, the linear form x 0 - a x 1 divides the value at x of the homogenization of degree n.
• Polynomial.homogenize_eq_C_mul_X_pow_mul_prod: if p has natDegree p roots and natDegree p ≤ n, then its homogenization of degree n is leadingCoeff p * X₁ ^ (n - natDegree p) * ∏ (X₀ - a X₁).
• Polynomial.sub_natDegree_le_one_of_not_sq_dvd_homogenize, Polynomial.nodup_roots_of_not_sq_dvd_homogenize: if neither X₁ ^ 2 nor any (X₀ - a X₁) ^ 2 divides the homogenization of degree n (with n ≥ natDegree p for the second), then n ≤ natDegree p + 1 and the roots of p are simple.
• Squarefree.not_sq_dvd_homogenize_natDegree: conversely, the homogenization of degree natDegree p of a squarefree polynomial p has no squared linear factor.
• Polynomial.eval_homogenize_integralNormalization: G(a x, y) = a ^ (d - 1) F(x, y) for the homogenizations F of p and G of p.integralNormalization.
• Polynomial.bijOn_eval_homogenize_integralNormalization: over a domain, (x, y) ↦ (a x, y) is a bijection from the solutions of F(x, y) = m onto those of G(x', y) = a ^ (d - 1) m with a ∣ x'.
• Polynomial.aeval_homogenize_eq_sum, Polynomial.aeval_homogenize: the value of the homogenization of degree n at (a, b), as a sum of terms and, for b ≠ 0 in a semifield algebra and natDegree p ≤ n, as p(a / b) b ^ n.
• Polynomial.aeval_homogenize_of_eq_zero, Polynomial.aeval_homogenize_reflect: the value at (a, 0) is p_n a ^ n, and reflecting p at n exchanges the two coordinates.
• Polynomial.eval_homogenize_geom_sum: the homogenization of degree m (p - 1) of the geometric sum ∑_{i < p} (X ^ m) ^ i takes the value ∑_{i < p} (a ^ m) ^ i (b ^ m) ^ (p - 1 - i).
• MvPolynomial.aeval_X_one_map: the dehomogenization F(X, 1) commutes with mapping the coefficients along a ring homomorphism.
• MvPolynomial.IsHomogeneous.exists_linear_factors: a binary form of degree d with no squared linear factor, whose dehomogenization splits, is a ∏_{ℓ ∈ T} (ℓ.1 X₀ + ℓ.2 X₁) for d pairwise non-proportional linear forms.
• MvPolynomial.IsHomogeneous.mem_span_X_one_pow_of_aeval_eq_smul: over a domain, a binary form of degree d that is semi-invariant under the universal substitution x ↦ x - t y is a multiple of X₁ ^ d.

References

• [J.-H. Evertse, Diophantine Approximation, lecture notes, Leiden/Mastermath, 2019], Chapter 5, proof of Theorem 5.13, p. 97 (the reduction of Thue equations to the monic case).

theorem Polynomial.homogenize_multiset_prod_X_sub_C {R : Type u_1} [CommRing R] (s : Multiset R) : (Multiset.map (fun (a : R) => X - C a) s).prod.homogenize s.card = (Multiset.map (fun (a : R) => MvPolynomial.X 0 - MvPolynomial.C a * MvPolynomial.X 1) s).prod

The homogenization of ∏_{a ∈ s} (X - a) in degree card s is the product of the linear binary forms X₀ - a X₁.

theorem Polynomial.homogenize_eq_X_pow_mul_homogenize_natDegree {R : Type u_1} [CommRing R] {p : Polynomial R} {n : ℕ} (hn : p.natDegree ≤ n) : p.homogenize n = MvPolynomial.X 1 ^ (n - p.natDegree) * p.homogenize p.natDegree

The homogenization of p of degree n ≥ natDegree p is X₁ ^ (n - natDegree p) times its homogenization of degree natDegree p.

theorem Polynomial.homogenize_eq_C_mul_X_pow_mul_prod {R : Type u_1} [CommRing R] [IsDomain R] {p : Polynomial R} {n : ℕ} (hn : p.natDegree ≤ n) (hroots : p.roots.card = p.natDegree) : p.homogenize n = MvPolynomial.C p.leadingCoeff * MvPolynomial.X 1 ^ (n - p.natDegree) * (Multiset.map (fun (a : R) => MvPolynomial.X 0 - MvPolynomial.C a * MvPolynomial.X 1) p.roots).prod

If p has as many roots as its degree, its homogenization of degree n ≥ natDegree p is the binary form leadingCoeff p * X₁ ^ (n - natDegree p) * ∏_{a ∈ roots p} (X₀ - a X₁).

theorem Polynomial.eval_homogenize_natDegree_of_card_roots {R : Type u_1} [CommRing R] [IsDomain R] {p : Polynomial R} (hroots : p.roots.card = p.natDegree) (x : Fin 2 → R) : (MvPolynomial.eval x) (p.homogenize p.natDegree) = p.leadingCoeff * (Multiset.map (fun (a : R) => x 0 - a * x 1) p.roots).prod

If p has as many roots as its degree, its homogenization F of degree natDegree p factors at every point as F(x) = leadingCoeff p * ∏_{a ∈ roots p} (x 0 - a x 1).

theorem Polynomial.sub_mul_dvd_eval_homogenize {R : Type u_1} [CommRing R] {p : Polynomial R} {a : R} (ha : p.IsRoot a) {n : ℕ} (hn : p.natDegree ≤ n) (x : Fin 2 → R) : x 0 - a * x 1 ∣ (MvPolynomial.eval x) (p.homogenize n)

If a is a root of p and natDegree p ≤ n, then at every point x the value of the linear form x 0 - a x 1 divides the value of the homogenization of p of degree n. No splitting of p is needed, and R is an arbitrary commutative ring.

theorem Polynomial.sub_natDegree_le_one_of_not_sq_dvd_homogenize {R : Type u_1} [CommRing R] {p : Polynomial R} {n : ℕ} (h : ¬MvPolynomial.X 1 ^ 2 ∣ p.homogenize n) : n - p.natDegree ≤ 1

If X₁ ^ 2 does not divide the homogenization of p of degree n, then n ≤ natDegree p + 1, stated as n - natDegree p ≤ 1.

theorem Polynomial.nodup_roots_of_not_sq_dvd_homogenize {R : Type u_1} [CommRing R] [IsDomain R] {p : Polynomial R} {n : ℕ} (hn : p.natDegree ≤ n) (h : ∀ (a : R), ¬(MvPolynomial.X 0 - MvPolynomial.C a * MvPolynomial.X 1) ^ 2 ∣ p.homogenize n) : p.roots.Nodup

If no square (X₀ - a X₁) ^ 2 divides the homogenization of p of degree n ≥ natDegree p, then the roots of p are simple.

theorem Squarefree.not_sq_dvd_homogenize_natDegree {R : Type u_1} [CommRing R] [IsDomain R] {p : Polynomial R} (hp : Squarefree p) {a b : R} : ¬(MvPolynomial.C a * MvPolynomial.X 0 + MvPolynomial.C b * MvPolynomial.X 1) ^ 2 ∣ p.homogenize p.natDegree

The homogenization of degree natDegree p of a squarefree polynomial p over a domain has no squared linear factor (a X₀ + b X₁) ^ 2.

theorem Polynomial.eval_homogenize_integralNormalization {S : Type u_2} [CommSemiring S] {p : Polynomial S} (hp : 1 ≤ p.natDegree) (n : ℕ) (x y : S) : (MvPolynomial.eval ![p.leadingCoeff * x, y]) (p.integralNormalization.homogenize n) = p.leadingCoeff ^ (p.natDegree - 1) * (MvPolynomial.eval ![x, y]) (p.homogenize n)

Homogenized integral normalization. Let p have degree d ≥ 1 and leading coefficient a, and let F and G be the homogenizations of degree n of p and of the monic polynomial p.integralNormalization = a ^ (d - 1) p(X / a). Then G(a x, y) = a ^ (d - 1) F(x, y) for all x, y. This is the binary-form version of Polynomial.integralNormalization_eval₂_leadingCoeff_mul; it holds for every n, also below the degree.

theorem Polynomial.bijOn_eval_homogenize_integralNormalization {S : Type u_2} [CommSemiring S] [IsDomain S] {p : Polynomial S} (hp : 1 ≤ p.natDegree) (n : ℕ) (m : S) : Set.BijOn (fun (v : S × S) => (p.leadingCoeff * v.1, v.2)) {v : S × S | (MvPolynomial.eval ![v.1, v.2]) (p.homogenize n) = m} {v : S × S | (MvPolynomial.eval ![v.1, v.2]) (p.integralNormalization.homogenize n) = p.leadingCoeff ^ (p.natDegree - 1) * m ∧ p.leadingCoeff ∣ v.1}

Thue equations and integral normalization (Evertse, proof of Theorem 5.13). Over a domain, let p have degree d ≥ 1 and leading coefficient a, and let F and G be the homogenizations of degree n of p and of p.integralNormalization. Then (x, y) ↦ (a x, y) is a bijection from the solutions of F(x, y) = m onto the solutions (x', y) of G(x', y) = a ^ (d - 1) m with a ∣ x'.

theorem Polynomial.aeval_homogenize_eq_sum {S : Type u_2} [CommSemiring S] {A : Type u_3} [CommSemiring A] [Algebra S A] (p : Polynomial S) (n : ℕ) (a b : A) : (MvPolynomial.aeval ![a, b]) (p.homogenize n) = ∑ kl ∈ Finset.antidiagonal n, (algebraMap S A) (p.coeff kl.1) * (a ^ kl.1 * b ^ kl.2)

The value of the homogenization of degree n of p at (a, b) is the sum of the terms p_k a ^ k b ^ l over k + l = n.

theorem Polynomial.aeval_homogenize {S : Type u_2} [CommSemiring S] {K : Type u_3} [Semifield K] [Algebra S K] {p : Polynomial S} {n : ℕ} (hn : p.natDegree ≤ n) (x : Fin 2 → K) (hx : x 1 ≠ 0) : (MvPolynomial.aeval x) (p.homogenize n) = (aeval (x 0 / x 1)) p * x 1 ^ n

For natDegree p ≤ n and x 1 ≠ 0, the homogenization of degree n of p takes the value p(x 0 / x 1) x 1 ^ n at x, in any semifield that is an algebra over the coefficients. This is Polynomial.eval_homogenize with the coefficients mapped into the semifield.

theorem Polynomial.aeval_homogenize_of_eq_zero {S : Type u_2} [CommSemiring S] {A : Type u_3} [CommSemiring A] [Algebra S A] (p : Polynomial S) (n : ℕ) (x : Fin 2 → A) (hx : x 1 = 0) : (MvPolynomial.aeval x) (p.homogenize n) = (algebraMap S A) (p.coeff n) * x 0 ^ n

At a point whose second coordinate vanishes, the homogenization of degree n of p takes the value p_n (x 0) ^ n: only the monomial X₀ ^ n survives.

theorem Polynomial.aeval_homogenize_reflect {S : Type u_2} [CommSemiring S] {A : Type u_3} [CommSemiring A] [Algebra S A] (p : Polynomial S) (n : ℕ) (a b : A) : (MvPolynomial.aeval ![a, b]) ((reflect n p).homogenize n) = (MvPolynomial.aeval ![b, a]) (p.homogenize n)

Reflecting p at n exchanges the two variables of its homogenization of degree n: the homogenization of p.reflect n takes at (a, b) the value that the homogenization of p takes at (b, a).

theorem Polynomial.eval_homogenize_geom_sum {S : Type u_2} [CommSemiring S] (m p : ℕ) (a b : S) : (MvPolynomial.eval ![a, b]) ((∑ i ∈ Finset.range p, (X ^ m) ^ i).homogenize (m * (p - 1))) = ∑ i ∈ Finset.range p, (a ^ m) ^ i * (b ^ m) ^ (p - 1 - i)

The homogenization of the geometric sum ∑_{i < p} (X ^ m) ^ i at degree m (p - 1) takes the value ∑_{i < p} (a ^ m) ^ i (b ^ m) ^ (p - 1 - i) at (a, b).

theorem MvPolynomial.aeval_X_one_map {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (φ : R →+* S) (F : MvPolynomial (Fin 2) R) : (aeval ![Polynomial.X, 1]) ((map φ) F) = Polynomial.map φ ((aeval ![Polynomial.X, 1]) F)

The dehomogenization F(X, 1) of a binary form commutes with mapping the coefficients along a ring homomorphism φ.

theorem MvPolynomial.IsHomogeneous.exists_linear_factors {R : Type u_1} [CommRing R] [IsDomain R] {F : MvPolynomial (Fin 2) R} {d : ℕ} (hF : F.IsHomogeneous d) (hroots : ((MvPolynomial.aeval ![Polynomial.X, 1]) F).roots.card = ((MvPolynomial.aeval ![Polynomial.X, 1]) F).natDegree) (hsq : ∀ (a b : R), (a, b) ≠ (0, 0) → ¬(C a * X 0 + C b * X 1) ^ 2 ∣ F) : ∃ (a : R), a ≠ 0 ∧ ∃ (T : Finset (R × R)), T.card = d ∧ ((↑T).Pairwise fun (ℓ ℓ' : R × R) => ℓ.1 * ℓ'.2 - ℓ.2 * ℓ'.1 ≠ 0) ∧ (∀ ℓ ∈ T, ℓ = (0, 1) ∨ ∃ α ∈ ((MvPolynomial.aeval ![Polynomial.X, 1]) F).roots, ℓ = (1, -α)) ∧ F = C a * ∏ ℓ ∈ T, (C ℓ.1 * X 0 + C ℓ.2 * X 1)

Splitting of binary forms. Let F be a binary form of degree d over a domain, with no squared linear factor (so F ≠ 0), whose dehomogenization F(X, 1) has as many roots as its degree (for instance, over an algebraically closed field). Then F = a ∏_{ℓ ∈ T} (ℓ.1 X₀ + ℓ.2 X₁) with a ≠ 0 and d pairwise non-proportional linear forms, each either X₁ or X₀ - α X₁ with α a root of F(X, 1).

theorem MvPolynomial.IsHomogeneous.mem_span_X_one_pow_of_aeval_eq_smul {R : Type u_1} [CommRing R] [IsDomain R] {f : MvPolynomial (Fin 2) R} {d : ℕ} (hf : f.IsHomogeneous d) (c : Polynomial R) (h : (MvPolynomial.aeval ![X 0 - C Polynomial.X * X 1, X 1]) f = c • (map (algebraMap R (Polynomial R))) f) : f ∈ R ∙ X 1 ^ d

Binary forms semi-invariant under x ↦ x - t y are multiples of yᵈ. Over a domain, if a binary form f of degree d satisfies f(x - t y, y) = c f(x, y) in R[t][x, y] for some c ∈ R[t], then f is a multiple of X₁ ^ d.