restrictNormalHom_ker — Mathlib

English

For E an intermediate field of K⊂L with a normal extension, the kernel of restrictNormalHom equals the fixedField subgroup.

Русский

Пусть E — промежуточное поле K⊂L с нормальным расширением; ядро restrictNormalHom равно fixingSubgroup.

LaTeX

$$$\ker(\text{restrictNormalHom}(E)) = E.\text{fixingSubgroup}$$$

Lean4

theorem restrictNormalHom_ker (E : IntermediateField K L) [Normal K E] : (restrictNormalHom E).ker = E.fixingSubgroup :=
  by
  simp only [Subgroup.ext_iff, MonoidHom.mem_ker, AlgEquiv.ext_iff, one_apply, Subtype.ext_iff, restrictNormalHom_apply,
    Subtype.forall, mem_fixingSubgroup_iff, implies_true]

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