Automatic bidegree genus bound for plane curves

For an absolutely irreducible plane curve with both coordinate projections separating, the intrinsic genus of its function field is bounded by the bidegree monomial budget. The proof combines three already formalized ingredients:

• exactness of the constant field;
• Riemann--Roch for the exhaustive finite-extension divisor model;
• the finite-place bidegree form of Riemann's inequality.

The finite place needed by the one-point comparison is constructed above the prime (X) of K[X], so it is not an additional hypothesis.

@[instance_reducible]

noncomputable def BGS.HasseWeil.automaticGenusPolynomialAlgebra (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 curve genus bound automatic construction.

Equations

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

theorem BGS.HasseWeil.automaticGenusPolynomialTower (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.automaticGenusFiniteClosureIntegral (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.automaticGenusPolynomialTorsionFree (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.finiteExtensionFinitePlace_nonempty (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Nonempty (CorvajaZannier.FiniteExtensionFinitePlace K L)

A finite separable extension of K(X) has an exhaustive finite place. We select a prime of the finite integral closure lying above (X).

theorem BGS.HasseWeil.planeCurve_genus_le_bidegreeGenusBudget {K : Type u_1} [Field K] [Finite 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 := ⋯; MarkoffRiemannRoch.FunctionField.genus K (CorvajaZannier.PlaneCurveFunctionField f) ≤ planeCurveBidegreeGenusBudget f

The function-field genus of an absolutely irreducible plane curve is at most its bidegree monomial budget

(degreeOf 0 f - 1) * (degreeOf 1 f - 1).

This theorem has no Riemann--Roch, constant-field, or place hypothesis: all three are discharged by the existing formalized theory.