Unconditional indexed zeta rationality from exact constants

This file discharges the uniform Riemann--Roch premise of the indexed zeta composition by transporting the vendored Riemann--Roch theorem to the exhaustive BGS divisor model.

@[instance_reducible]

noncomputable def BGS.HasseWeil.automaticIndexedZetaConstantAlgebra (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 indexed zeta rationality automatic construction.

Equations

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

theorem BGS.HasseWeil.automaticIndexedZetaConstantTower (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.automaticIndexedZetaPolynomialAlgebra (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 indexed zeta rationality automatic construction.

Equations

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

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

theorem BGS.HasseWeil.exists_finiteExtensionClosedPlaceZeta_indexed_rational_of_constants (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 = ⊥) : ∃ (P : Polynomial ℂ), P.coeff 0 = 1 ∧ HasIndexedCurveZetaRationalForm (formalPointCountZeta (finiteExtensionClosedPlaceExtensionCount K L)) (Nat.card K) (finiteExtensionDivisorDegreeIndex K L) P

Exact constants alone supply the indexed rational form of the exhaustive closed-place zeta series.

theorem BGS.HasseWeil.exists_finiteExtensionClosedPlaceZeta_indexed_rational_with_natDegree_lt_of_constants (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 = ⊥) : ∃ (genus : ℕ) (threshold : ℕ) (P : Polynomial ℂ), HasFiniteExtensionUniformEventualRiemannFormula K L genus threshold ∧ P.coeff 0 = 1 ∧ P.natDegree < threshold + 2 * finiteExtensionDivisorDegreeIndex K L ∧ HasIndexedCurveZetaRationalForm (formalPointCountZeta (finiteExtensionClosedPlaceExtensionCount K L)) (Nat.card K) (finiteExtensionDivisorDegreeIndex K L) P

The same automatic composition retains the truncation bound on the indexed numerator.