Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtensionFrobeniusTwistStepanovUpper

A uniform Stepanov upper bound for exact-constant Frobenius twists #

For one fixed exact extension of the constants, the Frobenius-twist fixed fields have a common finite-place Riemann budget and exact constant field. When the ground constant field is a square, the intrinsic one-point Stepanov theorem therefore applies to every twist with the same numerical budget. The degree theorem for the twists replaces the residual function-field degree term by the degree of the original field.

This is the uniform upper estimate used in the fixed-field averaging route to Hasse--Weil. It does not require a separate genus-invariance hypothesis: the common Riemann budget is the exact input consumed by the Stepanov theorem.

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

The algebra structure from C to N used in the exact constant extension frobenius twist stepanov upper construction.

Equations
Instances For
    source
    theorem BGS.HasseWeil.twistStepanovBaseConstantTower (C : Type u_2) (N : Type u_3) [Field C] [Field N] [Algebra (RatFunc C) N] :
    IsScalarTower C (RatFunc C) N
    source
    @[instance_reducible]
    noncomputable def BGS.HasseWeil.twistStepanovFieldDecidableEq (F : Type u_5) :
    DecidableEq F

    Classical equality on the Frobenius-twisted constant field for the Stepanov bound.

    Equations
    Instances For
      source
      @[instance_reducible]
      noncomputable def BGS.HasseWeil.twistStepanovRatFuncDecidableEq (F : Type u_5) [Field F] :
      DecidableEq (RatFunc F)

      Classical equality on its rational function field for the Stepanov bound.

      Equations
      Instances For
        source
        theorem BGS.HasseWeil.exists_uniform_frobeniusTwistField_squareFieldStepanov_budget (K : Type u_1) (C : Type u_2) (N : Type u_3) (S : Type u_4) [Field K] [Fintype K] [Field C] [Fintype C] [DecidableEq C] [Algebra K C] [DecidableEq (RatFunc C)] [Field N] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [Field S] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] [Finite S] (hcard : Fintype.card C = Fintype.card K ^ 2) (hExact : algebraicClosure C N = ⊥) (hdiv : Nat.card Gal(N/RatFunc C) ∣ Module.finrank C S) :
        have T := ExactConstantExtension C N S; ∃ (budget : ℕ), ∀ (g : Gal(N/RatFunc C)), let F := exactConstantExtensionFrobeniusTwistField C (RatFunc C) N S hExact g; (budget + 1) * (budget + 2) ≤ Fintype.card K → finiteExtensionRationalPlaceCount C ↥F ≤ Fintype.card C + (2 * budget + 1) * Fintype.card K + Module.finrank (RatFunc C) N

        A single Stepanov budget gives the square-field rational-place upper bound for every Frobenius-twist fixed field. The final degree term is uniform: it is the degree of the original function field N / C(X).

        The divisibility condition is exactly the one used to prove that every twist has the same degree as N; in the Stichtenoth construction it is ensured by the chosen constant-extension degree.

        source
        theorem BGS.HasseWeil.frobeniusTwistFieldRationalPlaceCount_le_squareField_of_genus (K : Type u_1) (C : Type u_2) (N : Type u_3) (S : Type u_4) [Field K] [Fintype K] [Field C] [Fintype C] [DecidableEq C] [Algebra K C] [DecidableEq (RatFunc C)] [Field N] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [IsGalois (RatFunc C) N] [Field S] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] [Finite S] (hcard : Fintype.card C = Fintype.card K ^ 2) (hExact : algebraicClosure C N = ⊥) (hdiv : Nat.card Gal(N/RatFunc C) ∣ Module.finrank C S) (g : Gal(N/RatFunc C)) (hlarge : (MarkoffRiemannRoch.FunctionField.genus C N + 1) * (MarkoffRiemannRoch.FunctionField.genus C N + 2) ≤ Fintype.card K) :
        frobeniusTwistFieldRationalPlaceCount C S N hExact g ≤ Fintype.card C + (2 * MarkoffRiemannRoch.FunctionField.genus C N + 1) * Fintype.card K + Module.finrank (RatFunc C) N

        The uniform twist estimate with the intrinsic genus of the original field as its fixed budget. Unlike the existential compatibility theorem above, every constant in this statement is independent of the auxiliary constant extension S.

        source
        theorem BGS.HasseWeil.abs_frobeniusTwistFieldRationalPlaceError_le_squareField_of_genus (K : Type u_1) (C : Type u_2) (N : Type u_3) (S : Type u_4) [Field K] [Fintype K] [Field C] [Fintype C] [DecidableEq C] [Algebra K C] [DecidableEq (RatFunc C)] [Field N] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [IsGalois (RatFunc C) N] [Field S] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] [Finite S] (hcard : Fintype.card C = Fintype.card K ^ 2) (hExact : algebraicClosure C N = ⊥) (hdiv : Nat.card Gal(N/RatFunc C) ∣ Module.finrank C S) (hlarge : (MarkoffRiemannRoch.FunctionField.genus C N + 1) * (MarkoffRiemannRoch.FunctionField.genus C N + 2) ≤ Fintype.card K) (g : Gal(N/RatFunc C)) :
        |↑(frobeniusTwistFieldRationalPlaceCount C S N hExact g) - ↑(Nat.card C) - 1| ≤ ↑(Nat.card Gal(N/RatFunc C)) * ↑(Module.finrank (RatFunc C) N) + ↑(Nat.card Gal(N/RatFunc C) - 1) * ↑((2 * MarkoffRiemannRoch.FunctionField.genus C N + 1) * Fintype.card K + Module.finrank (RatFunc C) N)

        Combining the genus-uniform Stepanov upper bound with the bounded complete-place average gives a two-sided estimate for every rational-base twist. All constants shown here are independent of S.