The canonical different degree of a plane function field

This module combines the sharp finite different bound with the complementary bound above infinity. Keeping the actual polynomial discriminant as the intermediate budget makes its degree cancel between the two contributions. The result is the expected first-projection canonical bound

2 * degreeOf 0 f * degreeOf 1 f - 2 * degreeOf 0 f - 2 * degreeOf 1 f.

No algebraic closure of the constant field is assumed.

theorem BGS.CorvajaZannier.hasBidegreeAtMost_degreeOf {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : External.HasBidegreeAtMost f (MvPolynomial.degreeOf 0 f) (MvPolynomial.degreeOf 1 f)

Every bivariate polynomial has its tautological support-wise bidegree bound given by its two degreeOf values.

theorem BGS.CorvajaZannier.planeCurvePolynomialInSecondCoordinate_discr_natDegree_le_degreeOf {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : (planeCurvePolynomialInSecondCoordinate f).discr.natDegree ≤ (2 * MvPolynomial.degreeOf 1 f - 2) * MvPolynomial.degreeOf 0 f

The second-coordinate equation's discriminant satisfies the sharp bidegree estimate at the curve's actual coordinate degrees.

theorem BGS.CorvajaZannier.planeCurve_finiteDifferentDegree_le_bidegreeDiscriminantBudget {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (hcardK : MvPolynomial.degreeOf 1 f < Fintype.card K) : have hx := ⋯; finiteExtensionFiniteDifferentDegree K (PlaneCurveFunctionField f) ⋯ ≤ (2 * MvPolynomial.degreeOf 1 f - 2) * MvPolynomial.degreeOf 0 f

The sharp finite-different estimate implies the usual bidegree-only finite discriminant budget. The canonical theorem below retains the sharper intermediate discriminant so that it cancels against the infinity complement.

theorem BGS.CorvajaZannier.planeCurve_canonicalDifferentDivisor_degree_le {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (hcardK : MvPolynomial.degreeOf 1 f < Fintype.card K) : have this := ⋯; have hx := ⋯; let this_1 := planeCurveFirstCoordinateRatFuncAlgebra f hx; have this_2 := ⋯; have this_3 := ⋯; finiteExtensionDivisorDegree K (PlaneCurveFunctionField f) (finiteExtensionCanonicalDifferentDivisor K (PlaneCurveFunctionField f) ⋯) ≤ 2 * ↑(MvPolynomial.degreeOf 0 f) * ↑(MvPolynomial.degreeOf 1 f) - 2 * ↑(MvPolynomial.degreeOf 0 f) - 2 * ↑(MvPolynomial.degreeOf 1 f)

The canonical different divisor of the first-coordinate plane function field has the sharp bidegree bound.