ker_map — Mathlib

English

The kernel of the induced map map equals the image of ker f under mk'.

Русский

Ядро индуцированного отображения map равно образу ядра f под mk'.

LaTeX

$$$\\ker(\\text{map } N\\; M\\; f\\; h) = \\operatorname{map}(\\mathrm{mk}' N)(\\ker f).$$$

Lean4

@[to_additive]
theorem ker_map (M : Subgroup H) [M.Normal] (f : G →* H) (h : N ≤ Subgroup.comap f M) :
    (map N M f h).ker = Subgroup.map (mk' N) (M.comap f) :=
  by
  simp_rw [← ker_mk' M, MonoidHom.comap_ker]
  exact QuotientGroup.ker_lift _ _ _

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