of_fixedField_normal_subgroup — Mathlib

English

A collection of simplification lemmas about kernels of restricting maps.

Русский

Серия вспомогательных лемм про ядра ограничивающих отображений.

LaTeX

$$restrictNormalHom_ker_simp$$

Lean4

/-- If `H` is a normal Subgroup of `Gal(L / K)`, then `fixedField H` is Galois over `K`. -/
instance of_fixedField_normal_subgroup [IsGalois K L] (H : Subgroup (L ≃ₐ[K] L)) [hn : Subgroup.Normal H] :
    IsGalois K (fixedField H)
    where
  to_isSeparable := Algebra.isSeparable_tower_bot_of_isSeparable K (fixedField H) L
  to_normal := by
    apply normal_iff_forall_map_le'.mpr
    rintro σ x ⟨a, ha, rfl⟩ τ
    exact (symm_apply_eq σ).mp (ha ⟨σ⁻¹ * τ * σ, Subgroup.Normal.conj_mem' hn τ.1 τ.2 σ⟩)

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