English
For an intermediate field L in a Galois extension, L.fixingSubgroup is normal iff L is Galois over k.
Русский
Для промежуточного поля L в Галуа-расширении L.fixingSubgroup является нормальной подгруппой тогда и только тогда, когда L является Галуа над k.
LaTeX
$$$ L.fixingSubgroup.Normal \iff IsGalois k L $$$
Lean4
theorem normal_iff_isGalois (L : IntermediateField k K) [IsGalois k K] : L.fixingSubgroup.Normal ↔ IsGalois k L :=
by
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
· let g (x : K) := L.fixingSubgroup.map (restrictNormalHom (adjoin k { x }))
let f (x : L) : IntermediateField k K := IntermediateField.lift <| IntermediateField.fixedField <| g x.1
have (x : K) : (g x).Normal :=
Subgroup.Normal.map h (restrictNormalHom (adjoin k { x })) (restrictNormalHom_surjective K)
have (l : L) : Normal k (f l) :=
Normal.of_algEquiv <| IntermediateField.liftAlgEquiv <| IntermediateField.fixedField (g l.1)
have n : Normal k ↥(⨆ l : L, f l) := IntermediateField.normal_iSup k K f
have : (⨆ l : L, f l) = L := by
apply le_antisymm
· apply iSup_le
intro l
simpa only [f, g, ← restrict_fixedField L.fixingSubgroup (adjoin k { l.1 }), fixedField_fixingSubgroup L] using
inf_le_left
· intro l hl
apply le_iSup f ⟨l, hl⟩
simpa only [f, g, ← restrict_fixedField L.fixingSubgroup (adjoin k { l }), fixedField_fixingSubgroup L,
IntermediateField.mem_inf, hl, true_and] using adjoin_simple_le_iff.mp le_rfl
rw [this] at n
constructor
·
simpa only [IntermediateFieldEquivClosedSubgroup, RelIso.coe_fn_mk, Equiv.coe_fn_mk,
← L.restrictNormalHom_ker] using MonoidHom.normal_ker (restrictNormalHom L)
