comap_le_comap_of_le_range — Mathlib

English

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

Русский

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

LaTeX

$$$K \\le f(G) \\Rightarrow \\bigl(f^{-1}(K) \\le f^{-1}(L) \\iff K \\le L\\bigr)$$$

Lean4

@[to_additive]
theorem comap_le_comap_of_le_range {f : G →* N} {K L : Subgroup N} (hf : K ≤ f.range) : K.comap f ≤ L.comap f ↔ K ≤ L :=
  ⟨(map_comap_eq_self hf).ge.trans ∘ map_le_iff_le_comap.mpr, comap_mono⟩

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