English
For a normal subgroup N of G, the quotient G/N is commutative if and only if the commutator G is contained in N.
Русский
Для нормальной подгруппы N группы G, фактор-группа G/N коммутативна тогда и только тогда, когда коммутатор G ≤ N.
LaTeX
$$$ \\text{Std.Commutative} (\\cdot * \\cdot : G \\!/N \\to _ \\to _) \\iff [G,G] \\le N $$$
Lean4
theorem quotient_commutative_iff_commutator_le {N : Subgroup G} [N.Normal] :
Std.Commutative (· * · : G ⧸ N → _ → _) ↔ _root_.commutator G ≤ N :=
by
constructor
· intro hcomm
rw [commutator_eq_normalClosure]
rw [← Subgroup.normalClosure_subset_iff]
rintro x ⟨p, q, rfl⟩
rw [SetLike.mem_coe, ← QuotientGroup.eq_one_iff, commutatorElement_def]
simp only [QuotientGroup.mk_mul, QuotientGroup.mk_inv]
simp only [← commutatorElement_def, commutatorElement_eq_one_iff_mul_comm]
apply hcomm.comm
· intro hGN
apply Std.Commutative.mk
rintro x'; obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective N x'
intro y'; obtain ⟨y, rfl⟩ := QuotientGroup.mk'_surjective N y'
rw [← commutatorElement_eq_one_iff_mul_comm, ← map_commutatorElement, QuotientGroup.mk'_apply,
QuotientGroup.eq_one_iff]
apply hGN
rw [commutator_eq_closure]
exact Subgroup.subset_closure (commutator_mem_commutatorSet x y)
