Indexed zeta rationality for an exact-constant function field

This file composes the exhaustive divisor-class recurrence with the proved closed-place Euler recurrence. The only input at this boundary is the uniform Riemann--Roch formula for arbitrary divisors. The denominator still uses the divisor-degree index; replacing it by the standard degree-one denominator is a separate constant-field theorem.

@[instance_reducible]

noncomputable def BGS.HasseWeil.indexedZetaConstantAlgebra (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 construction.

Equations

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

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

theorem BGS.HasseWeil.finiteExtensionEffectiveDivisorCount_zero (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] : finiteExtensionEffectiveDivisorCount K L 0 = 1

There is exactly one effective exhaustive divisor of degree zero.

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

Uniform Riemann--Roch, exact constants, and the exhaustive Euler product give the indexed rational form of the closed-place zeta series.