Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.FormalZetaDegreeIndexOne

An ordinary-extension specialization of the degree-index argument #

Suppose a zeta series has the indexed denominator

(1 - T^d) (1 - q^d T^d).

After extending the constants by degree d, the formal identity is

Z_extended(T^d) = Z(T)^d.

If the extended zeta series has the ordinary denominator over the enlarged constant field, clearing denominators gives

P_extended(T^d) D(T)^(d - 1) = P(T)^d.

For d > 1, evaluation at T = 1 forces P(1) = 0. Thus the single, explicit noncancellation hypothesis P(1) ≠ 0 forces d = 1. This file contains only that formal algebra. Its ordinary-rationality premise for the extended zeta series is deliberately stronger than indexed rationality and is not used to close the geometric F. K. Schmidt argument. The noncircular indexed-to-indexed theorem is in FormalZetaDegreeIndexOneIndexed.

source
noncomputable def BGS.HasseWeil.indexedCurveZetaDenominatorPolynomial (q d : ℕ) :
Polynomial ℂ

Polynomial realization of the indexed curve-zeta denominator.

Equations
Instances For
    source
    @[simp]
    theorem BGS.HasseWeil.coe_indexedCurveZetaDenominatorPolynomial (q d : ℕ) :
    ↑(indexedCurveZetaDenominatorPolynomial q d) = indexedCurveZetaDenominator q d
    source
    @[simp]
    theorem BGS.HasseWeil.indexedCurveZetaDenominatorPolynomial_eval_one (q d : ℕ) :
    Polynomial.eval 1 (indexedCurveZetaDenominatorPolynomial q d) = 0
    source
    def BGS.HasseWeil.HasFormalDegreeExtensionZetaIdentity (Z extendedZeta : PowerSeries ℂ) (d : ℕ) :
    Prop

    The formal constant-extension identity Z_extended(T^d) = Z(T)^d.

    This is kept as an explicit proposition because proving it for the geometric closed-place zeta series is a separate part of the constant-extension argument.

    Equations
    Instances For
      source
      theorem BGS.HasseWeil.subst_coe_eq_coe_comp_X_pow (Q : Polynomial ℂ) (d : ℕ) (hd : 0 < d) :
      PowerSeries.subst (PowerSeries.X ^ d) ↑Q = ↑(Q.comp (Polynomial.X ^ d))

      Substituting T^d into a polynomial power series agrees with polynomial composition by T^d.

      source
      theorem BGS.HasseWeil.subst_curveZetaDenominator_pow (q d : ℕ) (hd : 0 < d) :
      PowerSeries.subst (PowerSeries.X ^ d) (curveZetaDenominator (q ^ d)) = indexedCurveZetaDenominator q d

      Substituting T^d into the ordinary denominator over the degree-d constant extension produces the indexed denominator over the original constant field.

      source
      theorem BGS.HasseWeil.clearedNumeratorIdentity_of_indexed_rational_and_degreeExtension (Z extendedZeta : PowerSeries ℂ) (q d : ℕ) (P extendedP : Polynomial ℂ) (hd : 0 < d) (hindexed : HasIndexedCurveZetaRationalForm Z q d P) (hextended : HasCurveZetaRationalForm extendedZeta (q ^ d) extendedP) (hextension : HasFormalDegreeExtensionZetaIdentity Z extendedZeta d) :
      extendedP.comp (Polynomial.X ^ d) * indexedCurveZetaDenominatorPolynomial q d ^ (d - 1) = P ^ d

      Clearing the base and constant-extension denominators leaves exactly d - 1 copies of the indexed denominator.

      No noncancellation hypothesis is used here.

      source
      theorem BGS.HasseWeil.indexedNumerator_eval_one_eq_zero_of_clearedIdentity (q d : ℕ) (P extendedP : Polynomial ℂ) (hd : 0 < d) (htwo : 2 ≤ d) (hcleared : extendedP.comp (Polynomial.X ^ d) * indexedCurveZetaDenominatorPolynomial q d ^ (d - 1) = P ^ d) :
      Polynomial.eval 1 P = 0

      If d > 1, the cleared identity forces the original indexed numerator to vanish at T = 1. This is the formal pole-order mismatch.

      source
      theorem BGS.HasseWeil.degreeIndex_eq_one_of_clearedNumeratorIdentity (q d : ℕ) (P extendedP : Polynomial ℂ) (hd : 0 < d) (hPone : Polynomial.eval 1 P ≠ 0) (hcleared : extendedP.comp (Polynomial.X ^ d) * indexedCurveZetaDenominatorPolynomial q d ^ (d - 1) = P ^ d) :
      d = 1

      Pure polynomial form of the F. K. Schmidt conclusion: numerator noncancellation at T = 1 rules out every positive index greater than one.

      source
      theorem BGS.HasseWeil.degreeIndex_eq_one_of_indexed_rational_and_degreeExtension (Z extendedZeta : PowerSeries ℂ) (q d : ℕ) (P extendedP : Polynomial ℂ) (hd : 0 < d) (hPone : Polynomial.eval 1 P ≠ 0) (hindexed : HasIndexedCurveZetaRationalForm Z q d P) (hextended : HasCurveZetaRationalForm extendedZeta (q ^ d) extendedP) (hextension : HasFormalDegreeExtensionZetaIdentity Z extendedZeta d) :
      d = 1

      Conditional ordinary-extension specialization of the degree-index theorem.

      This algebraic implication is retained as a convenience lemma. The geometric development does not use its strong ordinary-rationality premise for the degree-d constant extension; it uses the indexed-to-indexed replacement instead.