Exact constants of Frobenius-twist fields

Let T = S ⊗[C] N be an exact finite constant extension and let F_g be the fixed field of the cyclic group generated by (Frob, g). This file proves that C is the exact constant field of every F_g.

Indeed, an element of F_g algebraic over C is algebraic over S in T, so exactness of the constants of T puts it in the embedded copy of S. Since the element is fixed by (Frob, g), its representative in S is fixed by Frobenius and hence belongs to C.

The order calculation for (Frob, g) is not needed for this descent, so the result is stronger than the version with the usual divisibility hypothesis.

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

Every Frobenius-twist fixed field has exact constant field C.

No divisibility condition on the order of Gal(N/L) is required: only the restriction of the twist generator to S, which is the C-Frobenius, enters the proof.