English
If N is a normal subgroup and H is a commutative subgroup with N ⊔ H = ⊤, then the commutator of G is contained in N.
Русский
Если N — нормальная подгруппа, а H — коммутативная подгруппа и N ⊔ H = ⊤, то коммутатор G ≤ N.
LaTeX
$$$ _root_.commutator G \\le N $ given the conditions$$
Lean4
/-- If `N` is a normal subgroup of `G` and `H` a commutative subgroup such that `H ⊔ N = ⊤`,
then `N` contains `commutator G`. -/
theorem commutator_le_of_self_sup_commutative_eq_top {N : Subgroup G} [N.Normal] {H : Subgroup G} (hHN : N ⊔ H = ⊤)
(hH : IsMulCommutative H) : _root_.commutator G ≤ N := by
-- It is enough to prove that Q = G ⧸ N is commutative
rw [← quotient_commutative_iff_commutator_le]
-- Q is a quotient of H
let φ : H →ₙ* G ⧸ N :=
MonoidHom.comp (QuotientGroup.mk' N)
(Subgroup.subtype H)
-- It is enough to prove that φ is surjective
apply Function.Surjective.mul_comm (f := φ) _ hH.is_comm
rw [MulHom.coe_coe, ← MonoidHom.range_eq_top]
-- We have to prove that `MonoidHom.range φ = ⊤`
simp only [MonoidHom.range_eq_map, ← Subgroup.map_map]
have : Subgroup.map (QuotientGroup.mk' N) ⊤ = ⊤ :=
by
rw [← MonoidHom.range_eq_map, MonoidHom.range_eq_top]
exact QuotientGroup.mk'_surjective N
simp only [← this, Subgroup.map_eq_map_iff, QuotientGroup.ker_mk', sup_comm, ← hHN]
simp [← MonoidHom.range_eq_map]
