Degrees of exact-constant Frobenius twists

For an exact constant extension S \otimes[C] N, every Frobenius-twist fixed field has the same degree over C(X) as the original function field N. This file records the rational-function specialization used by the Hasse--Weil averaging argument and combines it with the general bound on rational places above infinity.

theorem BGS.HasseWeil.finrank_frobeniusTwistField_over_ratFunc_eq_original (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] [Finite S] (hExact : algebraicClosure C N = ⊥) (g : Gal(N/RatFunc C)) (hdiv : Nat.card Gal(N/RatFunc C) ∣ Module.finrank C S) : Module.finrank (RatFunc C) ↥(exactConstantExtensionFrobeniusTwistField C (RatFunc C) N S hExact g) = Module.finrank (RatFunc C) N

A Frobenius-twist fixed field has the same C(X)-degree as the original function field.

theorem BGS.HasseWeil.rationalInfinityPlace_card_frobeniusTwistField_le_original_finrank (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 = ⊥) (g : Gal(N/RatFunc C)) (hdiv : Nat.card Gal(N/RatFunc C) ∣ Module.finrank C S) : let F := exactConstantExtensionFrobeniusTwistField C (RatFunc C) N S hExact g; Nat.card (FiniteExtensionRationalInfinityPlace C ↥F) ≤ Module.finrank (RatFunc C) N

The number of rational infinity places on a Frobenius-twist fixed field is bounded uniformly by the degree of the original function field.