Noncancellation of the indexed zeta numerator

The strict divisor-count growth across one degree-index step detects the uncancelled factor 1 - T^d in the indexed zeta denominator. This file proves the formal coefficient statement and then specializes it to the finite-extension effective-divisor series.

theorem BGS.HasseWeil.sum_range_coeff_mul_curveZetaDenominator (Z : PowerSeries ℂ) (q n : ℕ) : ∑ k ∈ Finset.range (n + 2), (PowerSeries.coeff k) (Z * curveZetaDenominator q) = (PowerSeries.coeff (n + 1)) Z - ↑q * (PowerSeries.coeff n) Z

The partial sum of the coefficients of Z(T) (1 - T) (1 - q T) is the boundary difference Z_{n+1} - q Z_n.

theorem BGS.HasseWeil.curveZetaNumerator_eval_one_ne_zero_of_boundary (Z : PowerSeries ℂ) (q n : ℕ) (P : Polynomial ℂ) (hdegree : P.natDegree < n + 2) (hboundary : ↑q * (PowerSeries.coeff n) Z ≠ (PowerSeries.coeff (n + 1)) Z) (hform : HasCurveZetaRationalForm Z q P) : Polynomial.eval 1 P ≠ 0

For an ordinary curve denominator, every sufficiently late strict boundary difference forces the numerator to be nonzero at T = 1.

noncomputable def BGS.HasseWeil.compressPowerSeries (d : ℕ) (Z : PowerSeries ℂ) : PowerSeries ℂ

Compress a power series supported in degrees divisible by d.

Equations

• BGS.HasseWeil.compressPowerSeries d Z = PowerSeries.mk fun (n : ℕ) => (PowerSeries.coeff (d * n)) Z

theorem BGS.HasseWeil.expand_compressPowerSeries_eq (Z : PowerSeries ℂ) (d : ℕ) (hd : 0 < d) (hsupport : ∀ (n : ℕ), ¬d ∣ n → (PowerSeries.coeff n) Z = 0) : (PowerSeries.expand d ⋯) (compressPowerSeries d Z) = Z

Expanding the compressed series recovers a series supported on multiples of d.

theorem BGS.HasseWeil.expand_curveZetaDenominator (q d : ℕ) (hd : 0 < d) : (PowerSeries.expand d ⋯) (curveZetaDenominator (q ^ d)) = indexedCurveZetaDenominator q d

Power-series expansion sends the ordinary denominator over q^d to the indexed denominator over q.

theorem BGS.HasseWeil.coe_polynomial_expand (P : Polynomial ℂ) (d : ℕ) (hd : 0 < d) : ↑((Polynomial.expand ℂ d) P) = (PowerSeries.expand d ⋯) ↑P

Polynomial and power-series expansion commute with the polynomial coercion.

theorem BGS.HasseWeil.hasCurveZetaRationalForm_compress_of_indexed (Z : PowerSeries ℂ) (q d : ℕ) (P : Polynomial ℂ) (hd : 0 < d) (hsupport : ∀ (n : ℕ), ¬d ∣ n → (PowerSeries.coeff n) Z = 0) (hindexed : HasIndexedCurveZetaRationalForm Z q d P) : HasCurveZetaRationalForm (compressPowerSeries d Z) (q ^ d) (Polynomial.contract d P)

Indexed rationality for a series supported on multiples of d compresses to ordinary rationality, with numerator P.contract d.

theorem BGS.HasseWeil.polynomial_expand_contract_eq_of_indexed (Z : PowerSeries ℂ) (q d : ℕ) (P : Polynomial ℂ) (hd : 0 < d) (hsupport : ∀ (n : ℕ), ¬d ∣ n → (PowerSeries.coeff n) Z = 0) (hindexed : HasIndexedCurveZetaRationalForm Z q d P) : (Polynomial.expand ℂ d) (Polynomial.contract d P) = P

Under the same support hypothesis, the indexed polynomial is the d-fold expansion of its contraction.

theorem BGS.HasseWeil.indexedCurveZetaNumerator_eval_one_ne_zero_of_growth (Z : PowerSeries ℂ) (A : ℕ → ℕ) (q d n : ℕ) (P : Polynomial ℂ) (hd : 0 < d) (hcoeff : ∀ (m : ℕ), (PowerSeries.coeff m) Z = ↑(A m)) (hsupport : ∀ (m : ℕ), ¬d ∣ m → A m = 0) (hn : d ∣ n) (hdegree : P.natDegree < n + 2 * d) (hgrowth : q ^ d * A n < A (n + d)) (hindexed : HasIndexedCurveZetaRationalForm Z q d P) : Polynomial.eval 1 P ≠ 0

A sufficiently late strict growth witness in one admissible degree forces noncancellation of the indexed numerator at T = 1.

The bound P.natDegree < n + 2*d is the exact condition needed after compressing degrees by d; the admissibility condition d ∣ n identifies the boundary coefficients with consecutive compressed coefficients.

theorem BGS.HasseWeil.effectiveDivisorCountSeries_indexedNumerator_eval_one_ne_zero_of_growth (A : ℕ → ℕ) (q d n : ℕ) (P : Polynomial ℂ) (hd : 0 < d) (hsupport : ∀ (m : ℕ), ¬d ∣ m → A m = 0) (hn : d ∣ n) (hdegree : P.natDegree < n + 2 * d) (hgrowth : q ^ d * A n < A (n + d)) (hindexed : HasIndexedCurveZetaRationalForm (effectiveDivisorCountSeries A) q d P) : Polynomial.eval 1 P ≠ 0

The coefficient-cast effective-divisor series inherits indexed numerator noncancellation from any sufficiently late admissible strict-growth witness.

@[instance_reducible]

noncomputable def BGS.HasseWeil.numeratorNoncancellationConstantAlgebra (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 numerator noncancellation construction.

Equations

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

theorem BGS.HasseWeil.numeratorNoncancellationConstantTower (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_eq_zero_of_not_dvd_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] (n : ℕ) (hn : ¬finiteExtensionDivisorDegreeIndex K L ∣ n) : finiteExtensionEffectiveDivisorCount K L n = 0

The finite-extension effective-divisor series is supported precisely in degrees admissible for the divisor-degree index.

theorem BGS.HasseWeil.exists_finiteExtensionEffectiveDivisorCount_pow_mul_lt_add_index_ge (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 lowerBound : ℕ) (hconstants : algebraicClosure K L = ⊥) (hRiemann : HasFiniteExtensionUniformEventualRiemannFormula K L genus threshold) : ∃ (n : ℕ), lowerBound ≤ n ∧ threshold ≤ n ∧ finiteExtensionDivisorDegreeIndex K L ∣ n ∧ Nat.card K ^ finiteExtensionDivisorDegreeIndex K L * finiteExtensionEffectiveDivisorCount K L n < finiteExtensionEffectiveDivisorCount K L (n + finiteExtensionDivisorDegreeIndex K L)

Strict growth witnesses supplied by uniform Riemann--Roch can be chosen beyond any prescribed lower degree and remain divisible by the canonical divisor-degree index.

theorem BGS.HasseWeil.finiteExtensionEffectiveDivisorZeta_indexedNumerator_eval_one_ne_zero_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) (P : Polynomial ℂ) (hindexed : HasIndexedCurveZetaRationalForm (effectiveDivisorCountSeries (finiteExtensionEffectiveDivisorCount K L)) (Nat.card K) (finiteExtensionDivisorDegreeIndex K L) P) : Polynomial.eval 1 P ≠ 0

Uniform Riemann--Roch forces noncancellation for every indexed rational form of the finite-extension effective-divisor series.

theorem BGS.HasseWeil.finiteExtensionClosedPlaceZeta_indexedNumerator_eval_one_ne_zero_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) (P : Polynomial ℂ) (hindexed : HasIndexedCurveZetaRationalForm (formalPointCountZeta (finiteExtensionClosedPlaceExtensionCount K L)) (Nat.card K) (finiteExtensionDivisorDegreeIndex K L) P) : Polynomial.eval 1 P ≠ 0

Uniform Riemann--Roch also forces noncancellation for every indexed rational form of the exhaustive closed-place point-count zeta series.

theorem BGS.HasseWeil.exists_finiteExtensionClosedPlaceZeta_indexed_rational_nonvanishing (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 ∧ Polynomial.eval 1 P ≠ 0 ∧ HasIndexedCurveZetaRationalForm (formalPointCountZeta (finiteExtensionClosedPlaceExtensionCount K L)) (Nat.card K) (finiteExtensionDivisorDegreeIndex K L) P

The finite-extension closed-place zeta series has an indexed rational form whose numerator is normalized and does not vanish at T = 1.