Powered coordinate heights in the first-coordinate place model

The canonical place summation uses the first-coordinate RatFunc model. This module records the exact first-coordinate height and the transported upper bound for the second-coordinate height, including positive powers.

theorem BGS.CorvajaZannier.finiteExtensionPositiveDegree_planeCurveFirstCoordinate_pow {K : Type u_1} [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ℕ) (_hm : 0 < m) : have hx := ⋯; finiteExtensionPositiveDegree K (PlaneCurveFunctionField f) (planeCurveFunction f 0 ^ m) = m * MvPolynomial.degreeOf 1 f

In the first-coordinate place model, x^m has its expected exact positive divisor degree.

theorem BGS.CorvajaZannier.finiteExtensionPositiveDegree_planeCurveSecondCoordinate_pow_le {K : Type u_1} [Field K] [Finite K] [DecidableEq K] [DecidableEq (RatFunc K)] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (n : ℕ) : have hx := ⋯; finiteExtensionPositiveDegree K (PlaneCurveFunctionField f) (planeCurveFunction f 1 ^ n) ≤ n * MvPolynomial.degreeOf 0 f

In the same first-coordinate place model, the transported second coordinate power has height at most n * degreeOf 0 f.

theorem BGS.CorvajaZannier.finiteExtensionGcdWeightedDegree_one_sub_planeCurvePowers_le {K : Type u_1} [Field K] [Finite K] [DecidableEq K] [DecidableEq (RatFunc K)] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) : have hx := ⋯; finiteExtensionGcdWeightedDegree K (PlaneCurveFunctionField f) (1 - planeCurveFunction f 0 ^ m) (1 - planeCurveFunction f 1 ^ n) ≤ n * MvPolynomial.degreeOf 0 f

The exhaustive gcd of 1-u and 1-v is bounded by the powered height of v, and hence by its displayed plane-curve degree budget.

theorem BGS.CorvajaZannier.finiteExtensionGcdWeightedDegree_comm {K : Type u_1} [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] {L : Type u_2} [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x y : L) : finiteExtensionGcdWeightedDegree K L x y = finiteExtensionGcdWeightedDegree K L y x

The exhaustive gcd degree is symmetric in its two arguments.

theorem BGS.CorvajaZannier.finiteExtensionGcdWeightedDegree_neg_neg {K : Type u_1} [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] {L : Type u_2} [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x y : L) (hx : x ≠ 0) (hy : y ≠ 0) : finiteExtensionGcdWeightedDegree K L (-x) (-y) = finiteExtensionGcdWeightedDegree K L x y

Simultaneously changing the signs of the two functions does not change their exhaustive gcd divisor degree.

theorem BGS.CorvajaZannier.planeCurveExhaustiveTorsionGcdWeightedDegree_eq_one_sub {K : Type u_1} [Field K] [DecidableEq K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) : have hx := ⋯; planeCurveExhaustiveTorsionGcdWeightedDegree hf hpartialSecond m n = finiteExtensionGcdWeightedDegree K (PlaneCurveFunctionField f) (1 - planeCurveFunction f 0 ^ m) (1 - planeCurveFunction f 1 ^ n)

The torsion gcd used by the endpoint is exactly the 1-u, 1-v gcd used by the canonical Wronskian estimate.

theorem BGS.CorvajaZannier.finiteExtensionGcdWeightedDegree_one_sub_planeCurvePowers_swapped_le {K : Type u_1} [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) : have hx := ⋯; finiteExtensionGcdWeightedDegree K (PlaneCurveFunctionField f) (1 - planeCurveFunction f 1 ^ n) (1 - planeCurveFunction f 0 ^ m) ≤ m * MvPolynomial.degreeOf 1 f

With the coordinates swapped, the one-minus gcd is bounded by the exact powered height of the first coordinate.