Complete rational-place averaging over an intermediate base

The finite-place average over Gal(N/L) is exact. Complete rational-place counts differ from it only at infinity, and both the twists and L have at most the original degree [N : C(X)] rational infinity places. This gives a uniform aggregate error independent of the auxiliary constant extension.

@[instance_reducible]

noncomputable def BGS.HasseWeil.intermediateRationalAverageBaseConstantAlgebra (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 intermediate frobenius twist rational place average construction.

Equations

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

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

@[instance_reducible]

noncomputable def BGS.HasseWeil.intermediateRationalAverageConstantAlgebra (C : Type u_1) [Field C] (L : Type u_4) [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 rational place average construction.

Equations

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

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

noncomputable def BGS.HasseWeil.intermediateFrobeniusTwistFieldRationalInfinityPlaceCount (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 = ⊥) (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] (g : Gal(N/L)) : ℕ

The rational infinity-place count of one intermediate-base twist.

Equations

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

noncomputable def BGS.HasseWeil.intermediateFrobeniusTwistFieldRationalPlaceCount (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 = ⊥) (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] (g : Gal(N/L)) : ℕ

The complete rational-place count of one intermediate-base twist, split into finite and infinity parts.

Equations

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

theorem BGS.HasseWeil.intermediateFrobeniusTwistFieldRationalPlaceCount_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 = ⊥) (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] (g : Gal(N/L)) : have T := ExactConstantExtension C N S; let F := exactConstantExtensionFrobeniusTwistField C L N S hExact g; intermediateFrobeniusTwistFieldRationalPlaceCount C S N hExact L g = finiteExtensionRationalPlaceCount C ↥F

The split definition is the actual complete rational-place count.

theorem BGS.HasseWeil.intermediateFrobeniusTwistFieldRationalInfinityPlaceCount_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 = ⊥) (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] [FiniteDimensional L N] (hdivL : Nat.card Gal(N/L) ∣ Module.finrank C S) (g : Gal(N/L)) : intermediateFrobeniusTwistFieldRationalInfinityPlaceCount C S N hExact L g ≤ Module.finrank (RatFunc C) N

Each intermediate twist has at most [N : C(X)] rational infinity places, provided its intermediate Galois order divides the constant degree.

theorem BGS.HasseWeil.intermediateBaseRationalInfinityPlaceCount_le_original_finrank (C : Type u_1) (N : Type u_3) [Field C] [Field N] [DecidableEq C] [DecidableEq (RatFunc C)] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [IsGalois (RatFunc C) N] (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [FiniteDimensional (RatFunc C) L] [Algebra.IsSeparable (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] : Nat.card (FiniteExtensionRationalInfinityPlace C L) ≤ Module.finrank (RatFunc C) N

Rational infinity places of the intermediate field itself are bounded by the original degree.

theorem BGS.HasseWeil.sum_intermediateFrobeniusTwistFieldRationalInfinityPlaceCount_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 = ⊥) (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] [FiniteDimensional L N] (hdivL : Nat.card Gal(N/L) ∣ Module.finrank C S) : ∑ g : Gal(N/L), intermediateFrobeniusTwistFieldRationalInfinityPlaceCount C S N hExact L g ≤ Nat.card Gal(N/L) * Module.finrank (RatFunc C) N

The total infinity contribution of the twists is bounded by the group order times the original degree.

theorem BGS.HasseWeil.sum_intermediateFrobeniusTwistFieldRationalPlaceCount_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 = ⊥) (L : Type u_4) [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] (hdivL : Nat.card Gal(N/L) ∣ Module.finrank C S) : ∑ g : Gal(N/L), intermediateFrobeniusTwistFieldRationalPlaceCount C S N hExact L g = Nat.card Gal(N/L) * Nat.card (FiniteExtensionRationalFinitePlace C L) + ∑ g : Gal(N/L), intermediateFrobeniusTwistFieldRationalInfinityPlaceCount C S N hExact L g

Exact finite-plus-infinity aggregate identity over Gal(N/L).

theorem BGS.HasseWeil.abs_sum_intermediateFrobeniusTwistFieldRationalPlaceCount_sub_card_mul_base_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 = ⊥) (L : Type u_4) [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] (hdivL : Nat.card Gal(N/L) ∣ Module.finrank C S) : |∑ g : Gal(N/L), ↑(intermediateFrobeniusTwistFieldRationalPlaceCount C S N hExact L g) - ↑(Nat.card Gal(N/L)) * ↑(finiteExtensionRationalPlaceCount C L)| ≤ 2 * ↑(Module.finrank (RatFunc C) N) ^ 2

The complete rational-place aggregate is uniformly close to the group order times the complete rational-place count of L.