ker_lift — Mathlib

English

Same kernel description as ker_lift above; the kernel of the lift equals the image of ker φ under mk'.

Русский

То же описание ядра спуска как и выше; ядро лифта равно образу ядра φ под mk'.

LaTeX

$$$(\\ker(\\hat{\\varphi})) = \\operatorname{map}(\\mathrm{mk}' N)(\\ker \\varphi).$$$

Lean4

@[to_additive]
theorem ker_lift (φ : G →* M) (HN : N ≤ φ.ker) :
    (QuotientGroup.lift N φ HN).ker = Subgroup.map (QuotientGroup.mk' N) φ.ker := by
  rw [← congrArg MonoidHom.ker (lift_comp_mk' N φ HN), ← MonoidHom.comap_ker,
    Subgroup.map_comap_eq_self_of_surjective (mk'_surjective N)]

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