English
For a finite-dimensional extension E/F, the following are equivalent: (i) E/F is Galois; (ii) the fixed field of Aut_F(E) is F; (iii) |Aut_F(E)| = [E:F]; (iv) there exists a separable polynomial p with E as a splitting field over F.
Русский
Для конечномерного расширения E/F следующие условия эквивалентны: (i) E/F галуа; (ii) фиксированное поле Aut_F(E) равно F; (iii) |Aut_F(E)| = [E:F]; (iv) существует разделимый многочлен p, такой что E является разложением p над F.
LaTeX
$$$\text{IsGalois}(F,E) \iff \operatorname{FixedField}(\operatorname{Aut}_F(E)) = F \iff |\operatorname{Aut}_F(E)| = [E:F] \iff \exists p\in F[X], p.Separable \wedge p.IsSplittingField F E$$$
Lean4
/-- Equivalent characterizations of a Galois extension of finite degree. -/
theorem tfae [FiniteDimensional F E] :
List.TFAE
[IsGalois F E, IntermediateField.fixedField (⊤ : Subgroup (E ≃ₐ[F] E)) = ⊥, Nat.card (E ≃ₐ[F] E) = finrank F E,
∃ p : F[X], p.Separable ∧ p.IsSplittingField F E] :=
by
tfae_have 1 → 2 := fun h ↦ OrderIso.map_bot (@intermediateFieldEquivSubgroup F _ E _ _ _ h).symm
tfae_have 1 → 3 := fun _ ↦ card_aut_eq_finrank F E
tfae_have 1 → 4 := fun _ ↦ is_separable_splitting_field F E
tfae_have 2 → 1 := of_fixedField_eq_bot F E
tfae_have 3 → 1 := of_card_aut_eq_finrank F E
tfae_have 4 → 1 := fun ⟨h, hp1, _⟩ ↦ of_separable_splitting_field hp1
tfae_finish
