fixingSubgroup_normal_of_isGalois

English

The fixingSubgroup after mapping equals the image under the map of the original fixingSubgroup.

Русский

После отображения фиксационная подгруппа равна изображению исходной подгруппы фиксации.

LaTeX

$$$\text{map fixingSubgroup}(E) = \text{image}(\text{fixingSubgroup}(E))$$$

Lean4

/-- Let `E` be an intermediateField of a Galois extension `L / K`. If `E / K` is
Galois extension, then `E.fixingSubgroup` is a normal subgroup of `Gal(L / K)`. -/
instance fixingSubgroup_normal_of_isGalois [IsGalois K L] [IsGalois K E] : E.fixingSubgroup.Normal :=
  by
  apply Subgroup.Normal.of_conjugate_fixed (fun σ ↦ ?_)
  rw [← map_fixingSubgroup, normal_iff_forall_map_eq'.mp inferInstance σ]

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