map_commutator_eq — Mathlib

English

For a group homomorphism f: G → H, the image of the commutator subgroup satisfies (commutator G).map f = [f(G), f(G)].

Русский

Для гомоморфизма f: G → H образ коммутаторной подгруппы равен коммутатору образа: (commutator G).map f = [f(G), f(G)].

LaTeX

$$$ (\\operatorname{Subgroup.map} f) (\\operatorname{commutator}(G)) = \\operatorname{Subgroup.commutator.bracket (f.range) (f.range) } $$$

Lean4

theorem map_commutator_eq {H : Type*} [Group H] (f : G →* H) : (commutator G).map f = ⁅f.range, f.range⁆ :=
  by
  rw [_root_.commutator_def, Subgroup.map_commutator]
  apply congr_arg₂ <;>
    · rw [Subgroup.map_eq_range_iff]
      rw [codisjoint_iff, top_sup_eq]

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