feat(group_theory/commutator): Define the set of commutators (#17276)

With some of my upcoming group theory PRs, it is going to start being helpful to have a name for the set of commutators.

src/group_theory/abelianization.lean

@@ -36,24 +36,24 @@ def commutator : subgroup G :=
 
 lemma commutator_def : commutator G = ⁅(⊤ : subgroup G), ⊤⁆ := rfl
 
-lemma commutator_eq_closure : commutator G = subgroup.closure {g | ∃ g₁ g₂ : G, ⁅g₁, g₂⁆ = g} :=
-by simp_rw [commutator, subgroup.commutator_def, subgroup.mem_top, exists_true_left]
+lemma commutator_eq_closure : commutator G = subgroup.closure (commutator_set G) :=
+by simp [commutator, subgroup.commutator_def, commutator_set]
 
 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]
+  commutator G = subgroup.normal_closure (commutator_set G) :=
+by simp [commutator, subgroup.commutator_def', commutator_set]
 
 instance commutator_characteristic : (commutator G).characteristic :=
 subgroup.commutator_characteristic ⊤ ⊤
 
-instance [finite {g | ∃ g₁ g₂ : G, ⁅g₁, g₂⁆ = g}] : group.fg (commutator G) :=
+instance [finite (commutator_set 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} :=
+lemma rank_commutator_le_card [finite (commutator_set G)] :
+  group.rank (commutator G) ≤ nat.card (commutator_set G) :=
 begin
   rw subgroup.rank_congr (commutator_eq_closure G),
   apply subgroup.rank_closure_finite_le_nat_card,

src/group_theory/commutator.lean

@@ -204,3 +204,25 @@ begin
 end
 
 end subgroup
+
+variables (G)
+
+/-- The set of commutator elements `⁅g₁, g₂⁆` in `G`. -/
+def commutator_set : set G :=
+{g | ∃ g₁ g₂ : G, ⁅g₁, g₂⁆ = g}
+
+lemma commutator_set_def : commutator_set G = {g | ∃ g₁ g₂ : G, ⁅g₁, g₂⁆ = g} := rfl
+
+lemma one_mem_commutator_set : (1 : G) ∈ commutator_set G :=
+⟨1, 1, commutator_element_self 1⟩
+
+instance : nonempty (commutator_set G) :=
+⟨⟨1, one_mem_commutator_set G⟩⟩
+
+variables {G g}
+
+lemma mem_commutator_set_iff : g ∈ commutator_set G ↔ ∃ g₁ g₂ : G, ⁅g₁, g₂⁆ = g :=
+iff.rfl
+
+lemma commutator_mem_commutator_set : ⁅g₁, g₂⁆ ∈ commutator_set G :=
+⟨g₁, g₂, rfl⟩

src/group_theory/schreier.lean

@@ -146,9 +146,9 @@ 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}] :
+lemma card_commutator_dvd_index_center_pow [finite (commutator_set G)] :
   nat.card (commutator G) ∣
-    (center G).index ^ ((center G).index * nat.card {g | ∃ g₁ g₂ : G, ⁅g₁, g₂⁆ = g} + 1) :=
+    (center G).index ^ ((center G).index * nat.card (commutator_set 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,