Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionZetaDegreeIndexOneAutomatic

Automatic divisor-degree index one #

The exact constant-extension splitting formula supplies the sole geometric hypothesis of the noncircular F. K. Schmidt argument. Consequently a finite separable function field with exact constants has divisor-degree index one.

source
@[instance_reducible]
noncomputable def BGS.HasseWeil.automaticIndexOneBaseConstantAlgebra (C : Type u_1) (N : Type u_2) [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 automatic construction.

Equations
Instances For
    source
    theorem BGS.HasseWeil.automaticIndexOneBaseConstantTower (C : Type u_1) (N : Type u_2) [Field C] [Field N] [Algebra (RatFunc C) N] :
    IsScalarTower C (RatFunc C) N
    source
    theorem BGS.HasseWeil.finiteExtensionDivisorDegreeIndex_eq_one_of_exactConstants (C : Type u_1) (N : Type u_2) [Field C] [DecidableEq C] [DecidableEq (RatFunc C)] [Field N] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [Finite C] (hExact : algebraicClosure C N = ⊥) :
    finiteExtensionDivisorDegreeIndex C N = 1

    F. K. Schmidt's divisor-index-one theorem, with the constant-extension closed-place identity discharged internally.

    source
    theorem BGS.HasseWeil.exists_finiteExtensionClosedPlaceZeta_rational_with_genus_degree_bound_of_exactConstants (C : Type u_1) (N : Type u_2) [Field C] [Fintype C] [DecidableEq C] [DecidableEq (RatFunc C)] [Field N] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] (hExact : algebraicClosure C N = ⊥) :
    ∃ (P : Polynomial ℂ), P.coeff 0 = 1 ∧ Polynomial.eval 1 P ≠ 0 ∧ P.natDegree < 2 * MarkoffRiemannRoch.FunctionField.genus C N + 2 ∧ HasCurveZetaRationalForm (formalPointCountZeta (finiteExtensionClosedPlaceExtensionCount C N)) (Nat.card C) P

    Exact constants now give the standard curve zeta form without a separate divisor-index hypothesis.

    source
    theorem BGS.HasseWeil.exists_finiteExtensionClosedPlaceZeta_trace_with_degree_budget_of_exactConstants (C : Type u_1) (N : Type u_2) [Field C] [Fintype C] [DecidableEq C] [DecidableEq (RatFunc C)] [Field N] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] (budget : ℕ) (hExact : algebraicClosure C N = ⊥) (hgenus : MarkoffRiemannRoch.FunctionField.genus C N ≤ budget) :
    ∃ (P : Polynomial ℂ), P.coeff 0 = 1 ∧ Polynomial.eval 1 P ≠ 0 ∧ P.natDegree ≤ 2 * budget + 1 ∧ HasCurveZetaRationalForm (formalPointCountZeta (finiteExtensionClosedPlaceExtensionCount C N)) (Nat.card C) P ∧ HasZetaNumeratorPointCountFormula (Nat.card C) (finiteExtensionClosedPlaceExtensionCount C N) P

    Exact constants and an intrinsic genus budget give the standard zeta trace package with no remaining degree-index premise.