Genus of Frobenius-twist fixed fields

Extending the constants of a Frobenius-twist fixed field gives the common exact constant extension. Genus invariance under exact extension of finite constants therefore identifies the genus of every twist with the genus of the original function field. This is Proposition 5.2.8(b) in the form used by the uniform Stepanov estimate.

@[instance_reducible]

noncomputable def BGS.HasseWeil.twistGenusBaseConstantAlgebra (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 genus construction.

Equations

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

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

theorem BGS.HasseWeil.genus_frobeniusTwistField_eq_original (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Finite S] [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)) : have T := ExactConstantExtension C N S; let F := exactConstantExtensionFrobeniusTwistField C (RatFunc C) N S hExact g; MarkoffRiemannRoch.FunctionField.genus C ↥F = MarkoffRiemannRoch.FunctionField.genus C N

Every canonical Frobenius-twist fixed field has the genus of the original exact-constant Galois function field. The equality is independent of the auxiliary constant extension.