refactor(group_theory/commutator): Define commutators of subgroups in…

… terms of commutators of elements (#12309)

This PR defines commutators of elements of groups.

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

src/algebra/group/basic.lean

@@ -5,6 +5,7 @@ Authors: Jeremy Avigad, Leonardo de Moura, Simon Hudon, Mario Carneiro
 -/
 
 import algebra.group.defs
+import data.bracket
 import logic.function.basic
 
 /-!
@@ -619,3 +620,14 @@ end
 by rw [div_eq_iff_eq_mul, div_mul_eq_mul_div', div_eq_iff_eq_mul', mul_div_assoc]
 
 end comm_group
+
+section commutator
+
+/-- The commutator of two elements `g₁` and `g₂`. -/
+instance commutator_element {G : Type*} [group G] : has_bracket G G :=
+⟨λ g₁ g₂, g₁ * g₂ * g₁⁻¹ * g₂⁻¹⟩
+
+lemma commutator_element_def  {G : Type*} [group G] (g₁ g₂ : G) :
+  ⁅g₁, g₂⁆ = g₁ * g₂ * g₁⁻¹ * g₂⁻¹ := rfl
+
+end commutator

src/group_theory/abelianization.lean

@@ -36,12 +36,11 @@ def commutator : 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} :=
+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_normal_closure :
-  commutator G = subgroup.normal_closure {x | ∃ p q, p * q * p⁻¹ * q⁻¹ = x} :=
+  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]
 
 /-- The abelianization of G is the quotient of G by its commutator subgroup. -/
@@ -84,7 +83,7 @@ lemma commutator_subset_ker : commutator G ≤ f.ker :=
 begin
   rw [commutator_eq_closure, subgroup.closure_le],
   rintros x ⟨p, q, rfl⟩,
-  simp [monoid_hom.mem_ker, mul_right_comm (f p) (f q)],
+  simp [monoid_hom.mem_ker, mul_right_comm (f p) (f q), commutator_element_def],
 end
 
 /-- If `f : G → A` is a group homomorphism to an abelian group, then `lift f` is the unique map from

src/group_theory/commutator.lean

@@ -16,27 +16,38 @@ is the subgroup of `G` generated by the commutators `h₁ * h₂ * h₁⁻¹ * h
 
 ## Main definitions
 
+* `⁅g₁, g₂⁆` : the commutator of the elements `g₁` and `g₂`
+    (defined by `commutator_element` elsewhere).
 * `⁅H₁, H₂⁆` : the commutator of the subgroups `H₁` and `H₂`.
 -/
 
-namespace subgroup
+variables {G G' F : Type*} [group G] [group G'] [monoid_hom_class F G G] (f : F) (g₁ g₂ g₃ : G)
+
+@[simp] lemma commutator_element_inv : ⁅g₁, g₂⁆⁻¹ = ⁅g₂, g₁⁆ :=
+by simp_rw [commutator_element_def, mul_inv_rev, inv_inv, mul_assoc]
+
+lemma map_commutator_element : f ⁅g₁, g₂⁆ = ⁅f g₁, f g₂⁆ :=
+by simp_rw [commutator_element_def, map_mul f, map_inv f]
 
-variables {G G' : Type*} [group G] [group G'] {f : G →* G'}
+lemma conjugate_commutator_element : g₃ * ⁅g₁, g₂⁆ * g₃⁻¹ = ⁅g₃ * g₁ * g₃⁻¹, g₃ * g₂ * g₃⁻¹⁆ :=
+map_commutator_element (mul_aut.conj g₃).to_monoid_hom g₁ g₂
+
+namespace subgroup
 
 /-- The commutator of two subgroups `H₁` and `H₂`. -/
 instance commutator : has_bracket (subgroup G) (subgroup G) :=
-⟨λ H₁ H₂, closure {x | ∃ (p ∈ H₁) (q ∈ H₂), p * q * p⁻¹ * q⁻¹ = x}⟩
+⟨λ H₁ H₂, closure {g | ∃ (g₁ ∈ H₁) (g₂ ∈ H₂), ⁅g₁, g₂⁆ = g}⟩
 
 lemma commutator_def (H₁ H₂ : subgroup G) :
-  ⁅H₁, H₂⁆ = closure {x | ∃ (p ∈ H₁) (q ∈ H₂), p * q * p⁻¹ * q⁻¹ = x} := rfl
+  ⁅H₁, H₂⁆ = closure {g | ∃ (g₁ ∈ H₁) (g₂ ∈ H₂), ⁅g₁, g₂⁆ = g} := rfl
 
 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},
+  change (closure base).normal,
   suffices h_base : base = group.conjugates_of_set base,
-  { dsimp only [commutator_def, ←base],
-    rw h_base,
+  { rw h_base,
     exact subgroup.normal_closure_normal },
   apply set.subset.antisymm group.subset_conjugates_of_set,
   intros a h,
@@ -54,8 +65,8 @@ begin
 end
 
 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₂⁆, commutator_def, normal_closure_closure_eq_normal_closure]
+  ⁅H₁, H₂⁆ = normal_closure {g | ∃ (g₁ ∈ H₁) (g₂ ∈ H₂), ⁅g₁, g₂⁆ = g} :=
+le_antisymm closure_le_normal_closure (normal_closure_le_normal subset_closure)
 
 lemma commutator_le (H₁ H₂ : subgroup G) (K : subgroup G) :
   ⁅H₁, H₂⁆ ≤ K ↔ ∀ (p ∈ H₁) (q ∈ H₂), p * q * p⁻¹ * q⁻¹ ∈ K :=

src/group_theory/nilpotent.lean

@@ -499,7 +499,7 @@ begin
       (λ y hy, by simp [f.map_inv, subgroup.inv_mem _ hy]),
     rintros a ⟨y, hy, z, ⟨-, rfl⟩⟩,
     apply mem_closure.mpr,
-    exact λ K hK, hK ⟨f y, hd (mem_map_of_mem f hy), by simp⟩ }
+    exact λ K hK, hK ⟨f y, hd (mem_map_of_mem f hy), by simp [commutator_element_def]⟩ }
 end
 
 lemma lower_central_series_succ_eq_bot {n : ℕ} (h : lower_central_series G n ≤ center G) :

src/tactic/group.lean

@@ -50,6 +50,7 @@ open tactic.simp_arg_type interactive tactic.group
 /-- Auxiliary tactic for the `group` tactic. Calls the simplifier only. -/
 meta def aux_group₁ (locat : loc) : tactic unit :=
   simp_core {} skip tt [
+  expr ``(commutator_element_def),
   expr ``(mul_one),
   expr ``(one_mul),
   expr ``(one_pow),

test/group.lean

@@ -11,18 +11,12 @@ by group
 example (a b c d : G) : c⁻¹*(b*c⁻¹)*c *(a*b)*(b⁻¹*a⁻¹*b⁻¹)*c = 1 :=
 by group
 
-
-def commutator {G} [group G] : G → G → G := λ g h, g * h * g⁻¹ * h⁻¹
-
-def commutator3 {G} [group G] : G → G → G → G := λ g h k, commutator (commutator g h) k
-
 -- The following is known as the Hall-Witt identity,
 -- see e.g.
 -- https://en.wikipedia.org/wiki/Three_subgroups_lemma#Proof_and_the_Hall%E2%80%93Witt_identity
 example (g h k : G) :
-  g * (commutator3 g⁻¹ h k) * g⁻¹ * k * (commutator3 k⁻¹ g h) * k⁻¹ *
-    h * (commutator3 h⁻¹ k g) * h⁻¹ = 1 :=
-by { dsimp [commutator3, commutator], group }
+  g * ⁅⁅g⁻¹, h⁆, k⁆ * g⁻¹ * k * ⁅⁅k⁻¹, g⁆, h⁆ * k⁻¹ * h *⁅⁅h⁻¹, k⁆, g⁆ * h⁻¹ = 1 :=
+by group
 
 example (a : G) : a^2*a = a^3 :=
 by group