A controlled pole place for the first plane coordinate

In the first-coordinate rational-function model of an irreducible plane curve, the pole divisor of the first coordinate has degree exactly the degree of the defining polynomial in the second variable. Consequently that pole divisor has nonempty support, and one can choose a pole place whose (possibly nontrivial) place degree is bounded by that second-variable degree.

No rationality assertion is made about the selected place.

theorem BGS.HasseWeil.finiteExtensionHeight_planeCurveFirstCoordinate {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) : have hx := ⋯; CorvajaZannier.finiteExtensionHeight K (CorvajaZannier.PlaneCurveFunctionField f) (CorvajaZannier.planeCurveFunction f 0) = MvPolynomial.degreeOf 1 f

In the first-coordinate RatFunc model, the pole height of the first coordinate is the degree of the plane equation in the second variable.

theorem BGS.HasseWeil.finiteExtensionDivisorDegree_planeCurveFirstCoordinate_poleDivisor {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) : have hx := ⋯; CorvajaZannier.finiteExtensionDivisorDegree K (CorvajaZannier.PlaneCurveFunctionField f) (finiteExtensionPoleDivisor K (CorvajaZannier.PlaneCurveFunctionField f) (CorvajaZannier.planeCurveFunction f 0)) = ↑(MvPolynomial.degreeOf 1 f)

Equivalently, the effective pole divisor of the first coordinate has degree equal to the degree of the plane equation in the second variable.

theorem BGS.HasseWeil.finiteExtensionPlaceDegree_le_divisorDegree_of_effective_of_pos {K : Type u_1} [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (D : CorvajaZannier.FiniteExtensionDivisor K L) (hD : ∀ (v : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ D v) {P : CorvajaZannier.FiniteExtensionPlace K L} (hP : 0 < D P) : ↑(CorvajaZannier.finiteExtensionPlaceDegree K L P) ≤ CorvajaZannier.finiteExtensionDivisorDegree K L D

A positive coefficient of an effective divisor contributes at least the degree of its place to the total divisor degree.

theorem BGS.HasseWeil.planeCurveFirstCoordinate_poleDivisor_support_nonempty {K : Type u_1} [Field K] [DecidableEq (RatFunc K)] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : have hx := ⋯; (finiteExtensionPoleDivisor K (CorvajaZannier.PlaneCurveFunctionField f) (CorvajaZannier.planeCurveFunction f 0)).support.Nonempty

The first-coordinate pole divisor has nonempty support.

theorem BGS.HasseWeil.exists_planeCurveFirstCoordinate_polePlace {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) : have hx := ⋯; ∃ (P : CorvajaZannier.FiniteExtensionPlace K (CorvajaZannier.PlaneCurveFunctionField f)), 0 < (finiteExtensionPoleDivisor K (CorvajaZannier.PlaneCurveFunctionField f) (CorvajaZannier.planeCurveFunction f 0)) P ∧ 0 < CorvajaZannier.finiteExtensionPlaceDegree K (CorvajaZannier.PlaneCurveFunctionField f) P ∧ CorvajaZannier.finiteExtensionPlaceDegree K (CorvajaZannier.PlaneCurveFunctionField f) P ≤ MvPolynomial.degreeOf 1 f

There is a pole place for the first coordinate. Its coefficient in the pole divisor is positive, and its (not necessarily one) place degree lies between one and the degree of the plane equation in the second variable.