Bounding the Riemann--Roch genus from a one-point inequality

Once the uniform Riemann--Roch formula is known, any coarse one-point Riemann inequality bounds its genus parameter. This is the bridge that will turn the existing bidegree monomial budget into a numerator-degree bound.

@[instance_reducible]

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

The algebra structure from K to L used in the finite extension genus bound construction.

Equations

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

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

theorem BGS.HasseWeil.genus_le_budget_of_uniformRiemann_onePoint (K : Type u_1) [Field K] [Fintype 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] (genus threshold budget : ℕ) (P : CorvajaZannier.FiniteExtensionPlace K L) (hRiemann : HasFiniteExtensionUniformEventualRiemannFormula K L genus threshold) (hLower : ∀ (N : ℕ), N * CorvajaZannier.finiteExtensionPlaceDegree K L P + 1 ≤ Module.finrank K ↥(CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P N) + budget) : genus ≤ budget

A one-point lower Riemann inequality with budget budget, together with the uniform eventual Riemann--Roch formula, forces genus ≤ budget.