Degree bounds for bivariate resultants

Corvaja--Zannier eliminate the first variable from a defining polynomial f(U,V) and an auxiliary relation P(U,V). They use the Sylvester determinant estimate

deg_V Res_U(f, P) ≤ deg_U(f) * deg_V(P) + deg_U(P) * deg_V(f).

Here bivariate polynomials are represented as polynomials in U whose coefficients lie in C[V]. The proof records the sharper columnwise degree bound for determinants: each determinant term uses exactly one entry from every Sylvester column, so the coefficient bounds add with the correct multiplicities.

noncomputable def BGS.CorvajaZannier.transposeBivariate {C : Type u_1} [Field C] : Polynomial (Polynomial C) →+* Polynomial (Polynomial C)

Exchange the two variables of an iterated bivariate polynomial. Both the source and target have Lean type C[U][V]; the target is interpreted as C[V][U].

Equations

• BGS.CorvajaZannier.transposeBivariate = Polynomial.eval₂RingHom (Polynomial.mapRingHom Polynomial.C) (Polynomial.C Polynomial.X)

@[simp]

theorem BGS.CorvajaZannier.transposeBivariate_C {C : Type u_1} [Field C] (p : Polynomial C) : transposeBivariate (Polynomial.C p) = Polynomial.map Polynomial.C p

@[simp]

theorem BGS.CorvajaZannier.transposeBivariate_X {C : Type u_1} [Field C] : transposeBivariate Polynomial.X = Polynomial.C Polynomial.X

@[simp]

theorem BGS.CorvajaZannier.evalBivariate_map_C {C : Type u_1} [Field C] {L : Type u_2} [Field L] [Algebra C L] (u v : L) (p : Polynomial C) : evalBivariate v u (Polynomial.map Polynomial.C p) = Polynomial.eval₂ (algebraMap C L) u p

@[simp]

theorem BGS.CorvajaZannier.evalBivariate_C_X_pow {C : Type u_1} [Field C] {L : Type u_2} [Field L] [Algebra C L] (u v : L) (n : ℕ) : evalBivariate v u (Polynomial.C Polynomial.X ^ n) = v ^ n

theorem BGS.CorvajaZannier.evalBivariate_transposeBivariate {C : Type u_1} [Field C] {L : Type u_2} [Field L] [Algebra C L] (u v : L) (P : Polynomial (Polynomial C)) : evalBivariate v u (transposeBivariate P) = evalBivariate u v P

Swapping variables and then evaluating at the swapped point preserves the value of a bivariate polynomial.

theorem BGS.CorvajaZannier.transposeBivariate_natDegree_le {C : Type u_1} [Field C] (P : Polynomial (Polynomial C)) (k : ℕ) (hcoeff : ∀ (s : ℕ), (P.coeff s).natDegree ≤ k) : (transposeBivariate P).natDegree ≤ k

A coefficientwise degree bound becomes an outer degree bound after transposing the variables.

theorem BGS.CorvajaZannier.transposeBivariate_coeff_natDegree_le {C : Type u_1} [Field C] (P : Polynomial (Polynomial C)) (h : ℕ) (hdegree : P.natDegree ≤ h) (r : ℕ) : ((transposeBivariate P).coeff r).natDegree ≤ h

An outer degree bound becomes a coefficientwise degree bound after transposing the variables.

theorem BGS.CorvajaZannier.auxiliaryRelationPolynomial_natDegree_le {C : Type u_1} [Field C] {h k : ℕ} (hh : 0 < h) (c : Fin k → C) (d : Fin (k + 1) × Fin h → C) : (auxiliaryRelationPolynomial c d).natDegree ≤ h

The source-oriented auxiliary relation has degree at most h in its outer variable V.

theorem BGS.CorvajaZannier.auxiliaryRelationPolynomial_coeff_natDegree_le {C : Type u_1} [Field C] {h k : ℕ} (hk : 0 < k) (c : Fin k → C) (d : Fin (k + 1) × Fin h → C) (s : ℕ) : ((auxiliaryRelationPolynomial c d).coeff s).natDegree ≤ k

Every V-coefficient of the source-oriented auxiliary relation has U-degree at most k.

theorem BGS.CorvajaZannier.transpose_auxiliaryRelationPolynomial_natDegree_le {C : Type u_1} [Field C] {h k : ℕ} (hk : 0 < k) (c : Fin k → C) (d : Fin (k + 1) × Fin h → C) : (transposeBivariate (auxiliaryRelationPolynomial c d)).natDegree ≤ k

In the U-oriented representation required by Res_U, the auxiliary relation has U-degree at most k.

theorem BGS.CorvajaZannier.transpose_auxiliaryRelationPolynomial_coeff_natDegree_le {C : Type u_1} [Field C] {h k : ℕ} (hh : 0 < h) (c : Fin k → C) (d : Fin (k + 1) × Fin h → C) (r : ℕ) : ((transposeBivariate (auxiliaryRelationPolynomial c d)).coeff r).natDegree ≤ h

In the U-oriented representation required by Res_U, every coefficient has V-degree at most h.

theorem BGS.CorvajaZannier.Matrix.natDegree_det_le_sum_columnDegree {C : Type u_1} [Field C] {n : Type u_2} [Fintype n] [DecidableEq n] (M : Matrix n n (Polynomial C)) (columnDegree : n → ℕ) (hM : ∀ (i j : n), (M i j).natDegree ≤ columnDegree j) : M.det.natDegree ≤ ∑ j : n, columnDegree j

A determinant over C[V] has degree at most the sum of columnwise degree bounds.

theorem BGS.CorvajaZannier.natDegree_resultant_le {C : Type u_1} [Field C] (f g : Polynomial (Polynomial C)) (m n df dg : ℕ) (hf : ∀ (i : ℕ), (f.coeff i).natDegree ≤ df) (hg : ∀ (i : ℕ), (g.coeff i).natDegree ≤ dg) : (f.resultant g m n).natDegree ≤ m * dg + n * df

The exact coefficient-degree estimate for a resultant over C[V].

f has U-degree bounded by m and every V-coefficient degree bounded by df; g has the analogous bounds n and dg.

theorem BGS.CorvajaZannier.natDegree_resultant_le_of_degree_le {C : Type u_1} [Field C] (f g : Polynomial (Polynomial C)) (m n df dg : ℕ) (hfDegree : f.natDegree ≤ m) (hgDegree : g.natDegree ≤ n) (hf : ∀ (i : ℕ), (f.coeff i).natDegree ≤ df) (hg : ∀ (i : ℕ), (g.coeff i).natDegree ≤ dg) : (f.resultant g).natDegree ≤ m * dg + n * df

The source-faithful version using the ordinary resultant at the actual degrees, while bounding those degrees by m and n.

theorem BGS.CorvajaZannier.natDegree_resultant_auxiliaryRelation_le {C : Type u_1} [Field C] (f : Polynomial (Polynomial C)) (a b h k : ℕ) (hh : 0 < h) (c : Fin k → C) (d : Fin (k + 1) × Fin h → C) (hf : ∀ (i : ℕ), (f.coeff i).natDegree ≤ b) : (f.resultant (transposeBivariate (auxiliaryRelationPolynomial c d)) a k).natDegree ≤ a * h + k * b

The exact Corvaja--Zannier resultant degree bound for the transposed auxiliary relation.

theorem BGS.CorvajaZannier.natDegree_resultant_auxiliaryRelation_default_le {C : Type u_1} [Field C] (f : Polynomial (Polynomial C)) (a b h k : ℕ) (hh : 0 < h) (hk : 0 < k) (c : Fin k → C) (d : Fin (k + 1) × Fin h → C) (hfDegree : f.natDegree ≤ a) (hf : ∀ (i : ℕ), (f.coeff i).natDegree ≤ b) : (f.resultant (transposeBivariate (auxiliaryRelationPolynomial c d))).natDegree ≤ a * h + k * b

The ordinary-resultant degree bound for the transposed auxiliary relation. This is the version used by the subsequent irreducibility/divisibility argument.

theorem BGS.CorvajaZannier.resultant_eq_zero_of_common_root {K : Type u_2} [Field K] (f g : Polynomial K) (m n : ℕ) (hf : f.natDegree ≤ m) (hg : g.natDegree ≤ n) (hmn : m ≠ 0 ∨ n ≠ 0) (x : K) (hfx : Polynomial.eval x f = 0) (hgx : Polynomial.eval x g = 0) : f.resultant g m n = 0

Two polynomials of the prescribed degree bounds with a common root have zero explicit-degree resultant.

theorem BGS.CorvajaZannier.eval₂_resultant_eq_zero_of_common_zero {C : Type u_1} [Field C] {L : Type u_2} [Field L] [Algebra C L] (f g : Polynomial (Polynomial C)) (m n : ℕ) (hf : f.natDegree ≤ m) (hg : g.natDegree ≤ n) (hmn : m ≠ 0 ∨ n ≠ 0) (u v : L) (hfu : evalBivariate v u f = 0) (hgu : evalBivariate v u g = 0) : Polynomial.eval₂ (algebraMap C L) v (f.resultant g m n) = 0

If two bivariate polynomials vanish at (u,v), their resultant in U vanishes at v.

theorem BGS.CorvajaZannier.eval₂_resultant_auxiliaryRelation_eq_zero_of_common_zero {C : Type u_1} [Field C] {L : Type u_2} [Field L] [Algebra C L] (f : Polynomial (Polynomial C)) (a h k : ℕ) (ha : 0 < a) (hk : 0 < k) (c : Fin k → C) (d : Fin (k + 1) × Fin h → C) (hfDegree : f.natDegree ≤ a) (u v : L) (hfZero : evalBivariate v u f = 0) (hauxZero : evalBivariate u v (auxiliaryRelationPolynomial c d) = 0) : Polynomial.eval₂ (algebraMap C L) v (f.resultant (transposeBivariate (auxiliaryRelationPolynomial c d)) a k) = 0

The common-zero implication specialized to the Corvaja--Zannier auxiliary relation.

theorem BGS.CorvajaZannier.minpoly_natDegree_le_of_eval₂_eq_zero {C : Type u_1} [Field C] {L : Type u_2} [Field L] [Algebra C L] (y : L) (P : Polynomial C) (hP : P ≠ 0) (hzero : Polynomial.eval₂ (algebraMap C L) y P = 0) : (minpoly C y).natDegree ≤ P.natDegree

A nonzero polynomial vanishing at an algebraic element has degree at least the degree of that element's minimal polynomial.

theorem BGS.CorvajaZannier.eq_zero_of_natDegree_lt_minpoly_of_eval₂_eq_zero {C : Type u_1} [Field C] {L : Type u_2} [Field L] [Algebra C L] (y : L) (P : Polynomial C) (hdegree : P.natDegree < (minpoly C y).natDegree) (hzero : Polynomial.eval₂ (algebraMap C L) y P = 0) : P = 0

A polynomial whose degree is strictly smaller than the minimal-polynomial degree cannot vanish at the element unless it is zero.

theorem BGS.CorvajaZannier.resultant_auxiliaryRelation_eq_zero_of_common_zero {C : Type u_1} [Field C] {L : Type u_2} [Field L] [Algebra C L] (f : Polynomial (Polynomial C)) (a b h k q : ℕ) (ha : 0 < a) (hh : 0 < h) (hk : 0 < k) (c : Fin k → C) (d : Fin (k + 1) × Fin h → C) (hfDegree : f.natDegree ≤ a) (hfCoeffDegree : ∀ (i : ℕ), (f.coeff i).natDegree ≤ b) (u v : L) (hminpoly : (minpoly C v).natDegree = q) (hfZero : evalBivariate v u f = 0) (hauxZero : evalBivariate u v (auxiliaryRelationPolynomial c d) = 0) (hsize : a * h + k * b < q) : f.resultant (transposeBivariate (auxiliaryRelationPolynomial c d)) a k = 0

The complete nonzero-resultant contradiction in the Corvaja--Zannier auxiliary-family argument. Under a*h + k*b < q and minimal-polynomial degree q, the resultant must vanish identically.

theorem BGS.CorvajaZannier.irreducible_dvd_of_resultant_eq_zero {K : Type u_2} [Field K] {f g : Polynomial K} (hf : Irreducible f) (hresultant : f.resultant g = 0) : f ∣ g

Over a field, an irreducible polynomial divides any nonzero polynomial with which it has zero resultant.

theorem BGS.CorvajaZannier.map_dvd_of_resultant_eq_zero {R : Type u_2} {K : Type u_3} [CommRing R] [Field K] (f g : Polynomial R) (phi : R →+* K) (hphi : Function.Injective ⇑phi) (hf : Irreducible (Polynomial.map phi f)) (hresultant : f.resultant g = 0) : Polynomial.map phi f ∣ Polynomial.map phi g

The zero-resultant divisibility branch after embedding the coefficient ring into a field (in the application, C[V] → C(V)).

theorem BGS.CorvajaZannier.natDegree_le_of_map_irreducible_of_resultant_eq_zero {R : Type u_2} {K : Type u_3} [CommRing R] [Field K] (f g : Polynomial R) (phi : R →+* K) (hphi : Function.Injective ⇑phi) (hf : Irreducible (Polynomial.map phi f)) (hg : g ≠ 0) (hresultant : f.resultant g = 0) : f.natDegree ≤ g.natDegree

The zero-resultant branch already forces the defining polynomial's degree in the eliminated variable to be no larger than that of the auxiliary relation after any injective coefficient-field embedding.