The first plane coordinate only has poles above infinity

The first-coordinate rational-function model sends RatFunc.X to the first plane coordinate. At a finite place, Polynomial.X lies in the finite integral closure, so its order is nonnegative. Thus the effective pole divisor of the first coordinate vanishes at every finite place.

Combining this support statement with the previously constructed controlled pole place shows that the selected pole may be taken above the rational- function place at infinity, without changing its place-degree bound.

@[instance_reducible]

noncomputable def BGS.HasseWeil.coordinatePolePolynomialAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra (Polynomial K) L

The algebra structure from K[X] to L used in the plane coordinate pole at infinity construction.

Equations

• BGS.HasseWeil.coordinatePolePolynomialAlgebra K L = ((algebraMap (RatFunc K) L).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra

theorem BGS.HasseWeil.coordinatePolePolynomialScalarTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower (Polynomial K) (RatFunc K) L

theorem BGS.HasseWeil.coordinatePoleFiniteIntegralClosureModuleFinite (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.Finite (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

theorem BGS.HasseWeil.coordinatePoleFiniteIntegralClosureIsIntegral (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra.IsIntegral (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

theorem BGS.HasseWeil.coordinatePolePolynomialTorsionFreeTop (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree (Polynomial K) L

theorem BGS.HasseWeil.coordinatePoleFiniteIntegralClosureIsTorsionFree (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

theorem BGS.HasseWeil.coordinatePoleInfinityIntegralClosureModuleFinite (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.Finite ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

theorem BGS.HasseWeil.coordinatePoleInfinityIntegralClosureIsIntegral (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra.IsIntegral ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

theorem BGS.HasseWeil.coordinatePoleInfinityBaseTorsionFreeTop (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree (↥(CorvajaZannier.RatFuncInfinityIntegers K)) L

theorem BGS.HasseWeil.coordinatePoleInfinityIntegralClosureIsTorsionFree (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

theorem BGS.HasseWeil.coordinatePoleInfinityIntegralClosureIsDedekindDomain (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : IsDedekindDomain ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

theorem BGS.HasseWeil.coordinatePoleInfinityIntegralClosureIsFractionRing (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] : IsFractionRing (↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)) L

theorem BGS.HasseWeil.finiteExtensionPrincipalDivisor_algebraMap_X_inr_negative (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)) : (CorvajaZannier.finiteExtensionPrincipalDivisor K L ((algebraMap (RatFunc K) L) RatFunc.X)) (Sum.inr P) < 0

At every place above the rational-function place at infinity, the image of RatFunc.X has strictly negative order. This is stronger than merely knowing that some infinity place is a pole: it makes the pole divisor of the first coordinate cofinal among divisors supported at infinity.

theorem BGS.HasseWeil.finiteExtensionPrincipalDivisor_planeCurveFirstCoordinate_inl_nonnegative {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 := ⋯; ∀ (q : CorvajaZannier.FiniteExtensionFinitePlace K (CorvajaZannier.PlaneCurveFunctionField f)), 0 ≤ (CorvajaZannier.finiteExtensionPrincipalDivisor K (CorvajaZannier.PlaneCurveFunctionField f) (CorvajaZannier.planeCurveFunction f 0)) (Sum.inl q)

The first plane coordinate has nonnegative principal-divisor order at every finite place in its rational-function model.

theorem BGS.HasseWeil.finiteExtensionPoleDivisor_planeCurveFirstCoordinate_inl_eq_zero {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 := ⋯; ∀ (q : CorvajaZannier.FiniteExtensionFinitePlace K (CorvajaZannier.PlaneCurveFunctionField f)), (finiteExtensionPoleDivisor K (CorvajaZannier.PlaneCurveFunctionField f) (CorvajaZannier.planeCurveFunction f 0)) (Sum.inl q) = 0

Consequently, the pole divisor of the first plane coordinate vanishes at every finite place.

theorem BGS.HasseWeil.finiteExtensionPoleDivisor_planeCurveFirstCoordinate_inr_positive {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 := ⋯; ∀ (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K (CorvajaZannier.PlaneCurveFunctionField f))), 0 < (finiteExtensionPoleDivisor K (CorvajaZannier.PlaneCurveFunctionField f) (CorvajaZannier.planeCurveFunction f 0)) (Sum.inr P)

Every place above infinity occurs with positive coefficient in the pole divisor of the first plane coordinate.

theorem BGS.HasseWeil.exists_planeCurveFirstCoordinate_infinityPolePlace {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.FiniteExtensionInfinityPlace K (CorvajaZannier.PlaneCurveFunctionField f))), 0 < (finiteExtensionPoleDivisor K (CorvajaZannier.PlaneCurveFunctionField f) (CorvajaZannier.planeCurveFunction f 0)) (Sum.inr P) ∧ 0 < CorvajaZannier.finiteExtensionPlaceDegree K (CorvajaZannier.PlaneCurveFunctionField f) (Sum.inr P) ∧ CorvajaZannier.finiteExtensionPlaceDegree K (CorvajaZannier.PlaneCurveFunctionField f) (Sum.inr P) ≤ MvPolynomial.degreeOf 1 f

The controlled pole place for the first plane coordinate lies above the rational-function place at infinity. Its positive pole coefficient and place-degree bound are the same as in exists_planeCurveFirstCoordinate_polePlace.