feat(group_theory/group_action/quotient): If G=<S>, then G / Z(G)…

… embeds into `S → {[g₁, g₂]}` (#17151)

In other words, if a finitely generated group has finitely many commutators, then the center has index at most #commutators^rank. This is building up to the theorem that the size of the commutator subgroup is bounded in terms of the number of commutators.

src/group_theory/group_action/conj_act.lean

@@ -184,6 +184,10 @@ begin
   simp [mem_center_iff, smul_def, mul_inv_eq_iff_eq_mul]
 end
 
+lemma stabilizer_eq_centralizer (g : G) : stabilizer (conj_act G) g = (zpowers g).centralizer :=
+le_antisymm (le_centralizer_iff.mp (zpowers_le.mpr (λ x, mul_inv_eq_iff_eq_mul.mp)))
+  (λ x h, mul_inv_eq_of_eq_mul (h g (mem_zpowers g)).symm)
+
 /-- As normal subgroups are closed under conjugation, they inherit the conjugation action
   of the underlying group. -/
 instance subgroup.conj_action {H : subgroup G} [hH : H.normal] :

src/group_theory/group_action/quotient.lean

@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Thomas Browning
 -/
 import dynamics.periodic_pts
-import group_theory.group_action.basic
+import group_theory.group_action.conj_act
+import group_theory.commutator
 import group_theory.quotient_group
 
 /-!
@@ -280,4 +281,28 @@ begin
     exact (mul_action.quotient.smul_mk H g 1).symm.trans (equiv.perm.ext_iff.mp hg (1 : G)) },
 end
 
+open quotient_group
+
+/-- Cosets of the centralizer of an element embed into the set of commutators. -/
+noncomputable def quotient_centralizer_embedding (g : G) :
+  G ⧸ centralizer (zpowers (g : G)) ↪ commutator_set G :=
+((mul_action.orbit_equiv_quotient_stabilizer (conj_act G) g).trans (quotient_equiv_of_eq
+  (conj_act.stabilizer_eq_centralizer g))).symm.to_embedding.trans ⟨λ x, ⟨x * g⁻¹,
+  let ⟨_, x, rfl⟩ := x in ⟨x, g, rfl⟩⟩, λ x y, subtype.ext ∘ mul_right_cancel ∘ subtype.ext_iff.mp⟩
+
+lemma quotient_centralizer_embedding_apply (g : G) (x : G) :
+  quotient_centralizer_embedding g x = ⟨⁅x, g⁆, x, g, rfl⟩ :=
+rfl
+
+/-- If `G` is generated by `S`, then the quotient by the center embeds into `S`-indexed sequences
+of commutators. -/
+noncomputable def quotient_center_embedding {S : set G} (hS : closure S = ⊤) :
+  G ⧸ center G ↪ S → commutator_set G :=
+(quotient_equiv_of_eq (center_eq_infi' S hS)).to_embedding.trans ((quotient_infi_embedding _).trans
+  (function.embedding.Pi_congr_right (λ g, quotient_centralizer_embedding g)))
+
+lemma quotient_center_embedding_apply {S : set G} (hS : closure S = ⊤) (g : G) (s : S) :
+  quotient_center_embedding hS g s = ⟨⁅g, s⁆, g, s, rfl⟩ :=
+rfl
+
 end subgroup

src/group_theory/index.lean

@@ -5,6 +5,7 @@ Authors: Thomas Browning
 -/
 
 import data.finite.card
+import group_theory.finiteness
 import group_theory.group_action.quotient
 
 /-!
@@ -412,6 +413,22 @@ begin
   apply_instance,
 end
 
+variables (G)
+
+instance finite_index_center [finite (commutator_set G)] [group.fg G] : finite_index (center G) :=
+begin
+  obtain ⟨S, -, hS⟩ := group.rank_spec G,
+  exact ⟨mt (finite.card_eq_zero_of_embedding (quotient_center_embedding hS)) finite.card_pos.ne'⟩,
+end
+
+lemma index_center_le_pow [finite (commutator_set G)] [group.fg G] :
+  (center G).index ≤ (nat.card (commutator_set G)) ^ group.rank G :=
+begin
+  obtain ⟨S, hS1, hS2⟩ := group.rank_spec G,
+  rw [←hS1, ←fintype.card_coe, ←nat.card_eq_fintype_card, ←finset.coe_sort_coe, ←nat.card_fun],
+  exact finite.card_le_of_embedding (quotient_center_embedding hS2),
+end
+
 end finite_index
 
 end subgroup