Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionDivisibleErrorFromConstantBase

Divisible-even errors from one enlarged constant field #

Let F / K(X) have exact constant field K, and let C / K be finite Galois of degree r. Exact constant-extension splitting identifies the closed-place count of C F at level m with the count of F at level r m. Since #C = (#K)^r, a square-root-scale estimate for C F along the levels 2 H n is therefore exactly such an estimate for F along the fixed divisible-even subsequence 2 (r H) n.

source
@[instance_reducible]
noncomputable def BGS.HasseWeil.divisibleErrorBaseConstantAlgebra (K : Type u_1) (F : Type u_3) [Field K] [Field F] [Algebra (RatFunc K) F] :
Algebra K F

The algebra structure from K to F used in the finite extension divisible error from constant base construction.

Equations
Instances For
    source
    theorem BGS.HasseWeil.divisibleErrorBaseConstantTower (K : Type u_1) (F : Type u_3) [Field K] [Field F] [Algebra (RatFunc K) F] :
    IsScalarTower K (RatFunc K) F
    source
    theorem BGS.HasseWeil.finiteExtensionClosedPlace_divisibleEvenError_bound_of_constantBase (K : Type u_1) (C : Type u_2) (F : Type u_3) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] [Field C] [Fintype C] [Algebra K C] [FiniteDimensional K C] [IsGalois K C] [Field F] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) (H : ℕ) (A B : ℝ) (hbound : ∀ (n : ℕ), 0 < n → |↑(exactConstantExtensionClosedPlaceExtensionCount K C F hExact (2 * H * n)) - ↑(Nat.card C) ^ (2 * H * n) - 1| ≤ A + B * ↑(Nat.card C) ^ (H * n)) (n : ℕ) :
    0 < n → |↑(finiteExtensionClosedPlaceExtensionCount K F (2 * (Module.finrank K C * H) * n)) - ↑(Nat.card K) ^ (2 * (Module.finrank K C * H) * n) - 1| ≤ A + B * (↑(Nat.card K) ^ (Module.finrank K C * H)) ^ n

    Pointwise error transport from the scalar extension C F to F. The multiplier r H, where r = [C : K], is independent of n.

    source
    theorem BGS.HasseWeil.finiteExtensionClosedPlace_divisibleEvenError_isBigO_of_constantBase (K : Type u_1) (C : Type u_2) (F : Type u_3) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] [Field C] [Fintype C] [Algebra K C] [FiniteDimensional K C] [IsGalois K C] [Field F] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) (H : ℕ) (A B : ℝ) (hA : 0 ≤ A) (hbound : ∀ (n : ℕ), 0 < n → |↑(exactConstantExtensionClosedPlaceExtensionCount K C F hExact (2 * H * n)) - ↑(Nat.card C) ^ (2 * H * n) - 1| ≤ A + B * ↑(Nat.card C) ^ (H * n)) :
    (fun (n : ℕ) => ↑(finiteExtensionClosedPlaceExtensionCount K F (2 * (Module.finrank K C * H) * n)) - ↑(Nat.card K) ^ (2 * (Module.finrank K C * H) * n) - 1) =O[Filter.atTop] fun (n : ℕ) => (↑(Nat.card K) ^ (Module.finrank K C * H)) ^ n

    The preceding pointwise transport immediately supplies the divisible-even IsBigO premise used by the spectral Hasse argument.

    source
    theorem BGS.HasseWeil.finiteExtensionClosedPlaceHasseBound_of_constantBase_bound (K : Type u_1) (C : Type u_2) (F : Type u_3) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] [Field C] [Fintype C] [Algebra K C] [FiniteDimensional K C] [IsGalois K C] [Field F] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (budget : ℕ) (hExact : algebraicClosure K F = ⊥) (hgenus : MarkoffRiemannRoch.FunctionField.genus K F ≤ budget) (H : ℕ) (hH : 0 < H) (A B : ℝ) (hA : 0 ≤ A) (hbound : ∀ (n : ℕ), 0 < n → |↑(exactConstantExtensionClosedPlaceExtensionCount K C F hExact (2 * H * n)) - ↑(Nat.card C) ^ (2 * H * n) - 1| ≤ A + B * ↑(Nat.card C) ^ (H * n)) :
    |↑(finiteExtensionClosedPlaceExtensionCount K F 1) - ↑(Nat.card K) - 1| ≤ (2 * ↑budget + 1) * √↑(Nat.card K)

    Closed Hasse--Weil over K from one fixed enlarged constant field. The geometric work is isolated in hbound; exact splitting and the spectral argument discharge every remaining count and zeta-function step.