Standard zeta rationality after proving degree index one

This file packages the exact downstream consequence of F. K. Schmidt's degree-index theorem. Once the exhaustive divisor-degree index is one, the automatic indexed zeta rational form becomes the standard curve denominator (1 - T) (1 - qT). The Riemann--Roch construction also retains a concrete numerator-degree bound and numerator noncancellation at T = 1.

@[instance_reducible]

noncomputable def BGS.HasseWeil.standardZetaConstantAlgebra (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 standard zeta rationality construction.

Equations

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

theorem BGS.HasseWeil.standardZetaConstantTower (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.standardZetaPolynomialAlgebra (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 standard zeta rationality construction.

Equations

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

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

theorem BGS.HasseWeil.hasCurveZetaRationalForm_of_indexed_index_one (Z : PowerSeries ℂ) (q : ℕ) (P : Polynomial ℂ) (hindexed : HasIndexedCurveZetaRationalForm Z q 1 P) : HasCurveZetaRationalForm Z q P

An indexed zeta rational form with index one is exactly a standard curve zeta rational form.

theorem BGS.HasseWeil.exists_finiteExtensionClosedPlaceZeta_rational_with_natDegree_lt_of_uniformRiemann (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 : ℕ) (hconstants : algebraicClosure K L = ⊥) (hRiemann : HasFiniteExtensionUniformEventualRiemannFormula K L genus threshold) (hindex : finiteExtensionDivisorDegreeIndex K L = 1) : ∃ (P : Polynomial ℂ), P.coeff 0 = 1 ∧ Polynomial.eval 1 P ≠ 0 ∧ P.natDegree < threshold + 2 ∧ HasCurveZetaRationalForm (formalPointCountZeta (finiteExtensionClosedPlaceExtensionCount K L)) (Nat.card K) P

Uniform Riemann--Roch and degree index one give a normalized standard zeta numerator. Its degree is bounded by the same truncation length used in the indexed recurrence, and its value at T = 1 is nonzero.

theorem BGS.HasseWeil.exists_finiteExtensionClosedPlaceZeta_rational_with_genus_degree_bound (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] (hconstants : algebraicClosure K L = ⊥) (hindex : finiteExtensionDivisorDegreeIndex K L = 1) : ∃ (P : Polynomial ℂ), P.coeff 0 = 1 ∧ Polynomial.eval 1 P ≠ 0 ∧ P.natDegree < 2 * MarkoffRiemannRoch.FunctionField.genus K L + 2 ∧ HasCurveZetaRationalForm (formalPointCountZeta (finiteExtensionClosedPlaceExtensionCount K L)) (Nat.card K) P

Exact constants and degree index one give the standard curve zeta form with numerator degree strictly below 2g + 2, where g is the transported function-field genus.

theorem BGS.HasseWeil.exists_finiteExtensionClosedPlaceZeta_trace_with_degree_budget (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] (budget : ℕ) (hconstants : algebraicClosure K L = ⊥) (hindex : finiteExtensionDivisorDegreeIndex K L = 1) (hgenus : MarkoffRiemannRoch.FunctionField.genus K L ≤ budget) : ∃ (P : Polynomial ℂ), P.coeff 0 = 1 ∧ Polynomial.eval 1 P ≠ 0 ∧ P.natDegree ≤ 2 * budget + 1 ∧ HasCurveZetaRationalForm (formalPointCountZeta (finiteExtensionClosedPlaceExtensionCount K L)) (Nat.card K) P ∧ HasZetaNumeratorPointCountFormula (Nat.card K) (finiteExtensionClosedPlaceExtensionCount K L) P

If the intrinsic genus is at most budget, the standard numerator has at most 2 * budget + 1 reciprocal roots. The same polynomial carries the formal extension point-count trace formula.