feat(group_theory/schreier): The size of the commutator subgroup is b…

…ounded in terms of the index of the center and the number of commutators (#16679)

This PR proves that the size of the commutator subgroup is bounded in terms of the index of the center and the number of commutators. The proof uses Schreier's lemma and the transfer homomorphism.

I included lots of comments since the proof is rather technical. But please let me know if I went overboard.

Ultimately, this is building up to a bound on the size of the commutator subgroup just in terms of the number of commutators.



Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>

src/group_theory/abelianization.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Michael Howes
 -/
 import group_theory.commutator
-import group_theory.quotient_group
+import group_theory.finiteness
 
 /-!
 # The abelianization of a group
@@ -46,6 +46,19 @@ by simp_rw [commutator, subgroup.commutator_def', subgroup.mem_top, exists_true_
 instance commutator_characteristic : (commutator G).characteristic :=
 subgroup.commutator_characteristic ⊤ ⊤
 
+instance [finite {g | ∃ g₁ g₂ : G, ⁅g₁, g₂⁆ = g}] : group.fg (commutator G) :=
+begin
+  rw commutator_eq_closure,
+  apply group.closure_finite_fg,
+end
+
+lemma rank_commutator_le_card [finite {g | ∃ g₁ g₂ : G, ⁅g₁, g₂⁆ = g}] :
+  group.rank (commutator G) ≤ nat.card {g | ∃ g₁ g₂ : G, ⁅g₁, g₂⁆ = g} :=
+begin
+  rw subgroup.rank_congr (commutator_eq_closure G),
+  apply subgroup.rank_closure_finite_le_nat_card,
+end
+
 lemma commutator_centralizer_commutator_le_center :
   ⁅(commutator G).centralizer, (commutator G).centralizer⁆ ≤ subgroup.center G :=
 begin

src/group_theory/schreier.lean

@@ -4,11 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning
 -/
 
-import data.finset.pointwise
-import group_theory.complement
-import group_theory.finiteness
-import group_theory.index
-import tactic.group
+import group_theory.abelianization
+import group_theory.exponent
+import group_theory.transfer
 
 /-!
 # Schreier's Lemma
@@ -144,4 +142,35 @@ begin
   ... = H.index * group.rank G : congr_arg ((*) H.index) hS₀,
 end
 
+variables (G)
+
+/-- If `G` has `n` commutators `[g₁, g₂]`, then `|G'| ∣ [G : Z(G)] ^ ([G : Z(G)] * n + 1)`,
+where `G'` denotes the commutator of `G`. -/
+lemma card_commutator_dvd_index_center_pow [finite {g | ∃ g₁ g₂ : G, ⁅g₁, g₂⁆ = g}] :
+  nat.card (commutator G) ∣
+    (center G).index ^ ((center G).index * nat.card {g | ∃ g₁ g₂ : G, ⁅g₁, g₂⁆ = g} + 1) :=
+begin
+  -- First handle the case when `Z(G)` has infinite index and `[G : Z(G)]` is defined to be `0`
+  by_cases hG : (center G).index = 0,
+  { simp_rw [hG, zero_mul, zero_add, pow_one, dvd_zero] },
+  -- Rewrite as `|Z(G) ∩ G'| * [G' : Z(G) ∩ G'] ∣ [G : Z(G)] ^ ([G : Z(G)] * n) * [G : Z(G)]`
+  rw [←((center G).subgroup_of (commutator G)).card_mul_index, pow_succ'],
+  -- We have `h1 : [G' : Z(G) ∩ G'] ∣ [G : Z(G)]`
+  have h1 := relindex_dvd_index_of_normal (center G) (commutator G),
+  -- So we can reduce to proving `|Z(G) ∩ G'| ∣ [G : Z(G)] ^ ([G : Z(G)] * n)`
+  refine mul_dvd_mul _ h1,
+  -- We have `h2 : rank (Z(G) ∩ G') ≤ [G' : Z(G) ∩ G'] * rank G'` by Schreier's lemma
+  have h2 := rank_le_index_mul_rank (ne_zero_of_dvd_ne_zero hG h1),
+  -- We have `h3 : [G' : Z(G) ∩ G'] * rank G' ≤ [G : Z(G)] * n` by `h1` and `rank G' ≤ n`
+  have h3 := nat.mul_le_mul (nat.le_of_dvd (nat.pos_of_ne_zero hG) h1) (rank_commutator_le_card G),
+  -- So we can reduce to proving `|Z(G) ∩ G'| ∣ [G : Z(G)] ^ rank (Z(G) ∩ G')`
+  refine dvd_trans _ (pow_dvd_pow (center G).index (h2.trans h3)),
+  -- `Z(G) ∩ G'` is abelian, so it enough to prove that `g ^ [G : Z(G)] = 1` for `g ∈ Z(G) ∩ G'`
+  apply card_dvd_exponent_pow_rank' _ (λ g, _),
+  -- `Z(G)` is abelian, so `g ∈ Z(G) ∩ G' ≤ G' ≤ ker (transfer : G → Z(G))`
+  have := abelianization.commutator_subset_ker (monoid_hom.transfer_center_pow' hG) g.1.2,
+  -- `transfer g` is defeq to `g ^ [G : Z(G)]`, so we are done
+  simpa only [monoid_hom.mem_ker, subtype.ext_iff] using this,
+end
+
 end subgroup