A sharp degree bound for a bivariate discriminant

For a polynomial F in one variable whose coefficients are polynomials of degree at most a, this file proves that the discriminant of F has degree at most (2 * F.natDegree - 2) * a in the coefficient variable. The missing two copies of a relative to the naive Sylvester-determinant estimate come from the constant bottom row in Mathlib's modified Sylvester matrix for the derivative.

This is the algebraic degree estimate needed in the Corvaja--Zannier canonical/divisor calculation.

theorem BGS.CorvajaZannier.natDegree_sylvesterDeriv_apply_le_of_row_ne {K : Type u_1} [Field K] (F : Polynomial (Polynomial K)) (a : ℕ) (hcoeff : ∀ (i : ℕ), (F.coeff i).natDegree ≤ a) (i j : Fin (F.natDegree - 1 + F.natDegree)) (hi : ↑i ≠ 2 * F.natDegree - 2) : (F.sylvesterDeriv i j).natDegree ≤ a

theorem BGS.CorvajaZannier.natDegree_sylvesterDeriv_apply_bottom {K : Type u_1} [Field K] (F : Polynomial (Polynomial K)) (hF : 0 < F.natDegree) (j : Fin (F.natDegree - 1 + F.natDegree)) : (F.sylvesterDeriv ⟨2 * F.natDegree - 2, ⋯⟩ j).natDegree = 0

theorem BGS.CorvajaZannier.natDegree_discr_le {K : Type u_1} [Field K] (F : Polynomial (Polynomial K)) (a : ℕ) (hcoeff : ∀ (i : ℕ), (F.coeff i).natDegree ≤ a) : F.discr.natDegree ≤ (2 * F.natDegree - 2) * a

The discriminant of a degree-b polynomial whose coefficients have degree at most a has degree at most (2 * b - 2) * a.

noncomputable def BGS.CorvajaZannier.planeCurvePolynomialInSecondCoordinate {K : Type u_1} [Field K] : MvPolynomial (Fin 2) K ≃ₐ[K] Polynomial (Polynomial K)

View a bivariate polynomial as a polynomial in coordinate 1, with ordinary polynomial coefficients in coordinate 0.

Equations

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

theorem BGS.CorvajaZannier.natDegree_uniqueAlgEquiv_le_degreeOf {K : Type u_1} [Field K] {σ : Type u_2} [Unique σ] (P : MvPolynomial σ K) : ((MvPolynomial.uniqueAlgEquiv K σ) P).natDegree ≤ MvPolynomial.degreeOf default P

@[simp]

theorem BGS.CorvajaZannier.planeCurvePolynomialInSecondCoordinate_natDegree {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : (planeCurvePolynomialInSecondCoordinate f).natDegree = MvPolynomial.degreeOf 1 f

theorem BGS.CorvajaZannier.planeCurvePolynomialInSecondCoordinate_coeff_natDegree_le_degreeOf_first {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) (i : ℕ) : ((planeCurvePolynomialInSecondCoordinate f).coeff i).natDegree ≤ MvPolynomial.degreeOf 0 f

theorem BGS.CorvajaZannier.planeCurvePolynomialInSecondCoordinate_coeff_natDegree_le {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} {firstDegree secondDegree : ℕ} (hdegree : External.HasBidegreeAtMost f firstDegree secondDegree) (i : ℕ) : ((planeCurvePolynomialInSecondCoordinate f).coeff i).natDegree ≤ firstDegree

theorem BGS.CorvajaZannier.planeCurvePolynomialInSecondCoordinate_discr_natDegree_le {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} {firstDegree secondDegree : ℕ} (hdegree : External.HasBidegreeAtMost f firstDegree secondDegree) : (planeCurvePolynomialInSecondCoordinate f).discr.natDegree ≤ (2 * secondDegree - 2) * firstDegree

The discriminant in the first coordinate of a plane curve of bidegree at most (firstDegree, secondDegree) has the sharp degree bound (2 * secondDegree - 2) * firstDegree.