Gauss descent for the Corvaja--Zannier bivariate resultant

When the resultant in the first variable vanishes, Corvaja and Zannier first obtain divisibility over the rational-function coefficient field and then use Gauss' lemma to descend that divisibility to the bivariate polynomial ring. This descent is what permits reading off both coordinate degrees, rather than only the degree in the eliminated variable.

theorem BGS.CorvajaZannier.transposeBivariate_eq_bivariateSwap {C : Type u_1} [Field C] : transposeBivariate = Polynomial.Bivariate.swap.toRingEquiv.toRingHom

The project-local transpose is the standard bivariate variable swap.

@[simp]

theorem BGS.CorvajaZannier.transposeBivariate_transposeBivariate {C : Type u_1} [Field C] (P : Polynomial (Polynomial C)) : transposeBivariate (transposeBivariate P) = P

Swapping the two variables twice is the identity.

theorem BGS.CorvajaZannier.transposeBivariate_injective {C : Type u_1} [Field C] : Function.Injective ⇑transposeBivariate

Swapping the variables is injective.

theorem BGS.CorvajaZannier.resultant_auxiliaryRelation_default_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)) = 0

The ordinary (actual-degree) resultant vanishes in the common-zero branch once its degree is smaller than the minimal-polynomial degree of v.

Using the ordinary resultant here is essential: a Sylvester determinant padded to an upper degree bound can vanish for the purely formal reason that one polynomial has smaller actual degree, and therefore cannot support the subsequent Gauss descent.

theorem BGS.CorvajaZannier.dvd_of_irreducible_of_resultant_eq_zero_via_gauss {C : Type u_1} [Field C] {f g : Polynomial (Polynomial C)} (hf : Irreducible f) (hfNonconstant : f.natDegree ≠ 0) (hresultant : f.resultant g = 0) : f ∣ g

Source-faithful Gauss descent: zero resultant gives divisibility already in C[V][U], not merely after passing to C(V)[U].

The nonconstant hypothesis is exactly what makes the irreducible polynomial primitive over C[V]; Gauss' lemma then descends the divisibility obtained over Frac(C[V]).

theorem BGS.CorvajaZannier.bidegree_le_of_irreducible_of_resultant_eq_zero {C : Type u_1} [Field C] {f g : Polynomial (Polynomial C)} (hf : Irreducible f) (hfNonconstant : f.natDegree ≠ 0) (hg : g ≠ 0) (hresultant : f.resultant g = 0) : f.natDegree ≤ g.natDegree ∧ (transposeBivariate f).natDegree ≤ (transposeBivariate g).natDegree

Gauss descent followed by variable swapping bounds both bidegrees of a nonzero multiple.

theorem BGS.CorvajaZannier.auxiliaryRelation_bidegree_bounds_of_resultant_eq_zero {C : Type u_1} [Field C] (f : Polynomial (Polynomial C)) (a b h k : ℕ) (ha : 0 < a) (hh : 0 < h) (hk : 0 < k) (c : Fin k → C) (d : Fin (k + 1) × Fin h → C) (hf : Irreducible f) (hfDegreeU : f.natDegree = a) (hfDegreeV : (transposeBivariate f).natDegree = b) (hauxNonzero : auxiliaryRelationPolynomial c d ≠ 0) (hresultant : f.resultant (transposeBivariate (auxiliaryRelationPolynomial c d)) = 0) : a ≤ k ∧ b ≤ h

The exact degree conclusion in the zero-resultant branch of the Corvaja--Zannier auxiliary-family argument.

Here f is oriented as a polynomial in U with coefficients in C[V]. Thus f.natDegree = a, while the degree of its variable swap is b. The auxiliary relation is constructed in the source orientation and swapped for the resultant.

theorem BGS.CorvajaZannier.auxiliaryFamily_linearIndependent_of_irreducible_bidegree {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) (hf : Irreducible f) (hfDegreeU : f.natDegree = a) (hfDegreeV : (transposeBivariate f).natDegree = b) (hfCoeffDegree : ∀ (i : ℕ), (f.coeff i).natDegree ≤ b) (u v : L) (hv : v ≠ 1) (hminpoly : (minpoly C v).natDegree = q) (hfZero : evalBivariate v u f = 0) (hsize : a * h + b * k < q) (hdegreeAlternativeExcluded : ¬(a ≤ k ∧ b ≤ h)) : LinearIndependent C (auxiliaryFamily u v h k)

Corvaja--Zannier Proposition 1, through its complete algebraic resultant branch. If the defining relation has bidegree (a,b), its ordinary resultant with any nonzero auxiliary relation would force a ≤ k and b ≤ h. Excluding that degree alternative therefore makes the exact auxiliary family linearly independent.

The assumptions expose the two genuinely external inputs to this algebraic step: iterated-polynomial irreducibility of the defining equation and the minimal-polynomial degree q of v over the coefficient field.