map_surjective_of_surjective — Mathlib

English

If φ is surjective (mod the quotient) and N ≤ ker φ, then the induced map map N M f h is surjective.

Русский

Если φ сюръективна (с учётом фактор-группы) и N ≤ ker φ, то индуцированное отображение map N M f h сюръективно.

LaTeX

$$$\\text{Surj}(\\varphi) \\Rightarrow \\text{Surj}(\\text{map } N\\; M\\; f\\; h).$$$

Lean4

@[to_additive]
theorem map_surjective_of_surjective (M : Subgroup H) [M.Normal] (f : G →* H)
    (hf : Function.Surjective (mk ∘ f : G → H ⧸ M)) (h : N ≤ M.comap f) : Function.Surjective (map N M f h) :=
  lift_surjective_of_surjective _ _ hf _

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