The fixed field of the automorphism group of a normal extension

For a normal extension E / F, the fixed field E ^ Aut(E/F) sits between F and E with F ⊆ E ^ Aut(E/F) purely inseparable and E ^ Aut(E/F) ⊆ E Galois. This is the splitting of Stacks, Fields, Lemma 9.27.3(2), whose proof reads "We set E_insep = E^{Aut(E/F)}. Details omitted." Mathlib has the Galois half as IsGalois.of_fixed_field; the purely inseparable half is new here. The two are stated separately, one conclusion each.

Order matters for the consumer (TauCeti.IsIntegralClosure.finite_of_forall_isPurelyInseparable): the purely inseparable step has to sit below the separable one, because the integral closure of a polynomial ring in a separable extension is no longer a polynomial ring.

Main results

• TauCeti.IntermediateField.isPurelyInseparable_fixedField_top: for E / F normal, the fixed field of Gal(E/F) is purely inseparable over F.

Provenance

The mathematics is Stacks, Fields, Lemma 9.27.3(2) (tag 030M), the splitting used by Stacks 10.161.12 (tag 032N) in its normalization-finiteness argument.

theorem TauCeti.IntermediateField.isPurelyInseparable_fixedField_top (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] [Normal F E] : IsPurelyInseparable F ↥(IntermediateField.fixedField ⊤)

Source: Stacks, Fields, Lemma 9.27.3(2): "F ⊂ E_insep is purely inseparable", with E_insep = E^{Aut(E/F)} (proof: "Details omitted"). For a normal extension E / F, the fixed field of the full automorphism group is purely inseparable over F: an element fixed by every automorphism has a single conjugate, since minpoly F x splits in E and its roots form one orbit.