A common Riemann budget for Frobenius-twist fields

For a fixed finite constant extension S / C, there are only finitely many Frobenius-twist fields attached to the elements of Gal(N / C(X)). The primitive-element Riemann inequality supplies a finite-place budget for each twist. Summing these finitely many budgets gives one budget which works for every twist field simultaneously.

This file also records that the same twist fields have exact constant field C, so the common budget and the constant-field input needed by the intrinsic Stepanov estimate are available at the same boundary.

theorem BGS.HasseWeil.finiteDimensional_frobeniusTwistField_over_ratFunc (C : Type u_1) (N : Type u_2) (S : Type u_3) [Field C] [Fintype C] [Field N] [Algebra (RatFunc C) N] [Algebra C N] [IsScalarTower C (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Field S] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (g : Gal(N/RatFunc C)) : let F := exactConstantExtensionFrobeniusTwistField C (RatFunc C) N S hExact g; FiniteDimensional (RatFunc C) ↥F

A twist fixed field is finite-dimensional over the rational-function base because it embeds into the finite exact constant extension.

theorem BGS.HasseWeil.isSeparable_frobeniusTwistField_over_ratFunc (C : Type u_1) (N : Type u_2) (S : Type u_3) [Field C] [Fintype C] [Field N] [Algebra (RatFunc C) N] [Algebra C N] [IsScalarTower C (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [Field S] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (g : Gal(N/RatFunc C)) : let F := exactConstantExtensionFrobeniusTwistField C (RatFunc C) N S hExact g; Algebra.IsSeparable (RatFunc C) ↥F

Separability descends from the finite separable exact constant extension to each intermediate twist fixed field.

theorem BGS.HasseWeil.exists_common_frobeniusTwistField_finitePlace_riemann_lower_budget (C : Type u_1) (N : Type u_2) (S : Type u_3) [Field C] [Fintype C] [DecidableEq C] [DecidableEq (RatFunc C)] [Field N] [Algebra (RatFunc C) N] [Algebra C N] [IsScalarTower C (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [Field S] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) : ∃ (budget : ℕ), ∀ (g : Gal(N/RatFunc C)), let F := exactConstantExtensionFrobeniusTwistField C (RatFunc C) N S hExact g; ∀ (q : CorvajaZannier.FiniteExtensionFinitePlace C ↥F) (poleOrder : ℕ), poleOrder * CorvajaZannier.finiteExtensionPlaceDegree C (↥F) (Sum.inl q) + 1 ≤ Module.finrank C ↥(CorvajaZannier.finiteExtensionOnePointRiemannSpace C (↥F) (Sum.inl q) poleOrder) + budget

For one fixed finite extension of the constants, a single natural-number budget works for the finite-place Riemann inequality in every Frobenius-twist field.

theorem BGS.HasseWeil.exists_common_frobeniusTwistField_exactConstants_and_riemann_budget (C : Type u_1) (N : Type u_2) (S : Type u_3) [Field C] [Fintype C] [DecidableEq C] [DecidableEq (RatFunc C)] [Field N] [Algebra (RatFunc C) N] [Algebra C N] [IsScalarTower C (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] (hExact : algebraicClosure C N = ⊥) : ∃ (budget : ℕ), ∀ (g : Gal(N/RatFunc C)), let F := exactConstantExtensionFrobeniusTwistField C (RatFunc C) N S hExact g; algebraicClosure C ↥F = ⊥ ∧ ∀ (q : CorvajaZannier.FiniteExtensionFinitePlace C ↥F) (poleOrder : ℕ), poleOrder * CorvajaZannier.finiteExtensionPlaceDegree C (↥F) (Sum.inl q) + 1 ≤ Module.finrank C ↥(CorvajaZannier.finiteExtensionOnePointRiemannSpace C (↥F) (Sum.inl q) poleOrder) + budget

The common Riemann budget can be chosen simultaneously with the statement that every Frobenius-twist field has exact constant field C.