map_comap_eq_self — Mathlib

English

If f is surjective, then map f (comap f H) = H for any subgroup H of the codomain.

Русский

Если отображение f сюръективно, то map f (comap f H) = H для любой подгруппы H на языке кодоменна.

LaTeX

$$$\text{Surjective}(f) \Rightarrow \operatorname{map}_f(\operatorname{comap}_f H) = H$$$

Lean4

@[to_additive]
theorem map_comap_eq_self {f : G →* N} {H : Subgroup N} (h : H ≤ f.range) : map f (comap f H) = H := by
  rwa [map_comap_eq, inf_eq_right]

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