GaloisCoinsertionIntermediateFieldSubgroup

English

Another formulation of the Galois coinsertion between FGIFs and closed subgroups via OrderDual.

Русский

Другая формулировка Galois коинсерции между FGIF и замкнутыми подгруппами через OrderDual.

LaTeX

$$$ \text{Coinsertion}(\text{OrderDual}...) $$$

Lean4

/-- The Galois correspondence as a `GaloisCoinsertion` -/
def GaloisCoinsertionIntermediateFieldSubgroup [IsGalois k K] :
    GaloisCoinsertion (OrderDual.toDual ∘ fun (E : IntermediateField k K) ↦ E.fixingSubgroup)
      ((fun (H : Subgroup (K ≃ₐ[k] K)) ↦ IntermediateField.fixedField H) ∘ OrderDual.toDual)
    where
  choice H _ := IntermediateField.fixedField H
  gc E H := (IntermediateField.le_iff_le H E).symm
  u_l_le K := le_of_eq (fixedField_fixingSubgroup K)
  choice_eq _ _ := rfl

Похожие утверждения