comap_le_comap_of_surjective — Mathlib

English

Let f: G → N be a surjective group homomorphism and K,L ≤ N be subgroups. Then f^{-1}(K) ≤ f^{-1}(L) if and only if K ≤ L.

Русский

Пусть f: G → N — сюръективный гомоморфизм групп, и K,L ≤ N — подгруппы. Тогда f^{-1}(K) ≤ f^{-1}(L) эквивалентно K ≤ L.

LaTeX

$$$\\text{Surj}(f) \\Rightarrow (K \\le f(G) \\implies f^{-1}(K) \\le f^{-1}(L) \\iff K \\le L)$.$$

Lean4

@[to_additive]
theorem comap_le_comap_of_surjective {f : G →* N} {K L : Subgroup N} (hf : Function.Surjective f) :
    K.comap f ≤ L.comap f ↔ K ≤ L :=
  comap_le_comap_of_le_range (range_eq_top.2 hf ▸ le_top)

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