Canonicality criterion for the finite-extension different divisor

The Corvaja--Zannier development constructs the divisor of the separating differential dX place by place: its finite coefficients are trace-different multiplicities, and its coefficients above infinity are the different multiplicity minus twice the ramification index. The Riemann--Roch library, on the other hand, defines canonical divisors as maximal vanishing divisors of nonzero adelic Weil functionals.

This module gives the exact theorem-level reduction between those two presentations. It does not assume or package canonicality. The target is equivalent to:

• the Riemann--Hurwitz identity for the total trace different; and

• the dimension statement

  genus K L ≤ finrank K (finiteExtensionRiemannSpace K L Ddiff).

Once the degree identity is known, Riemann--Roch proves that this finrank is already between g - 1 and g. Thus the exact remaining trace-residue/Kähler-to-Weil theorem is the displayed lower bound: construct the Weil functional attached to dX, identify its local annihilator with the trace-different/Kähler module, and thereby close the last one-dimensional gap.

@[instance_reducible]

noncomputable def BGS.HasseWeil.canonicalCriterionConstantAlgebra (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 canonicality criterion construction.

Equations

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

theorem BGS.HasseWeil.canonicalCriterionConstantTower (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.canonicalCriterionPolynomialAlgebra (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 canonicality criterion construction.

Equations

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

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

theorem BGS.HasseWeil.chart_ell_le_one_of_degree_eq_zero (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] [MarkoffRiemannRoch.FunctionField.IsFullConstantField K L] (D : MarkoffRiemannRoch.FunctionField.Chart.DivisorA K L) (hdegree : MarkoffRiemannRoch.FunctionField.Chart.deg K L D = 0) : MarkoffRiemannRoch.FunctionField.Chart.ell K L D ≤ 1

A degree-zero chart divisor has a Riemann--Roch space of dimension at most one.

theorem BGS.HasseWeil.chart_ell_le_genus_of_degree_eq_two_genus_sub_two (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] [MarkoffRiemannRoch.FunctionField.IsFullConstantField K L] (D : MarkoffRiemannRoch.FunctionField.Chart.DivisorA K L) (hdegree : MarkoffRiemannRoch.FunctionField.Chart.deg K L D = 2 * ↑(MarkoffRiemannRoch.FunctionField.Chart.genus K L) - 2) : MarkoffRiemannRoch.FunctionField.Chart.ell K L D ≤ MarkoffRiemannRoch.FunctionField.Chart.genus K L

At canonical degree, Riemann--Roch leaves at most a one-dimensional defect from canonicality.

theorem BGS.HasseWeil.finiteExtensionCanonicalDifferent_isCanonical_iff_degree_finrank (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] [MarkoffRiemannRoch.FunctionField.IsFullConstantField K L] : MarkoffRiemannRoch.FunctionField.Chart.IsCanonical K L ((finiteExtensionDivisorEquivChart K L) (CorvajaZannier.finiteExtensionCanonicalDifferentDivisor K L ⋯)) ↔ CorvajaZannier.finiteExtensionDivisorDegree K L (CorvajaZannier.finiteExtensionCanonicalDifferentDivisor K L ⋯) = 2 * ↑(MarkoffRiemannRoch.FunctionField.Chart.genus K L) - 2 ∧ Module.finrank K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L (CorvajaZannier.finiteExtensionCanonicalDifferentDivisor K L ⋯)) = MarkoffRiemannRoch.FunctionField.Chart.genus K L

Canonicality of the explicit different divisor is equivalent to its canonical degree and canonical Riemann--Roch dimension. Both conditions are stated entirely in the exhaustive BGS divisor model.

theorem BGS.HasseWeil.finiteExtensionCanonicalDifferent_isCanonical_iff_genus_le_finrank_of_degree_eq (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] [MarkoffRiemannRoch.FunctionField.IsFullConstantField K L] (hdegree : CorvajaZannier.finiteExtensionDivisorDegree K L (CorvajaZannier.finiteExtensionCanonicalDifferentDivisor K L ⋯) = 2 * ↑(MarkoffRiemannRoch.FunctionField.Chart.genus K L) - 2) : MarkoffRiemannRoch.FunctionField.Chart.IsCanonical K L ((finiteExtensionDivisorEquivChart K L) (CorvajaZannier.finiteExtensionCanonicalDifferentDivisor K L ⋯)) ↔ MarkoffRiemannRoch.FunctionField.Chart.genus K L ≤ Module.finrank K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L (CorvajaZannier.finiteExtensionCanonicalDifferentDivisor K L ⋯))

Once Riemann--Hurwitz supplies the degree identity, canonicality is equivalent to closing the single remaining Riemann--Roch dimension gap.

theorem BGS.HasseWeil.finiteExtensionCanonicalDifferent_finrank_bounds_of_degree_eq (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] [MarkoffRiemannRoch.FunctionField.IsFullConstantField K L] (hdegree : CorvajaZannier.finiteExtensionDivisorDegree K L (CorvajaZannier.finiteExtensionCanonicalDifferentDivisor K L ⋯) = 2 * ↑(MarkoffRiemannRoch.FunctionField.Chart.genus K L) - 2) : ↑(MarkoffRiemannRoch.FunctionField.Chart.genus K L) - 1 ≤ ↑(Module.finrank K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L (CorvajaZannier.finiteExtensionCanonicalDifferentDivisor K L ⋯))) ∧ Module.finrank K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L (CorvajaZannier.finiteExtensionCanonicalDifferentDivisor K L ⋯)) ≤ MarkoffRiemannRoch.FunctionField.Chart.genus K L

The degree identity leaves at most one unit of uncertainty in the Riemann--Roch dimension of the explicit different divisor.

theorem BGS.HasseWeil.finiteExtensionCanonicalDifferent_degree_eq_two_genus_sub_two_iff (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] : CorvajaZannier.finiteExtensionDivisorDegree K L (CorvajaZannier.finiteExtensionCanonicalDifferentDivisor K L ⋯) = 2 * ↑(MarkoffRiemannRoch.FunctionField.Chart.genus K L) - 2 ↔ ↑(CorvajaZannier.finiteExtensionFiniteDifferentDegree K L ⋯) + ↑(CorvajaZannier.infinityDifferentDegree K L) = 2 * ↑(Module.finrank (RatFunc K) L) + 2 * ↑(MarkoffRiemannRoch.FunctionField.Chart.genus K L) - 2

The degree half of canonicality is exactly the Riemann--Hurwitz identity for the finite and infinite trace different.