refactor(group_theory/commutator): Use variables and rearrange lemmas (…

…#12629)

This PR adds variables, and rearranges some of the lemmas (moving the lemmas about normal subgroups to a separate section).

src/group_theory/commutator.lean

@@ -58,16 +58,36 @@ instance commutator : has_bracket (subgroup G) (subgroup G) :=
 lemma commutator_def (H₁ H₂ : subgroup G) :
   ⁅H₁, H₂⁆ = closure {g | ∃ (g₁ ∈ H₁) (g₂ ∈ H₂), ⁅g₁, g₂⁆ = g} := rfl
 
-lemma commutator_mem_commutator {H₁ H₂ : subgroup G} {g₁ g₂ : G} (h₁ : g₁ ∈ H₁) (h₂ : g₂ ∈ H₂) :
-  ⁅g₁, g₂⁆ ∈ ⁅H₁, H₂⁆ :=
+variables {g₁ g₂ g₃} {H₁ H₂ H₃ K₁ K₂ : subgroup G}
+
+lemma commutator_mem_commutator (h₁ : g₁ ∈ H₁) (h₂ : g₂ ∈ H₂) : ⁅g₁, g₂⁆ ∈ ⁅H₁, H₂⁆ :=
 subset_closure ⟨g₁, h₁, g₂, h₂, rfl⟩
 
-lemma commutator_le {H₁ H₂ H₃ : subgroup G} :
-  ⁅H₁, H₂⁆ ≤ H₃ ↔ ∀ (g₁ ∈ H₁) (g₂ ∈ H₂), ⁅g₁, g₂⁆ ∈ H₃ :=
+lemma commutator_le : ⁅H₁, H₂⁆ ≤ H₃ ↔ ∀ (g₁ ∈ H₁) (g₂ ∈ H₂), ⁅g₁, g₂⁆ ∈ H₃ :=
 H₃.closure_le.trans ⟨λ h a b c d, h ⟨a, b, c, d, rfl⟩, λ h g ⟨a, b, c, d, h_eq⟩, h_eq ▸ h a b c d⟩
 
-instance commutator_normal (H₁ H₂ : subgroup G) [h₁ : H₁.normal]
-  [h₂ : H₂.normal] : normal ⁅H₁, H₂⁆ :=
+lemma commutator_mono (h₁ : H₁ ≤ K₁) (h₂ : H₂ ≤ K₂) : ⁅H₁, H₂⁆ ≤ ⁅K₁, K₂⁆ :=
+commutator_le.mpr (λ g₁ hg₁ g₂ hg₂, commutator_mem_commutator (h₁ hg₁) (h₂ hg₂))
+
+lemma commutator_eq_bot_iff_le_centralizer : ⁅H₁, H₂⁆ = ⊥ ↔ H₁ ≤ H₂.centralizer :=
+begin
+  rw [eq_bot_iff, commutator_le],
+  refine forall_congr (λ p, forall_congr (λ hp, forall_congr (λ q, forall_congr (λ hq, _)))),
+  rw [mem_bot, commutator_element_eq_one_iff_mul_comm, eq_comm],
+end
+
+variables (H₁ H₂)
+
+lemma commutator_comm_le : ⁅H₁, H₂⁆ ≤ ⁅H₂, H₁⁆ :=
+commutator_le.mpr (λ g₁ h₁ g₂ h₂,
+  commutator_element_inv g₂ g₁ ▸ ⁅H₂, H₁⁆.inv_mem_iff.mpr (commutator_mem_commutator h₂ h₁))
+
+lemma commutator_comm : ⁅H₁, H₂⁆ = ⁅H₂, H₁⁆ :=
+le_antisymm (commutator_comm_le H₁ H₂) (commutator_comm_le H₂ H₁)
+
+section normal
+
+instance commutator_normal [h₁ : H₁.normal] [h₂ : H₂.normal] : normal ⁅H₁, H₂⁆ :=
 begin
   let base : set G := {x | ∃ (g₁ ∈ H₁) (g₂ ∈ H₂), ⁅g₁, g₂⁆ = x},
   change (closure base).normal,
@@ -80,46 +100,28 @@ begin
   exact ⟨_, h₁.conj_mem c hc d, _, h₂.conj_mem e he d, (conjugate_commutator_element c e d).symm⟩,
 end
 
-lemma commutator_mono {H₁ H₂ K₁ K₂ : subgroup G} (h₁ : H₁ ≤ K₁) (h₂ : H₂ ≤ K₂) :
-  ⁅H₁, H₂⁆ ≤ ⁅K₁, K₂⁆ :=
-commutator_le.mpr (λ g₁ hg₁ g₂ hg₂, commutator_mem_commutator (h₁ hg₁) (h₂ hg₂))
-
-lemma commutator_def' (H₁ H₂ : subgroup G) [H₁.normal] [H₂.normal] :
+lemma commutator_def' [H₁.normal] [H₂.normal] :
   ⁅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_comm_le (H₁ H₂ : subgroup G) : ⁅H₁, H₂⁆ ≤ ⁅H₂, H₁⁆ :=
-commutator_le.mpr (λ g₁ h₁ g₂ h₂,
-  commutator_element_inv g₂ g₁ ▸ ⁅H₂, H₁⁆.inv_mem_iff.mpr (commutator_mem_commutator h₂ h₁))
-
-lemma commutator_comm (H₁ H₂ : subgroup G) : ⁅H₁, H₂⁆ = ⁅H₂, H₁⁆ :=
-le_antisymm (commutator_comm_le H₁ H₂) (commutator_comm_le H₂ H₁)
-
-lemma commutator_eq_bot_iff_le_centralizer {H₁ H₂ : subgroup G} :
-  ⁅H₁, H₂⁆ = ⊥ ↔ H₁ ≤ H₂.centralizer :=
-begin
-  rw [eq_bot_iff, commutator_le],
-  refine forall_congr (λ p, forall_congr (λ hp, forall_congr (λ q, forall_congr (λ hq, _)))),
-  rw [mem_bot, commutator_element_eq_one_iff_mul_comm, eq_comm],
-end
-
-lemma commutator_le_right (H₁ H₂ : subgroup G) [h : normal H₂] : ⁅H₁, H₂⁆ ≤ H₂ :=
+lemma commutator_le_right [h : H₂.normal] : ⁅H₁, H₂⁆ ≤ H₂ :=
 commutator_le.mpr (λ g₁ h₁ g₂ h₂, H₂.mul_mem (h.conj_mem g₂ h₂ g₁) (H₂.inv_mem h₂))
 
-lemma commutator_le_left (H₁ H₂ : subgroup G) [h : normal H₁] : ⁅H₁, H₂⁆ ≤ H₁ :=
+lemma commutator_le_left [H₁.normal] : ⁅H₁, H₂⁆ ≤ H₁ :=
 commutator_comm H₂ H₁ ▸ commutator_le_right H₂ H₁
 
-@[simp] lemma commutator_bot_left (H : subgroup G) : ⁅(⊥ : subgroup G), H⁆ = ⊥ :=
-le_bot_iff.mp (commutator_le_left ⊥ H)
+@[simp] lemma commutator_bot_left : ⁅(⊥ : subgroup G), H₁⁆ = ⊥ :=
+le_bot_iff.mp (commutator_le_left ⊥ H₁)
 
-@[simp] lemma commutator_bot_right (H : subgroup G) : ⁅H, ⊥⁆ = (⊥ : subgroup G) :=
-le_bot_iff.mp (commutator_le_right H ⊥)
+@[simp] lemma commutator_bot_right : ⁅H₁, ⊥⁆ = (⊥ : subgroup G) :=
+le_bot_iff.mp (commutator_le_right H₁ ⊥)
 
-lemma commutator_le_inf (H₁ H₂ : subgroup G) [normal H₁] [normal H₂] : ⁅H₁, H₂⁆ ≤ H₁ ⊓ H₂ :=
+lemma commutator_le_inf [normal H₁] [normal H₂] : ⁅H₁, H₂⁆ ≤ H₁ ⊓ H₂ :=
 le_inf (commutator_le_left H₁ H₂) (commutator_le_right H₁ H₂)
 
-lemma map_commutator {G₂ : Type*} [group G₂] (f : G →* G₂) (H₁ H₂ : subgroup G)  :
-  map f ⁅H₁, H₂⁆ = ⁅map f H₁, map f H₂⁆ :=
+end normal
+
+lemma map_commutator (f : G →* G') : map f ⁅H₁, H₂⁆ = ⁅map f H₁, map f H₂⁆ :=
 begin
   simp_rw [le_antisymm_iff, map_le_iff_le_comap, commutator_le, mem_comap, map_commutator_element],
   split,
@@ -130,9 +132,8 @@ begin
     exact mem_map_of_mem _ (commutator_mem_commutator hp hq) }
 end
 
-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₂⁆ :=
+lemma commutator_prod_prod (K₁ K₂ : subgroup G') :
+  ⁅H₁.prod K₁, H₂.prod K₂⁆ = ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆ :=
 begin
   apply le_antisymm,
   { rw commutator_le,