A discrete simple-pole witness for the divisor zeta series

The eventual Riemann--Roch class formula shows that, in every sufficiently large admissible degree, advancing by the divisor-degree index produces more effective divisors than multiplication by the corresponding power of the constant-field cardinality. This is the coefficient-level noncancellation behind the simple pole at T = 1.

@[instance_reducible]

noncomputable def BGS.HasseWeil.simplePoleConstantAlgebra (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 zeta simple pole construction.

Equations

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

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

noncomputable def BGS.HasseWeil.finiteExtensionDivisorClassOfDegreeIndexMul (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] (m : ℕ) : FiniteExtensionDivisorClassOfDegree K L ↑(m * finiteExtensionDivisorDegreeIndex K L)

Multiples of the canonical index divisor give actual divisor classes in all integer degrees that are nonnegative multiples of the index.

Equations

• BGS.HasseWeil.finiteExtensionDivisorClassOfDegreeIndexMul K L m = ⟨(BGS.HasseWeil.finiteExtensionDivisorClassMap K L) (m • BGS.HasseWeil.finiteExtensionDivisorIndexRepresentative K L), ⋯⟩

theorem BGS.HasseWeil.finiteExtensionEffectiveDivisorCount_pow_mul_lt_add_index_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 n : ℕ) (hconstants : algebraicClosure K L = ⊥) (hRiemann : HasFiniteExtensionUniformEventualRiemannFormula K L genus threshold) (hn : threshold ≤ n) (hclass : Nonempty (FiniteExtensionDivisorClassOfDegree K L ↑n)) : Nat.card K ^ finiteExtensionDivisorDegreeIndex K L * finiteExtensionEffectiveDivisorCount K L n < finiteExtensionEffectiveDivisorCount K L (n + finiteExtensionDivisorDegreeIndex K L)

In an admissible large degree, the effective-divisor coefficient grows strictly more than the geometric q^d multiple when the degree is advanced by the divisor-degree index d.

theorem BGS.HasseWeil.exists_finiteExtensionEffectiveDivisorCount_pow_mul_lt_add_index (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) : ∃ (n : ℕ), threshold ≤ n ∧ Nat.card K ^ finiteExtensionDivisorDegreeIndex K L * finiteExtensionEffectiveDivisorCount K L n < finiteExtensionEffectiveDivisorCount K L (n + finiteExtensionDivisorDegreeIndex K L)

There is always a sufficiently large admissible coefficient witnessing the strict simple-pole growth.