more

Mathlib.lean

@@ -3234,7 +3234,7 @@ import Mathlib.GroupTheory.ArchimedeanDensely
 import Mathlib.GroupTheory.ClassEquation
 import Mathlib.GroupTheory.Commensurable
 import Mathlib.GroupTheory.Commutator.Basic
-import Mathlib.GroupTheory.Commutator.Finite
+import Mathlib.GroupTheory.Commutator.Lemmas
 import Mathlib.GroupTheory.CommutingProbability
 import Mathlib.GroupTheory.Complement
 import Mathlib.GroupTheory.Congruence.Basic

Mathlib/GroupTheory/Commutator/Basic.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Jordan Brown, Thomas Browning, Patrick Lutz. All rights reser
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jordan Brown, Thomas Browning, Patrick Lutz
 -/
-import Mathlib.GroupTheory.GroupAction.Quotient
 import Mathlib.GroupTheory.Subgroup.Centralizer
 import Mathlib.Tactic.Group
 
@@ -211,36 +210,3 @@ theorem mem_commutatorSet_iff : g ∈ commutatorSet G ↔ ∃ g₁ g₂ : G, ⁅
 
 theorem commutator_mem_commutatorSet : ⁅g₁, g₂⁆ ∈ commutatorSet G :=
   ⟨g₁, g₂, rfl⟩
-
-namespace Subgroup
-
-open QuotientGroup
-
-/-- Cosets of the centralizer of an element embed into the set of commutators. -/
-noncomputable def quotientCentralizerEmbedding (g : G) :
-    G ⧸ centralizer (zpowers (g : G)) ↪ commutatorSet G :=
-  ((MulAction.orbitEquivQuotientStabilizer (ConjAct G) g).trans
-            (quotientEquivOfEq (ConjAct.stabilizer_eq_centralizer g))).symm.toEmbedding.trans
-    ⟨fun x =>
-      ⟨x * g⁻¹,
-        let ⟨_, x, rfl⟩ := x
-        ⟨x, g, rfl⟩⟩,
-      fun _ _ => Subtype.ext ∘ mul_right_cancel ∘ Subtype.ext_iff.mp⟩
-
-theorem quotientCentralizerEmbedding_apply (g : G) (x : G) :
-    quotientCentralizerEmbedding g x = ⟨⁅x, g⁆, x, g, rfl⟩ :=
-  rfl
-
-/-- If `G` is generated by `S`, then the quotient by the center embeds into `S`-indexed sequences
-of commutators. -/
-noncomputable def quotientCenterEmbedding {S : Set G} (hS : closure S = ⊤) :
-    G ⧸ center G ↪ S → commutatorSet G :=
-  (quotientEquivOfEq (center_eq_infi' S hS)).toEmbedding.trans
-    ((quotientiInfEmbedding _).trans
-      (Function.Embedding.piCongrRight fun g => quotientCentralizerEmbedding (g : G)))
-
-theorem quotientCenterEmbedding_apply {S : Set G} (hS : closure S = ⊤) (g : G) (s : S) :
-    quotientCenterEmbedding hS g s = ⟨⁅g, s⁆, g, s, rfl⟩ :=
-  rfl
-
-end Subgroup

Mathlib/GroupTheory/Commutator/Lemmas.lean

@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2021 Jordan Brown, Thomas Browning, Patrick Lutz. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jordan Brown, Thomas Browning, Patrick Lutz
+-/
+import Mathlib.Algebra.Group.Subgroup.Finite
+import Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
+import Mathlib.GroupTheory.Commutator.Basic
+import Mathlib.GroupTheory.GroupAction.Quotient
+
+/-!
+# Extra lemmas about commutators
+
+The commutator of a finite direct product is contained in the direct product of the commutators.
+-/
+
+open QuotientGroup
+
+namespace Subgroup
+variable {G : Type*} [Group G]
+
+/-- The commutator of a finite direct product is contained in the direct product of the commutators.
+-/
+theorem commutator_pi_pi_of_finite {η : Type*} [Finite η] {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 fun i => ⁅H i, K i⁆ := by
+  classical
+    apply le_antisymm (commutator_pi_pi_le H K)
+    rw [pi_le_iff]
+    intro i hi
+    rw [map_commutator]
+    apply commutator_mono <;>
+      · rw [le_pi_iff]
+        intro j _hj
+        rintro _ ⟨_, ⟨x, hx, rfl⟩, rfl⟩
+        by_cases h : j = i
+        · subst h
+          simpa using hx
+        · simp [h, one_mem]
+
+/-- Cosets of the centralizer of an element embed into the set of commutators. -/
+noncomputable def quotientCentralizerEmbedding (g : G) :
+    G ⧸ centralizer (zpowers (g : G)) ↪ commutatorSet G :=
+  ((MulAction.orbitEquivQuotientStabilizer (ConjAct G) g).trans
+            (quotientEquivOfEq (ConjAct.stabilizer_eq_centralizer g))).symm.toEmbedding.trans
+    ⟨fun x =>
+      ⟨x * g⁻¹,
+        let ⟨_, x, rfl⟩ := x
+        ⟨x, g, rfl⟩⟩,
+      fun _ _ => Subtype.ext ∘ mul_right_cancel ∘ Subtype.ext_iff.mp⟩
+
+theorem quotientCentralizerEmbedding_apply (g : G) (x : G) :
+    quotientCentralizerEmbedding g x = ⟨⁅x, g⁆, x, g, rfl⟩ :=
+  rfl
+
+/-- If `G` is generated by `S`, then the quotient by the center embeds into `S`-indexed sequences
+of commutators. -/
+noncomputable def quotientCenterEmbedding {S : Set G} (hS : closure S = ⊤) :
+    G ⧸ center G ↪ S → commutatorSet G :=
+  (quotientEquivOfEq (center_eq_infi' S hS)).toEmbedding.trans
+    ((quotientiInfEmbedding _).trans
+      (Function.Embedding.piCongrRight fun g => quotientCentralizerEmbedding (g : G)))
+
+theorem quotientCenterEmbedding_apply {S : Set G} (hS : closure S = ⊤) (g : G) (s : S) :
+    quotientCenterEmbedding hS g s = ⟨⁅g, s⁆, g, s, rfl⟩ :=
+  rfl
+
+end Subgroup

Mathlib/GroupTheory/Index.lean

@@ -6,6 +6,7 @@ Authors: Thomas Browning
 import Mathlib.Algebra.BigOperators.GroupWithZero.Finset
 import Mathlib.Data.Finite.Card
 import Mathlib.Data.Set.Card
+import Mathlib.GroupTheory.Commutator.Lemmas
 import Mathlib.GroupTheory.Coset.Card
 import Mathlib.GroupTheory.Finiteness
 import Mathlib.GroupTheory.GroupAction.Quotient

Mathlib/GroupTheory/Nilpotent.lean

@@ -6,7 +6,7 @@ Authors: Kevin Buzzard, Ines Wright, Joachim Breitner
 import Mathlib.GroupTheory.Solvable
 import Mathlib.GroupTheory.Sylow
 import Mathlib.Algebra.Group.Subgroup.Order
-import Mathlib.GroupTheory.Commutator.Finite
+import Mathlib.GroupTheory.Commutator.Lemmas
 
 /-!