A fixed-tower Hasse bound from intermediate Frobenius twists

The complete intermediate-base twist average is combined with the uniform square-field Stepanov estimate for the corresponding rational-base twists.

@[instance_reducible]

noncomputable def BGS.HasseWeil.intermediateHasseBaseConstantAlgebra (C : Type u_2) (N : Type u_4) [Field C] [Field N] [Algebra (RatFunc C) N] : Algebra C N

The algebra structure from C to N used in the exact constant extension intermediate frobenius twist hasse bound construction.

Equations

• BGS.HasseWeil.intermediateHasseBaseConstantAlgebra C N = BGS.HasseWeil.bridgeBaseConstantAlgebra C N

theorem BGS.HasseWeil.intermediateHasseBaseConstantTower (C : Type u_2) (N : Type u_4) [Field C] [Field N] [Algebra (RatFunc C) N] : IsScalarTower C (RatFunc C) N

@[instance_reducible]

noncomputable def BGS.HasseWeil.intermediateHasseConstantAlgebra (C : Type u_2) [Field C] (L : Type u_5) [Field L] [Algebra (RatFunc C) L] : Algebra C L

The algebra structure from C to L used in the exact constant extension intermediate frobenius twist hasse bound construction.

Equations

• BGS.HasseWeil.intermediateHasseConstantAlgebra C L = ((algebraMap (RatFunc C) L).comp (algebraMap C (RatFunc C))).toAlgebra

theorem BGS.HasseWeil.intermediateHasseConstantTower (C : Type u_2) (N : Type u_4) [Field C] [Field N] [Algebra (RatFunc C) N] (L : Type u_5) [Field L] [Algebra (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] : IsScalarTower C L N

theorem BGS.HasseWeil.intermediateFrobeniusTwistFieldRationalPlaceCount_eq_rationalBase (C : Type u_2) (S : Type u_3) (N : Type u_4) [Field C] [Fintype C] [DecidableEq C] [Field S] [DecidableEq (RatFunc C)] [Field N] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [IsGalois (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (L : Type u_5) [Field L] [Algebra (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] (g : Gal(N/L)) : intermediateFrobeniusTwistFieldRationalPlaceCount C S N hExact L g = frobeniusTwistFieldRationalPlaceCount C S N hExact (AlgEquiv.restrictScalars (RatFunc C) g)

The complete point count of an intermediate-base twist agrees with that of its rational-base incarnation.

theorem BGS.HasseWeil.abs_intermediateBaseRationalPlaceError_le_squareField_of_genus_exact (K : Type u_1) (C : Type u_2) (S : Type u_3) (N : Type u_4) [Field K] [Fintype K] [Field C] [Fintype C] [DecidableEq C] [Algebra K C] [Field S] [Finite S] [DecidableEq (RatFunc C)] [Field N] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [IsGalois (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (L : Type u_5) [Field L] [Algebra (RatFunc C) L] [FiniteDimensional (RatFunc C) L] [Algebra.IsSeparable (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] [FiniteDimensional L N] [IsGalois L N] (hcard : Fintype.card C = Fintype.card K ^ 2) (hExact : algebraicClosure C N = ⊥) (hdivL : Nat.card Gal(N/L) ∣ Module.finrank C S) (hdivBase : 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) : |↑(finiteExtensionRationalPlaceCount C L) - ↑(Nat.card C) - 1| ≤ 2 * ↑(Module.finrank (RatFunc C) N) ^ 2 + ↑(Nat.card Gal(N/L)) * (↑(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))

The complete twist average and the pointwise Stepanov estimate give a two-sided rational-place bound for the fixed intermediate field.

theorem BGS.HasseWeil.abs_intermediateBaseRationalPlaceError_le_squareField_of_genus (K : Type u_1) (C : Type u_2) (S : Type u_3) (N : Type u_4) [Field K] [Fintype K] [Field C] [Fintype C] [DecidableEq C] [Algebra K C] [Field S] [Finite S] [DecidableEq (RatFunc C)] [Field N] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [IsGalois (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (L : Type u_5) [Field L] [Algebra (RatFunc C) L] [FiniteDimensional (RatFunc C) L] [Algebra.IsSeparable (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] [FiniteDimensional L N] [IsGalois L N] (hcard : Fintype.card C = Fintype.card K ^ 2) (hExact : algebraicClosure C N = ⊥) (hdivL : Nat.card Gal(N/L) ∣ Module.finrank C S) (hdivBase : 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) : |↑(finiteExtensionRationalPlaceCount C L) - ↑(Nat.card C) - 1| ≤ 2 * ↑(Module.finrank (RatFunc C) N) ^ 2 + 2 * ↑(Module.finrank (RatFunc C) N) ^ 3 + ↑(Module.finrank (RatFunc C) N) ^ 2 * ↑((2 * MarkoffRiemannRoch.FunctionField.genus C N + 1) * Fintype.card K)

A degree-only version of the fixed-tower estimate. Both Galois-group orders in the exact bound are at most the degree of the top field over C(X); this deliberately looser polynomial bound is the form used by the normal-closure argument.