Riemann's inequality for divisors supported above infinity

The first coordinate of a plane curve has a pole at every branch above the rational-function place at infinity. Its pole divisor is therefore cofinal among effective divisors supported on those branches. A sufficiently large rectangular monomial pole budget dominates any such divisor.

The monomial budget already satisfies the bidegree form of Riemann's inequality. Removing the effective difference costs at most its divisor degree, so the same inequality descends to the original infinity-supported divisor.

theorem BGS.HasseWeil.exists_nsmul_ge_of_effective_supportedAtInfinity (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (E H : CorvajaZannier.FiniteExtensionDivisor K L) (hE : ∀ (v : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ E v) (hEfinite : ∀ (q : CorvajaZannier.FiniteExtensionFinitePlace K L), E (Sum.inl q) = 0) (hH : ∀ (v : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ H v) (hHinfinity : ∀ (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)), 0 < H (Sum.inr P)) : ∃ (n : ℕ), E ≤ n • H

An effective divisor supported above infinity is dominated by a natural multiple of any effective divisor that is positive at every infinity place.

theorem BGS.HasseWeil.planeCurve_infinitySupported_riemann_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) : have hx := ⋯; ∀ (E : CorvajaZannier.FiniteExtensionDivisor K (CorvajaZannier.PlaneCurveFunctionField f)), (∀ (v : CorvajaZannier.FiniteExtensionPlace K (CorvajaZannier.PlaneCurveFunctionField f)), 0 ≤ E v) → (∀ (q : CorvajaZannier.FiniteExtensionFinitePlace K (CorvajaZannier.PlaneCurveFunctionField f)), E (Sum.inl q) = 0) → (CorvajaZannier.finiteExtensionDivisorDegree K (CorvajaZannier.PlaneCurveFunctionField f) E).toNat + 1 ≤ Module.finrank K ↥(CorvajaZannier.finiteExtensionRiemannSpace K (CorvajaZannier.PlaneCurveFunctionField f) E) + planeCurveBidegreeGenusBudget f

Bidegree Riemann inequality for every effective divisor supported on the infinity branches of an absolutely irreducible plane curve.