feat(group_theory/abelianization): An application of the three subgro…

…ups lemma (#12677)

This PR uses the three subgroups lemma to prove that `⁅(commutator G).centralizer, (commutator G).centralizer⁆ ≤ subgroup.center G`.

src/group_theory/abelianization.lean

@@ -43,6 +43,17 @@ lemma commutator_eq_normal_closure :
   commutator G = subgroup.normal_closure {g | ∃ g₁ g₂ : G, ⁅g₁, g₂⁆ = g} :=
 by simp_rw [commutator, subgroup.commutator_def', subgroup.mem_top, exists_true_left]
 
+lemma commutator_centralizer_commutator_le_center :
+  ⁅(commutator G).centralizer, (commutator G).centralizer⁆ ≤ subgroup.center G :=
+begin
+  rw [←subgroup.centralizer_top, ←subgroup.commutator_eq_bot_iff_le_centralizer],
+  suffices : ⁅⁅⊤, (commutator G).centralizer⁆, (commutator G).centralizer⁆ = ⊥,
+  { refine subgroup.commutator_commutator_eq_bot_of_rotate _ this,
+    rwa subgroup.commutator_comm (commutator G).centralizer },
+  rw [subgroup.commutator_comm, subgroup.commutator_eq_bot_iff_le_centralizer],
+  exact set.centralizer_subset (subgroup.commutator_mono le_top le_top),
+end
+
 /-- The abelianization of G is the quotient of G by its commutator subgroup. -/
 def abelianization : Type u :=
 G ⧸ (commutator G)