English
The Galois correspondence between intermediate fields and closed subgroups forms a Galois insertion between the dual of intermediate fields and closed-subgroups.
Русский
Галоисово соответствие между промежуточными полями и замкнутыми подгруппами образует Galois-вставку между двойственным комплексом промежуточных полей и замкнутыми подгруппами.
LaTeX
$$$ \text{GaloisInsertion} : \text{IntermediateField}(k,K)^{op} \to \text{ClosedSubgroup}(K\simeq_K K) $ (with suitable dualities) $$$
Lean4
/-- The Galois correspondence from intermediate fields to closed subgroups. -/
def IntermediateFieldEquivClosedSubgroup [IsGalois k K] : IntermediateField k K ≃o (ClosedSubgroup (K ≃ₐ[k] K))ᵒᵈ
where
toFun L := ⟨L.fixingSubgroup, fixingSubgroup_isClosed L⟩
invFun H := IntermediateField.fixedField H.1
left_inv L := fixedField_fixingSubgroup L
right_inv
H := by
simp_rw [fixingSubgroup_fixedField H]
rfl
map_rel_iff'
{K L} := by
rw [← fixedField_fixingSubgroup L, IntermediateField.le_iff_le, fixedField_fixingSubgroup L]
rfl
