Exact constants after a finite constant extension

Let N / C have exact constant field C, and let S / C be a finite Galois extension of finite fields. This file proves that the tensor compositum S ⊗[C] N has exact constant field S.

For an element algebraic over S, adjoin it to C inside the compositum. This finite field is linearly disjoint from N, since its intersection with N is contained in the exact constants C. Its degree over C therefore divides [S : C]. The finite-field embedding criterion supplies an embedding into S; uniqueness of the roots of X ^ #K - X inside the common compositum then shows that the original element already belongs to S.

theorem BGS.HasseWeil.exactConstantExtension_algebraicClosure_eq_bot (C : Type u_1) (N : Type u_2) (S : Type u_3) [Field C] [Field N] [Field S] [Algebra C N] [Algebra C S] [Finite C] [Finite S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) : algebraicClosure S (ExactConstantExtension C N S) = ⊥

A finite Galois extension of the exact finite constant field remains the exact constant field after tensor base change.