subgroupEquivAlgEquiv — Mathlib

English

There is a canonical isomorphism between a subgroup H of Gal(E/F) and the Galois group of the fixed field over F.

Русский

Существует каноническое изоморфизм между подгруппой H Гал(E/F) и Гал(E/FixedField(H)).

LaTeX

$$$H \cong_* E \simeq_{\operatorname{FixedField}(H)} E$$$

Lean4

/-- A subgroup is isomorphic to the Galois group of its fixed field.
-/
def subgroupEquivAlgEquiv [FiniteDimensional F E] (H : Subgroup (E ≃ₐ[F] E)) :
    H ≃* E ≃ₐ[IntermediateField.fixedField H] E :=
  (MulEquiv.subgroupCongr (fixingSubgroup_fixedField H).symm).trans (fixingSubgroupEquiv _)

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