comap_map_eq_self — Mathlib

English

If ker f ≤ H, then comap f (map f H) = H; i.e., pulling back the image of H along f recovers H when H contains the kernel.

Русский

Если ядро f ⊆ H, то обратный образ образа H по f равен H; восстанавливается исходная подгруппа.

LaTeX

$$$\\ker(f) \\le H \\Rightarrow \\operatorname{comap}_f(\\operatorname{map}_f H) = H$$$

Lean4

@[to_additive]
theorem comap_map_eq_self {f : G →* N} {H : Subgroup G} (h : f.ker ≤ H) : comap f (map f H) = H := by
  rwa [comap_map_eq, sup_eq_left]

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