Canonical-different genus bridge

The explicit different divisor used by the Corvaja--Zannier development has the correct degree bound under only one separating coordinate. This module isolates the exact remaining bridge to the intrinsic Riemann--Roch genus: after transporting that divisor to the Riemann--Roch chart, it must be shown to be canonical.

No canonicality premise is hidden in a definition. The generic theorem below takes MarkoffRiemannRoch.FunctionField.Chart.IsCanonical explicitly, while the plane theorem proves the complete degree estimate available below that boundary.

@[instance_reducible]

noncomputable def BGS.HasseWeil.canonicalGenusConstantAlgebra (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 canonical different genus bound construction.

Equations

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

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

@[instance_reducible]

noncomputable def BGS.HasseWeil.canonicalGenusPolynomialAlgebra (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 finite extension canonical different genus bound construction.

Equations

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

theorem BGS.HasseWeil.canonicalGenusPolynomialTower (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.canonicalGenusConstantPolynomialTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K (Polynomial K) L

theorem BGS.HasseWeil.finiteExtension_genus_le_budget_of_canonicalDifferent_isCanonical (K : Type u_1) [Field 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] [MarkoffRiemannRoch.FunctionField.IsFullConstantField K L] (budget : ℕ) (hcanonical : MarkoffRiemannRoch.FunctionField.Chart.IsCanonical K L ((finiteExtensionDivisorEquivChart K L) (CorvajaZannier.finiteExtensionCanonicalDifferentDivisor K L ⋯))) (hdegree : CorvajaZannier.finiteExtensionDivisorDegree K L (CorvajaZannier.finiteExtensionCanonicalDifferentDivisor K L ⋯) ≤ 2 * ↑budget - 2) : MarkoffRiemannRoch.FunctionField.genus K L ≤ budget

Identifying the explicit different divisor with a canonical divisor turns any upper bound for its degree into a genus bound.

theorem BGS.HasseWeil.planeCurve_canonicalDifferentDivisor_degree_le_two_genusBudget_sub_two {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (hcardK : MvPolynomial.degreeOf 1 f < Fintype.card K) : have hx := ⋯; CorvajaZannier.finiteExtensionDivisorDegree K (CorvajaZannier.PlaneCurveFunctionField f) (CorvajaZannier.finiteExtensionCanonicalDifferentDivisor K (CorvajaZannier.PlaneCurveFunctionField f) ⋯) ≤ 2 * ↑(planeCurveBidegreeGenusBudget f) - 2

The one-separating-coordinate canonical-degree estimate already has exactly the degree shape needed for the bidegree genus budget.