English
There is a Galois correspondence between intermediate fields of E/F and subgroups of Aut_F(E), reversing inclusions.
Русский
Существует Галуа–соответствие между промежуточными полями E/F и подгруппами Aut_F(E), сохраняющее против включений.
LaTeX
$$$\text{intermediateFieldEquivSubgroup} : \operatorname{IntField}(E/F) \simeq_o (\operatorname{Subgroup}(\operatorname{Aut}_F(E)))^{\mathrm{op}}$$$
Lean4
/-- The Galois correspondence from intermediate fields to subgroups. -/
@[stacks 09DW]
def intermediateFieldEquivSubgroup [FiniteDimensional F E] [IsGalois F E] :
IntermediateField F E ≃o (Subgroup (E ≃ₐ[F] E))ᵒᵈ
where
toFun := IntermediateField.fixingSubgroup
invFun := IntermediateField.fixedField
left_inv K := fixedField_fixingSubgroup K
right_inv H := IntermediateField.fixingSubgroup_fixedField H
map_rel_iff'
{K L} := by
rw [← fixedField_fixingSubgroup L, IntermediateField.le_iff_le, fixedField_fixingSubgroup L]
rfl
