One-point Riemann-space lower bounds for plane curves

For an absolutely irreducible affine plane equation f, choose an infinity place P where the first coordinate has a pole. The rectangular monomial grid

{x^i y^j | 0 ≤ i ≤ n, 0 ≤ j < degreeOf 1 f}

lies in the Riemann space of a controlled effective pole divisor. Removing all components away from P and comparing divisor degrees gives the coarse one-point estimate

m * degree(P) + 1 ≤ finrank L(m P) + (degreeOf 0 f - 1) * (degreeOf 1 f - 1)

along an explicit arithmetic progression of pole levels m. The final theorem combines this estimate with the one-place increment bound and the exact constant field to force at least m - g strict levels in the one-point Riemann filtration, where g is the displayed bidegree budget.

noncomputable def BGS.HasseWeil.planeMonomialPoleBudget (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] (x y : L) (n b : ℕ) : CorvajaZannier.FiniteExtensionDivisor K L

The effective pole divisor containing the rectangular monomial grid x^i y^j with i ≤ n and j < b.

Equations

• BGS.HasseWeil.planeMonomialPoleBudget K L x y n b = n • BGS.HasseWeil.finiteExtensionPoleDivisor K L x + (b - 1) • BGS.HasseWeil.finiteExtensionPoleDivisor K L y

noncomputable def BGS.HasseWeil.planeMonomialPoleLevel (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] (x y : L) (n b : ℕ) (P : CorvajaZannier.FiniteExtensionPlace K L) : ℕ

The coefficient of the monomial pole budget at a selected place.

Equations

• BGS.HasseWeil.planeMonomialPoleLevel K L x y n b P = ((BGS.HasseWeil.planeMonomialPoleBudget K L x y n b) P).toNat

theorem BGS.HasseWeil.planeMonomialPoleLevel_eq (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] (x y : L) (n b : ℕ) (P : CorvajaZannier.FiniteExtensionPlace K L) : planeMonomialPoleLevel K L x y n b P = n * ((finiteExtensionPoleDivisor K L x) P).toNat + (b - 1) * ((finiteExtensionPoleDivisor K L y) P).toNat

The selected pole level is an explicit arithmetic progression in n.

noncomputable def BGS.HasseWeil.planeCurveBidegreeGenusBudget {K : Type u_3} [CommSemiring K] (f : MvPolynomial (Fin 2) K) : ℕ

The coarse bidegree genus budget used by the monomial argument. It is an upper-bound budget and does not assert that the affine plane model is smooth.

Equations

• BGS.HasseWeil.planeCurveBidegreeGenusBudget f = (MvPolynomial.degreeOf 0 f - 1) * (MvPolynomial.degreeOf 1 f - 1)

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

theorem BGS.HasseWeil.planeCurveMonomialPoleBudget_finrank_lower {K : Type u_1} [Field K] [Fintype 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 := ⋯; (n + 1) * MvPolynomial.degreeOf 1 f ≤ Module.finrank K ↥(CorvajaZannier.finiteExtensionRiemannSpace K (CorvajaZannier.PlaneCurveFunctionField f) (planeMonomialPoleBudget K (CorvajaZannier.PlaneCurveFunctionField f) (CorvajaZannier.planeCurveFunction f 0) (CorvajaZannier.planeCurveFunction f 1) n (MvPolynomial.degreeOf 1 f)))

theorem BGS.HasseWeil.exists_planeCurve_onePointRiemannSpace_progression_lower_bound {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] {f : MvPolynomial (Fin 2) K} (habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : have hf := ⋯; have hx := ⋯; ∃ (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K (CorvajaZannier.PlaneCurveFunctionField f))), have Q := Sum.inr P; 0 < (finiteExtensionPoleDivisor K (CorvajaZannier.PlaneCurveFunctionField f) (CorvajaZannier.planeCurveFunction f 0)) Q ∧ 0 < CorvajaZannier.finiteExtensionPlaceDegree K (CorvajaZannier.PlaneCurveFunctionField f) Q ∧ CorvajaZannier.finiteExtensionPlaceDegree K (CorvajaZannier.PlaneCurveFunctionField f) Q ≤ MvPolynomial.degreeOf 1 f ∧ ∀ (n : ℕ), have m := planeMonomialPoleLevel K (CorvajaZannier.PlaneCurveFunctionField f) (CorvajaZannier.planeCurveFunction f 0) (CorvajaZannier.planeCurveFunction f 1) n (MvPolynomial.degreeOf 1 f) Q; m = n * ((finiteExtensionPoleDivisor K (CorvajaZannier.PlaneCurveFunctionField f) (CorvajaZannier.planeCurveFunction f 0)) Q).toNat + (MvPolynomial.degreeOf 1 f - 1) * ((finiteExtensionPoleDivisor K (CorvajaZannier.PlaneCurveFunctionField f) (CorvajaZannier.planeCurveFunction f 1)) Q).toNat ∧ Module.Finite K ↥(CorvajaZannier.finiteExtensionOnePointRiemannSpace K (CorvajaZannier.PlaneCurveFunctionField f) Q m) ∧ m * CorvajaZannier.finiteExtensionPlaceDegree K (CorvajaZannier.PlaneCurveFunctionField f) Q + 1 ≤ Module.finrank K ↥(CorvajaZannier.finiteExtensionOnePointRiemannSpace K (CorvajaZannier.PlaneCurveFunctionField f) Q m) + planeCurveBidegreeGenusBudget f

An absolutely irreducible plane curve admits a controlled infinity place and an explicit arithmetic progression of one-point pole levels satisfying the coarse Riemann lower bound

m * degree(P) + 1 ≤ finrank L(m P) + g,

where g = (degreeOf 0 f - 1) * (degreeOf 1 f - 1). The first-partial hypothesis supplies the second-coordinate height bound used by the monomial budget; the second-partial hypothesis makes the first coordinate separating.

theorem BGS.HasseWeil.exists_planeCurve_onePointRiemannSpace_progression_strictLevels_lower_bound {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] {f : MvPolynomial (Fin 2) K} (habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : have hf := ⋯; have hx := ⋯; have constantAlg := ((algebraMap (RatFunc K) (CorvajaZannier.PlaneCurveFunctionField f)).comp (algebraMap K (RatFunc K))).toAlgebra; ∃ (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K (CorvajaZannier.PlaneCurveFunctionField f))), have Q := Sum.inr P; 0 < (finiteExtensionPoleDivisor K (CorvajaZannier.PlaneCurveFunctionField f) (CorvajaZannier.planeCurveFunction f 0)) Q ∧ 0 < CorvajaZannier.finiteExtensionPlaceDegree K (CorvajaZannier.PlaneCurveFunctionField f) Q ∧ CorvajaZannier.finiteExtensionPlaceDegree K (CorvajaZannier.PlaneCurveFunctionField f) Q ≤ MvPolynomial.degreeOf 1 f ∧ ∀ (n : ℕ), have m := planeMonomialPoleLevel K (CorvajaZannier.PlaneCurveFunctionField f) (CorvajaZannier.planeCurveFunction f 0) (CorvajaZannier.planeCurveFunction f 1) n (MvPolynomial.degreeOf 1 f) Q; planeCurveBidegreeGenusBudget f ≤ m → m - planeCurveBidegreeGenusBudget f ≤ (strictFiltrationLevels (fun (k : ℕ) => CorvajaZannier.finiteExtensionOnePointRiemannSpace K (CorvajaZannier.PlaneCurveFunctionField f) Q k) m).card

Along the progression from exists_planeCurve_onePointRiemannSpace_progression_lower_bound, every level m ≥ g contains at least m - g strict inclusions in the one-point Riemann filtration. Exact constants give the initial dimension one, while adding the selected place raises dimension by at most its residue degree.