English
The commutator of the centralizers of the commutator set is contained in the center: [C_G(C_G(Comm(G))), C_G(Comm(G))] ≤ Z(G).
Русский
Коммутатор центральизаторов множества коммутаторов содержится в центре: [C_G(Comm(G)), C_G(Comm(G))] ≤ Z(G).
LaTeX
$$$ [C_G(\\operatorname{commutator}(G)), C_G(\\operatorname{commutator}(G))] \\le Z(G) $$$
Lean4
theorem commutator_centralizer_commutator_le_center :
⁅centralizer (commutator G : Set G), centralizer (commutator G)⁆ ≤ Subgroup.center G :=
by
rw [← Subgroup.centralizer_univ, ← Subgroup.coe_top, ← Subgroup.commutator_eq_bot_iff_le_centralizer]
suffices ⁅⁅⊤, centralizer (commutator G : Set G)⁆, centralizer (commutator G : Set G)⁆ = ⊥
by
refine Subgroup.commutator_commutator_eq_bot_of_rotate ?_ this
rwa [Subgroup.commutator_comm (centralizer (commutator G : Set G))]
rw [Subgroup.commutator_comm, Subgroup.commutator_eq_bot_iff_le_centralizer]
exact Set.centralizer_subset (Subgroup.commutator_mono le_top le_top)
