refactor(group_theory/general_commutator): Rename general_commutator to subgroup.commutator (#12308)

This PR renames `general_commutator` to `subgroup.commutator`.

I'll change the file name in a followup PR, so that this PR is easier to review.

(This is one of the several orthogonal changes from #12134)

Author: tb65536

src/group_theory/abelianization.lean

@@ -38,11 +38,11 @@ lemma commutator_def : commutator G = ⁅(⊤ : subgroup G), ⊤⁆ := rfl
 
 lemma commutator_eq_closure :
   commutator G = subgroup.closure {x | ∃ p q, p * q * p⁻¹ * q⁻¹ = x} :=
-by simp_rw [commutator, general_commutator_def, subgroup.mem_top, exists_true_left]
+by simp_rw [commutator, subgroup.commutator_def, subgroup.mem_top, exists_true_left]
 
 lemma commutator_eq_normal_closure :
   commutator G = subgroup.normal_closure {x | ∃ p q, p * q * p⁻¹ * q⁻¹ = x} :=
-by simp_rw [commutator, general_commutator_def', subgroup.mem_top, exists_true_left]
+by simp_rw [commutator, subgroup.commutator_def', subgroup.mem_top, exists_true_left]
 
 /-- The abelianization of G is the quotient of G by its commutator subgroup. -/
 def abelianization : Type u :=

src/group_theory/general_commutator.lean

@@ -9,33 +9,33 @@ import group_theory.subgroup.basic
 import tactic.group
 
 /-!
-# General commutators.
+# Commutators of Subgroups
 
-If `G` is a group and `H₁ H₂ : subgroup G` then the general commutator `⁅H₁, H₂⁆ : subgroup G`
+If `G` is a group and `H₁ H₂ : subgroup G` then the commutator `⁅H₁, H₂⁆ : subgroup G`
 is the subgroup of `G` generated by the commutators `h₁ * h₂ * h₁⁻¹ * h₂⁻¹`.
 
 ## Main definitions
 
-* `general_commutator H₁ H₂` : the commutator of the subgroups `H₁` and `H₂`
+* `⁅H₁, H₂⁆` : the commutator of the subgroups `H₁` and `H₂`.
 -/
 
-open subgroup
+namespace subgroup
 
 variables {G G' : Type*} [group G] [group G'] {f : G →* G'}
 
 /-- The commutator of two subgroups `H₁` and `H₂`. -/
-instance general_commutator : has_bracket (subgroup G) (subgroup G) :=
+instance commutator : has_bracket (subgroup G) (subgroup G) :=
 ⟨λ H₁ H₂, closure {x | ∃ (p ∈ H₁) (q ∈ H₂), p * q * p⁻¹ * q⁻¹ = x}⟩
 
-lemma general_commutator_def (H₁ H₂ : subgroup G) :
+lemma commutator_def (H₁ H₂ : subgroup G) :
   ⁅H₁, H₂⁆ = closure {x | ∃ (p ∈ H₁) (q ∈ H₂), p * q * p⁻¹ * q⁻¹ = x} := rfl
 
-instance general_commutator_normal (H₁ H₂ : subgroup G) [h₁ : H₁.normal]
+instance commutator_normal (H₁ H₂ : subgroup G) [h₁ : H₁.normal]
   [h₂ : H₂.normal] : normal ⁅H₁, H₂⁆ :=
 begin
   let base : set G := {x | ∃ (p ∈ H₁) (q ∈ H₂), p * q * p⁻¹ * q⁻¹ = x},
   suffices h_base : base = group.conjugates_of_set base,
-  { dsimp only [general_commutator_def, ←base],
+  { dsimp only [commutator_def, ←base],
     rw h_base,
     exact subgroup.normal_closure_normal },
   apply set.subset.antisymm group.subset_conjugates_of_set,
@@ -45,124 +45,125 @@ begin
   exact ⟨d * c * d⁻¹, h₁.conj_mem c hc d, d * e * d⁻¹, h₂.conj_mem e he d, by group⟩,
 end
 
-lemma general_commutator_mono {H₁ H₂ K₁ K₂ : subgroup G} (h₁ : H₁ ≤ K₁) (h₂ : H₂ ≤ K₂) :
+lemma commutator_mono {H₁ H₂ K₁ K₂ : subgroup G} (h₁ : H₁ ≤ K₁) (h₂ : H₂ ≤ K₂) :
   ⁅H₁, H₂⁆ ≤ ⁅K₁, K₂⁆ :=
 begin
   apply closure_mono,
   rintros x ⟨p, hp, q, hq, rfl⟩,
   exact ⟨p, h₁ hp, q, h₂ hq, rfl⟩,
 end
 
-lemma general_commutator_def' (H₁ H₂ : subgroup G) [H₁.normal] [H₂.normal] :
+lemma commutator_def' (H₁ H₂ : subgroup G) [H₁.normal] [H₂.normal] :
   ⁅H₁, H₂⁆ = normal_closure {x | ∃ (p ∈ H₁) (q ∈ H₂), p * q * p⁻¹ * q⁻¹ = x} :=
-by rw [← normal_closure_eq_self ⁅H₁, H₂⁆, general_commutator_def,
-  normal_closure_closure_eq_normal_closure]
+by rw [← normal_closure_eq_self ⁅H₁, H₂⁆, commutator_def, normal_closure_closure_eq_normal_closure]
 
-lemma general_commutator_le (H₁ H₂ : subgroup G) (K : subgroup G) :
+lemma commutator_le (H₁ H₂ : subgroup G) (K : subgroup G) :
   ⁅H₁, H₂⁆ ≤ K ↔ ∀ (p ∈ H₁) (q ∈ H₂), p * q * p⁻¹ * q⁻¹ ∈ K :=
 begin
-  rw [general_commutator, closure_le],
+  rw [subgroup.commutator, closure_le],
   split,
   { intros h p hp q hq,
     exact h ⟨p, hp, q, hq, rfl⟩, },
   { rintros h x ⟨p, hp, q, hq, rfl⟩,
     exact h p hp q hq, }
 end
 
-lemma general_commutator_containment (H₁ H₂ : subgroup G) {p q : G} (hp : p ∈ H₁) (hq : q ∈ H₂) :
+lemma commutator_containment (H₁ H₂ : subgroup G) {p q : G} (hp : p ∈ H₁) (hq : q ∈ H₂) :
   p * q * p⁻¹ * q⁻¹ ∈ ⁅H₁, H₂⁆ :=
-(general_commutator_le H₁ H₂ ⁅H₁, H₂⁆).mp (le_refl ⁅H₁, H₂⁆) p hp q hq
+(commutator_le H₁ H₂ ⁅H₁, H₂⁆).mp (le_refl ⁅H₁, H₂⁆) p hp q hq
 
-lemma general_commutator_comm (H₁ H₂ : subgroup G) : ⁅H₁, H₂⁆ = ⁅H₂, H₁⁆ :=
+lemma commutator_comm (H₁ H₂ : subgroup G) : ⁅H₁, H₂⁆ = ⁅H₂, H₁⁆ :=
 begin
   suffices : ∀ H₁ H₂ : subgroup G, ⁅H₁, H₂⁆ ≤ ⁅H₂, H₁⁆, { exact le_antisymm (this _ _) (this _ _) },
   intros H₁ H₂,
-  rw general_commutator_le,
+  rw commutator_le,
   intros p hp q hq,
   have h : (p * q * p⁻¹ * q⁻¹)⁻¹ ∈ ⁅H₂, H₁⁆ := subset_closure ⟨q, hq, p, hp, by group⟩,
   convert inv_mem ⁅H₂, H₁⁆ h,
   group,
 end
 
-lemma general_commutator_le_right (H₁ H₂ : subgroup G) [h : normal H₂] :
+lemma commutator_le_right (H₁ H₂ : subgroup G) [h : normal H₂] :
   ⁅H₁, H₂⁆ ≤ H₂ :=
 begin
-  rw general_commutator_le,
+  rw commutator_le,
   intros p hp q hq,
   exact mul_mem H₂ (h.conj_mem q hq p) (inv_mem H₂ hq),
 end
 
-lemma general_commutator_le_left (H₁ H₂ : subgroup G) [h : normal H₁] :
+lemma commutator_le_left (H₁ H₂ : subgroup G) [h : normal H₁] :
   ⁅H₁, H₂⁆ ≤ H₁ :=
 begin
-  rw general_commutator_comm,
-  exact general_commutator_le_right H₂ H₁,
+  rw commutator_comm,
+  exact commutator_le_right H₂ H₁,
 end
 
-@[simp] lemma general_commutator_bot (H : subgroup G) : ⁅H, ⊥⁆ = (⊥ : subgroup G) :=
-by { rw eq_bot_iff, exact general_commutator_le_right H ⊥ }
+@[simp] lemma commutator_bot (H : subgroup G) : ⁅H, ⊥⁆ = (⊥ : subgroup G) :=
+by { rw eq_bot_iff, exact commutator_le_right H ⊥ }
 
-@[simp] lemma bot_general_commutator (H : subgroup G) : ⁅(⊥ : subgroup G), H⁆ = (⊥ : subgroup G) :=
-by { rw eq_bot_iff, exact general_commutator_le_left ⊥ H }
+@[simp] lemma bot_commutator (H : subgroup G) : ⁅(⊥ : subgroup G), H⁆ = (⊥ : subgroup G) :=
+by { rw eq_bot_iff, exact commutator_le_left ⊥ H }
 
-lemma general_commutator_le_inf (H₁ H₂ : subgroup G) [normal H₁] [normal H₂] :
+lemma commutator_le_inf (H₁ H₂ : subgroup G) [normal H₁] [normal H₂] :
   ⁅H₁, H₂⁆ ≤ H₁ ⊓ H₂ :=
-by simp only [general_commutator_le_left, general_commutator_le_right, le_inf_iff, and_self]
+by simp only [commutator_le_left, commutator_le_right, le_inf_iff, and_self]
 
-lemma map_general_commutator {G₂ : Type*} [group G₂] (f : G →* G₂) (H₁ H₂ : subgroup G)  :
+lemma map_commutator {G₂ : Type*} [group G₂] (f : G →* G₂) (H₁ H₂ : subgroup G)  :
   map f ⁅H₁, H₂⁆ = ⁅map f H₁, map f H₂⁆ :=
 begin
   apply le_antisymm,
-  { rw [gc_map_comap, general_commutator_le],
+  { rw [gc_map_comap, commutator_le],
     intros p hp q hq,
     simp only [mem_comap, map_inv, map_mul],
-    exact general_commutator_containment _ _ (mem_map_of_mem _ hp) (mem_map_of_mem _ hq), },
-  { rw [general_commutator_le],
+    exact commutator_containment _ _ (mem_map_of_mem _ hp) (mem_map_of_mem _ hq), },
+  { rw [commutator_le],
     rintros _ ⟨p, hp, rfl⟩ _ ⟨q, hq, rfl⟩,
     simp only [← map_inv, ← map_mul],
-    exact mem_map_of_mem _ (general_commutator_containment _ _ hp hq), }
+    exact mem_map_of_mem _ (commutator_containment _ _ hp hq), }
 end
 
-lemma general_commutator_prod_prod {G₂ : Type*} [group G₂]
+lemma commutator_prod_prod {G₂ : Type*} [group G₂]
   (H₁ K₁ : subgroup G) (H₂ K₂ : subgroup G₂) :
   ⁅H₁.prod H₂, K₁.prod K₂⁆ = ⁅H₁, K₁⁆.prod ⁅H₂, K₂⁆ :=
 begin
   apply le_antisymm,
-  { rw general_commutator_le,
+  { rw commutator_le,
     rintros ⟨p₁, p₂⟩ ⟨hp₁, hp₂⟩ ⟨q₁, q₂⟩ ⟨hq₁, hq₂⟩,
-    exact ⟨general_commutator_containment _ _ hp₁ hq₁, general_commutator_containment _ _ hp₂ hq₂⟩},
+    exact ⟨commutator_containment _ _ hp₁ hq₁, commutator_containment _ _ hp₂ hq₂⟩},
   { rw prod_le_iff, split;
-    { rw map_general_commutator,
-      apply general_commutator_mono;
+    { rw map_commutator,
+      apply commutator_mono;
       simp [le_prod_iff, map_map, monoid_hom.fst_comp_inl, monoid_hom.snd_comp_inl,
         monoid_hom.fst_comp_inr, monoid_hom.snd_comp_inr ], }, }
 end
 
 /-- The commutator of direct product is contained in the direct product of the commutators.
 
-See `general_commutator_pi_pi_of_fintype` for equality given `fintype η`.
+See `commutator_pi_pi_of_fintype` for equality given `fintype η`.
 -/
-lemma general_commutator_pi_pi_le {η : Type*} {Gs : η → Type*} [∀ i, group (Gs i)]
+lemma commutator_pi_pi_le {η : Type*} {Gs : η → Type*} [∀ i, group (Gs i)]
   (H K : Π i, subgroup (Gs i)) :
   ⁅subgroup.pi set.univ H, subgroup.pi set.univ K⁆ ≤ subgroup.pi set.univ (λ i, ⁅H i, K i⁆) :=
-(general_commutator_le _ _ _).mpr $
-  λ p hp q hq i hi, general_commutator_containment _ _ (hp i hi) (hq i hi)
+(commutator_le _ _ _).mpr $
+  λ p hp q hq i hi, commutator_containment _ _ (hp i hi) (hq i hi)
 
 /-- The commutator of a finite direct product is contained in the direct product of the commutators.
 -/
-lemma general_commutator_pi_pi_of_fintype {η : Type*} [fintype η] {Gs : η → Type*}
+lemma commutator_pi_pi_of_fintype {η : Type*} [fintype η] {Gs : η → Type*}
   [∀ i, group (Gs i)] (H K : Π i, subgroup (Gs i)) :
   ⁅subgroup.pi set.univ H, subgroup.pi set.univ K⁆ = subgroup.pi set.univ (λ i, ⁅H i, K i⁆) :=
 begin
   classical,
-  apply le_antisymm (general_commutator_pi_pi_le H K),
+  apply le_antisymm (commutator_pi_pi_le H K),
   { rw pi_le_iff, intros i hi,
-    rw map_general_commutator,
-    apply general_commutator_mono;
+    rw map_commutator,
+    apply commutator_mono;
     { rw le_pi_iff,
       intros j hj,
       rintros _ ⟨_, ⟨x, hx, rfl⟩, rfl⟩,
       by_cases h : j = i,
       { subst h, simpa using hx, },
       { simp [h, one_mem] }, }, },
 end
+
+end subgroup

src/group_theory/nilpotent.lean

@@ -290,7 +290,7 @@ instance (n : ℕ) : normal (lower_central_series G n) :=
 begin
   induction n with d hd,
   { exact (⊤ : subgroup G).normal_of_characteristic },
-  { exactI general_commutator_normal (lower_central_series G d) ⊤ },
+  { exactI subgroup.commutator_normal (lower_central_series G d) ⊤ },
 end
 
 lemma lower_central_series_antitone :
@@ -313,7 +313,7 @@ theorem lower_central_series_is_descending_central_series :
 begin
   split, refl,
   intros x n hxn g,
-  exact general_commutator_containment _ _ hxn (subgroup.mem_top g),
+  exact commutator_containment _ _ hxn (mem_top g),
 end
 
 /-- Any descending central series for a group is bounded below by the lower central series. -/
@@ -322,7 +322,7 @@ lemma descending_central_series_ge_lower (H : ℕ → subgroup G)
 | 0 := hH.1.symm ▸ le_refl ⊤
 | (n + 1) := begin
   specialize descending_central_series_ge_lower n,
-  apply (general_commutator_le _ _ _).2,
+  apply (commutator_le _ _ _).2,
   intros x hx q _,
   exact hH.2 x n (descending_central_series_ge_lower hx) q,
 end
@@ -671,7 +671,7 @@ end
 
 
 lemma derived_le_lower_central (n : ℕ) : derived_series G n ≤ lower_central_series G n :=
-by { induction n with i ih, { simp }, { apply general_commutator_mono ih, simp } }
+by { induction n with i ih, { simp }, { apply commutator_mono ih, simp } }
 
 /-- Abelian groups are nilpotent -/
 @[priority 100]
@@ -715,7 +715,7 @@ begin
     ... = ⁅(lower_central_series G₁ n).prod (lower_central_series G₂ n), (⊤ : subgroup G₁).prod ⊤⁆ :
       by simp
     ... = ⁅lower_central_series G₁ n, (⊤ : subgroup G₁)⁆.prod ⁅lower_central_series G₂ n, ⊤⁆ :
-      general_commutator_prod_prod _ _ _ _
+      commutator_prod_prod _ _ _ _
     ... = (lower_central_series G₁ n.succ).prod (lower_central_series G₂ n.succ) : rfl }
 end
 
@@ -755,9 +755,9 @@ begin
   { simp [pi_top] },
   { calc lower_central_series (Π i, Gs i) n.succ
         = ⁅lower_central_series (Π i, Gs i) n, ⊤⁆           : rfl
-    ... ≤ ⁅pi (λ i, (lower_central_series (Gs i) n)), ⊤⁆    : general_commutator_mono ih (le_refl _)
+    ... ≤ ⁅pi (λ i, (lower_central_series (Gs i) n)), ⊤⁆    : commutator_mono ih (le_refl _)
     ... = ⁅pi (λ i, (lower_central_series (Gs i) n)), pi (λ i, ⊤)⁆ : by simp [pi, pi_top]
-    ... ≤ pi (λ i, ⁅(lower_central_series (Gs i) n), ⊤⁆)    : general_commutator_pi_pi_le _ _
+    ... ≤ pi (λ i, ⁅(lower_central_series (Gs i) n), ⊤⁆)    : commutator_pi_pi_le _ _
     ... = pi (λ i, lower_central_series (Gs i) n.succ)      : rfl }
 end
 
@@ -793,7 +793,7 @@ begin
         = ⁅lower_central_series (Π i, Gs i) n, ⊤⁆          : rfl
     ... = ⁅pi (λ i, (lower_central_series (Gs i) n)), ⊤⁆   : by rw ih
     ... = ⁅pi (λ i, (lower_central_series (Gs i) n)), pi (λ i, ⊤)⁆ : by simp [pi, pi_top]
-    ... = pi (λ i, ⁅(lower_central_series (Gs i) n), ⊤⁆)   : general_commutator_pi_pi_of_fintype _ _
+    ... = pi (λ i, ⁅(lower_central_series (Gs i) n), ⊤⁆)   : commutator_pi_pi_of_fintype _ _
     ... = pi (λ i, lower_central_series (Gs i) n.succ)     : rfl }
 end
 

src/group_theory/solvable.lean

@@ -46,7 +46,7 @@ lemma derived_series_normal (n : ℕ) : (derived_series G n).normal :=
 begin
   induction n with n ih,
   { exact (⊤ : subgroup G).normal_of_characteristic },
-  { exactI general_commutator_normal (derived_series G n) (derived_series G n) }
+  { exactI subgroup.commutator_normal (derived_series G n) (derived_series G n) }
 end
 
 @[simp] lemma derived_series_one : derived_series G 1 = commutator G :=
@@ -58,7 +58,7 @@ section commutator_map
 
 lemma commutator_le_map_commutator {H₁ H₂ : subgroup G} {K₁ K₂ : subgroup G'} (h₁ : K₁ ≤ H₁.map f)
   (h₂ : K₂ ≤ H₂.map f) : ⁅K₁, K₂⁆ ≤ ⁅H₁, H₂⁆.map f :=
-by { rw map_general_commutator, exact general_commutator_mono h₁ h₂ }
+by { rw map_commutator, exact commutator_mono h₁ h₂ }
 
 section derived_series_map
 
@@ -69,7 +69,7 @@ lemma map_derived_series_le_derived_series (n : ℕ) :
 begin
   induction n with n ih,
   { simp only [derived_series_zero, le_top], },
-  { simp only [derived_series_succ, map_general_commutator, general_commutator_mono, *], }
+  { simp only [derived_series_succ, map_commutator, commutator_mono, ih] }
 end
 
 variables {f}
@@ -195,8 +195,8 @@ begin
   { exact derived_series_one G },
   rw [derived_series_succ, ih],
   cases (commutator.normal G).eq_bot_or_eq_top with h h,
-  { rw [h, general_commutator_bot] },
-  { rwa [h, ←commutator_def] },
+  { rw [h, commutator_bot] },
+  { rwa h },
 end
 
 lemma is_simple_group.comm_iff_is_solvable :
@@ -236,7 +236,7 @@ begin
   { exact mem_top x },
   { rw key,
     exact (derived_series_normal _ _).conj_mem _
-      (general_commutator_containment _ _ ih ((derived_series_normal _ _).conj_mem _ ih _)) _ },
+      (commutator_containment _ _ ih ((derived_series_normal _ _).conj_mem _ ih _)) _ },
 end
 
 lemma equiv.perm.not_solvable (X : Type*) (hX : 5 ≤ cardinal.mk X) :