GaloisInsertionIntermediateFieldClosedSubgroup

English

There is a Galois coinsertion between OrderDual ∘ (E ↦ E.fixingSubgroup) and the corresponding fixed-field map; i.e., the left and right adjoints establish an optimal correspondence.

Русский

Существует Galois-коинсерция между двумя отображениями: промежуточные поля ↦ их фиксирующие подгруппы и обратно; они образуют оптимальную корреспонденцию.

LaTeX

$$$ \text{GaloisCoinsertionIntermediateFieldSubgroup} : \text{(order dual)} \to \text{FixedField} \text{ correspondence} $$$

Lean4

/-- The Galois correspondence as a `GaloisInsertion` -/
def GaloisInsertionIntermediateFieldClosedSubgroup [IsGalois k K] :
    GaloisInsertion
      (OrderDual.toDual ∘ fun (E : IntermediateField k K) ↦
        (⟨E.fixingSubgroup, fixingSubgroup_isClosed E⟩ : ClosedSubgroup (K ≃ₐ[k] K)))
      ((fun (H : ClosedSubgroup (K ≃ₐ[k] K)) ↦ IntermediateField.fixedField H) ∘ OrderDual.toDual) :=
  OrderIso.toGaloisInsertion IntermediateFieldEquivClosedSubgroup

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