Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionZetaDegreeIndexOne

The geometric F. K. Schmidt composition #

This file composes indexed zeta rationality, numerator noncancellation, the formal constant-extension identity, and indexed rationality after exact constant extension. The extension is never assumed to have degree index one.

The only geometric input left explicit is the closed-place count identity for the constant extension whose degree is the original divisor-degree index.

source
@[instance_reducible]
noncomputable def BGS.HasseWeil.degreeIndexOneAutomaticConstantAlgebra (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 degree index one construction.

Equations
Instances For
    source
    theorem BGS.HasseWeil.degreeIndexOneAutomaticConstantTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] :
    IsScalarTower K (RatFunc K) L
    source
    theorem BGS.HasseWeil.exists_finiteExtensionClosedPlaceZeta_indexed_rational_nonvanishing_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 ∧ Polynomial.eval 1 P ≠ 0 ∧ HasIndexedCurveZetaRationalForm (formalPointCountZeta (finiteExtensionClosedPlaceExtensionCount K L)) (Nat.card K) (finiteExtensionDivisorDegreeIndex K L) P

    Exact constants automatically give an indexed rational numerator which does not vanish at T = 1.

    source
    @[instance_reducible]
    noncomputable def BGS.HasseWeil.degreeIndexOneBaseConstantAlgebra (C : Type u_3) (N : Type u_5) [Field C] [Field N] [Algebra (RatFunc C) N] :
    Algebra C N

    The algebra structure from C to N used in the finite extension zeta degree index one construction.

    Equations
    Instances For
      source
      theorem BGS.HasseWeil.degreeIndexOneBaseConstantTower (C : Type u_3) (N : Type u_5) [Field C] [Field N] [Algebra (RatFunc C) N] :
      IsScalarTower C (RatFunc C) N
      source
      noncomputable def BGS.HasseWeil.exactConstantExtensionClosedPlaceExtensionCount (C : Type u_3) (S : Type u_4) (N : Type u_5) [Field C] [Field S] [Field N] [Fintype S] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (r : ℕ) :
      ℕ

      The exhaustive closed-place point-count sequence of the exact constant extension, packaged with its canonical S(X)-function-field structure.

      Equations
      Instances For
        source
        theorem BGS.HasseWeil.exactConstantExtensionClosedPlaceExtensionCount_eq_classical_decidableEq (C : Type u_3) (S : Type u_4) (N : Type u_5) [Field C] [Field S] [Field N] [Fintype S] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (r : ℕ) :
        exactConstantExtensionClosedPlaceExtensionCount C S N hExact r = let E := ExactConstantExtension C N S; finiteExtensionClosedPlaceExtensionCount S E r

        Replacing the former explicit Classical.decEq choices by the canonical closed-place choices does not change the exact-constant-extension count.

        source
        theorem BGS.HasseWeil.finiteExtensionDivisorDegreeIndex_eq_one_of_exactConstantExtension_closedPlaceCount (C : Type u_3) (S : Type u_4) (N : Type u_5) [Field C] [Field S] [Field N] [Fintype C] [Fintype S] [DecidableEq C] [DecidableEq (RatFunc C)] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (hdegree : Module.finrank C S = finiteExtensionDivisorDegreeIndex C N) (hcount : ∀ (r : ℕ), exactConstantExtensionClosedPlaceExtensionCount C S N hExact r = finiteExtensionClosedPlaceExtensionCount C N (finiteExtensionDivisorDegreeIndex C N * r)) :
        finiteExtensionDivisorDegreeIndex C N = 1

        Noncircular geometric F. K. Schmidt theorem.

        S/C is required to have degree equal to the original divisor-degree index. The sole remaining geometric relation says that the closed-place point count after this constant extension at level r is the original count at level d*r. Indexed rationality of both zeta series, including the extension, is derived internally.