refactor(group_theory/abelianization): Define commutator in terms of general_commutator (#11949)

It seems reasonable to define `commutator` in terms of `general_commutator`.

Author: tb65536

src/group_theory/abelianization.lean

@@ -3,8 +3,8 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Michael Howes
 -/
+import group_theory.general_commutator
 import group_theory.quotient_group
-import tactic.group
 
 /-!
 # The abelianization of a group
@@ -32,7 +32,17 @@ variables (G : Type u) [group G]
   generated by the commutators [p,q]=`p*q*p⁻¹*q⁻¹`. -/
 @[derive subgroup.normal]
 def commutator : subgroup G :=
-subgroup.normal_closure {x | ∃ p q, p * q * p⁻¹ * q⁻¹ = x}
+⁅(⊤ : subgroup G), ⊤⁆
+
+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]
+
+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]
 
 /-- The abelianization of G is the quotient of G by its commutator subgroup. -/
 def abelianization : Type u :=
@@ -43,13 +53,8 @@ namespace abelianization
 local attribute [instance] quotient_group.left_rel
 
 instance : comm_group (abelianization G) :=
-{ mul_comm := λ x y, quotient.induction_on₂' x y $ λ a b,
-  begin
-    apply quotient.sound,
-    apply subgroup.subset_normal_closure,
-    use b⁻¹, use a⁻¹,
-    group,
-  end,
+{ mul_comm := λ x y, quotient.induction_on₂' x y $ λ a b, quotient.sound' $
+    subgroup.subset_closure ⟨b⁻¹, subgroup.mem_top b⁻¹, a⁻¹, subgroup.mem_top a⁻¹, by group⟩,
 .. quotient_group.quotient.group _ }
 
 instance : inhabited (abelianization G) := ⟨1⟩
@@ -77,7 +82,7 @@ variables {A : Type v} [comm_group A] (f : G →* A)
 
 lemma commutator_subset_ker : commutator G ≤ f.ker :=
 begin
-  apply subgroup.normal_closure_le_normal,
+  rw [commutator_eq_closure, subgroup.closure_le],
   rintros x ⟨p, q, rfl⟩,
   simp [monoid_hom.mem_ker, mul_right_comm (f p) (f q)],
 end

src/group_theory/nilpotent.lean

@@ -269,8 +269,7 @@ variable {G}
 
 @[simp] lemma lower_central_series_zero : lower_central_series G 0 = ⊤ := rfl
 
-@[simp] lemma lower_central_series_one : lower_central_series G 1 = commutator G :=
-by simp [lower_central_series]
+@[simp] lemma lower_central_series_one : lower_central_series G 1 = commutator G := rfl
 
 lemma mem_lower_central_series_succ_iff (n : ℕ) (q : G) :
   q ∈ lower_central_series G (n + 1) ↔

src/group_theory/solvable.lean

@@ -49,25 +49,8 @@ begin
   { exactI general_commutator_normal (derived_series G n) (derived_series G n) }
 end
 
-@[simp] lemma general_commutator_eq_commutator :
-  ⁅(⊤ : subgroup G), (⊤ : subgroup G)⁆ = commutator G :=
-begin
-  rw [commutator, general_commutator_def'],
-  apply le_antisymm; apply normal_closure_mono,
-  { exact λ x ⟨p, _, q, _, h⟩, ⟨p, q, h⟩, },
-  { exact λ x ⟨p, q, h⟩, ⟨p, mem_top p, q, mem_top q, h⟩, }
-end
-
-lemma commutator_def' : commutator G = subgroup.closure {x : G | ∃ p q, p * q * p⁻¹ * q⁻¹ = x} :=
-begin
-  rw [← general_commutator_eq_commutator, general_commutator],
-  apply le_antisymm; apply closure_mono,
-  { exact λ x ⟨p, _, q, _, h⟩, ⟨p, q, h⟩ },
-  { exact λ x ⟨p, q, h⟩, ⟨p, mem_top p, q, mem_top q, h⟩ }
-end
-
 @[simp] lemma derived_series_one : derived_series G 1 = commutator G :=
-general_commutator_eq_commutator G
+rfl
 
 end derived_series
 
@@ -220,9 +203,11 @@ variable [is_simple_group G]
 lemma is_simple_group.derived_series_succ {n : ℕ} : derived_series G n.succ = commutator G :=
 begin
   induction n with n ih,
-  { exact derived_series_one _ },
+  { exact derived_series_one G },
   rw [derived_series_succ, ih],
-  cases (commutator.normal G).eq_bot_or_eq_top with h h; simp [h]
+  cases (commutator.normal G).eq_bot_or_eq_top with h h,
+  { rw [h, general_commutator_bot] },
+  { rwa [h, ←commutator_def] },
 end
 
 lemma is_simple_group.comm_iff_is_solvable :
@@ -236,8 +221,8 @@ lemma is_simple_group.comm_iff_is_solvable :
       exact mem_top _ } },
   { rw is_simple_group.derived_series_succ at hn,
     intros a b,
-    rw [← mul_inv_eq_one, mul_inv_rev, ← mul_assoc, ← mem_bot, ← hn],
-    exact subset_normal_closure ⟨a, b, rfl⟩ }
+    rw [← mul_inv_eq_one, mul_inv_rev, ← mul_assoc, ← mem_bot, ← hn, commutator_eq_closure],
+    exact subset_closure ⟨a, b, rfl⟩ }
 end⟩
 
 end is_simple_group