From 5fefdfa15e664c3606bcd6dd5c0a931301263a0b Mon Sep 17 00:00:00 2001 From: Thomas Browning Date: Sat, 1 Oct 2022 02:05:34 +0000 Subject: [PATCH] feat(group_theory/schreier): The size of the commutator subgroup is bounded 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 --- src/group_theory/abelianization.lean | 15 ++++++++++- src/group_theory/schreier.lean | 39 ++++++++++++++++++++++++---- 2 files changed, 48 insertions(+), 6 deletions(-) diff --git a/src/group_theory/abelianization.lean b/src/group_theory/abelianization.lean index e7be75497aac9..4bb299c2123ac 100644 --- a/src/group_theory/abelianization.lean +++ b/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 diff --git a/src/group_theory/schreier.lean b/src/group_theory/schreier.lean index bf5b797a3e06a..6ea43693665e8 100644 --- a/src/group_theory/schreier.lean +++ b/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