Complete rational-place averaging for Frobenius twists

The finite-place Frobenius average is exact, including above ramified base places. Passing from finite rational places to the complete rational-place count therefore introduces only the places above infinity. Their number on each twist is bounded by the degree of the original function field, uniformly in the auxiliary constant extension.

This file records both the exact aggregate identity and the resulting uniform bound for the centered aggregate error. No branch-locus estimate is needed at this boundary.

@[instance_reducible]

noncomputable def BGS.HasseWeil.rationalPlaceAverageBaseConstantAlgebra (C : Type u_1) (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 rational place average construction.

Equations

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

theorem BGS.HasseWeil.rationalPlaceAverageBaseConstantTower (C : Type u_1) (N : Type u_3) [Field C] [Field N] [Algebra (RatFunc C) N] : IsScalarTower C (RatFunc C) N

noncomputable def BGS.HasseWeil.frobeniusTwistFieldRationalInfinityPlaceCount (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [DecidableEq C] [DecidableEq (RatFunc C)] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (g : Gal(N/RatFunc C)) : ℕ

The number of rational places above infinity on one Frobenius-twist field.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BGS.HasseWeil.frobeniusTwistFieldRationalPlaceCount (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [DecidableEq C] [DecidableEq (RatFunc C)] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (g : Gal(N/RatFunc C)) : ℕ

The complete rational-place count of one Frobenius-twist field, split into its finite and infinity parts.

Equations

• One or more equations did not get rendered due to their size.

theorem BGS.HasseWeil.frobeniusTwistFieldRationalPlaceCount_eq_finiteExtensionRationalPlaceCount (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [DecidableEq C] [DecidableEq (RatFunc C)] [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 = ⊥) (g : Gal(N/RatFunc C)) : have T := ExactConstantExtension C N S; let F := exactConstantExtensionFrobeniusTwistField C (RatFunc C) N S hExact g; frobeniusTwistFieldRationalPlaceCount C S N hExact g = finiteExtensionRationalPlaceCount C ↥F

The split definition is the actual complete degree-one place count of the twist field.

theorem BGS.HasseWeil.frobeniusTwistFieldRationalInfinityPlaceCount_le_original_finrank (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Finite S] [DecidableEq C] [DecidableEq (RatFunc C)] [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 = ⊥) (g : Gal(N/RatFunc C)) (hdiv : Nat.card Gal(N/RatFunc C) ∣ Module.finrank C S) : frobeniusTwistFieldRationalInfinityPlaceCount C S N hExact g ≤ Module.finrank (RatFunc C) N

The infinity contribution of each twist is bounded by the degree of the original function field, independently of the auxiliary constant extension.

theorem BGS.HasseWeil.sum_frobeniusTwistFieldRationalInfinityPlaceCount_le (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Finite S] [DecidableEq C] [DecidableEq (RatFunc C)] [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 = ⊥) (hdiv : Nat.card Gal(N/RatFunc C) ∣ Module.finrank C S) : ∑ g : Gal(N/RatFunc C), frobeniusTwistFieldRationalInfinityPlaceCount C S N hExact g ≤ Nat.card Gal(N/RatFunc C) * Module.finrank (RatFunc C) N

The total infinity contribution of all twists is uniformly bounded by the Galois-group order times the original function-field degree.

theorem BGS.HasseWeil.sum_frobeniusTwistFieldRationalPlaceCount_eq (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Finite S] [DecidableEq C] [DecidableEq (RatFunc C)] [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 = ⊥) (hdiv : Nat.card Gal(N/RatFunc C) ∣ Module.finrank C S) : ∑ g : Gal(N/RatFunc C), frobeniusTwistFieldRationalPlaceCount C S N hExact g = Nat.card Gal(N/RatFunc C) * Nat.card C + ∑ g : Gal(N/RatFunc C), frobeniusTwistFieldRationalInfinityPlaceCount C S N hExact g

Exact finite-plus-infinity aggregate identity. All finite rational places contribute exactly |Gal(N/C(X))| * |C|; the displayed infinity sum is the entire correction to the complete rational-place count.

theorem BGS.HasseWeil.sum_frobeniusTwistFieldRationalPlaceError_eq (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Finite S] [DecidableEq C] [DecidableEq (RatFunc C)] [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 = ⊥) (hdiv : Nat.card Gal(N/RatFunc C) ∣ Module.finrank C S) : ∑ g : Gal(N/RatFunc C), (↑(frobeniusTwistFieldRationalPlaceCount C S N hExact g) - ↑(Nat.card C) - 1) = ∑ g : Gal(N/RatFunc C), ↑(frobeniusTwistFieldRationalInfinityPlaceCount C S N hExact g) - ↑(Nat.card Gal(N/RatFunc C))

Exact centered aggregate-error identity over the reals. It makes explicit that the complete-place error is the infinity contribution minus one point for each twist.

theorem BGS.HasseWeil.abs_sum_frobeniusTwistFieldRationalPlaceError_le (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Finite S] [DecidableEq C] [DecidableEq (RatFunc C)] [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 = ⊥) (hdiv : Nat.card Gal(N/RatFunc C) ∣ Module.finrank C S) : |∑ 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)

The centered aggregate error is bounded uniformly in the auxiliary constant extension. The sharper factor finrank, rather than finrank + 1, follows because the original function-field degree is positive.