more

Author: YaelDillies

Mathlib/Algebra/Ring/Periodic.lean

@@ -24,7 +24,7 @@ Note that any `c`-antiperiodic function will necessarily also be `2 • c`-perio
 
 period, periodic, periodicity, antiperiodic
 -/
-
+pcommut
 assert_not_exists Field
 
 variable {α β γ : Type*} {f g : α → β} {c c₁ c₂ x : α}

Mathlib/GroupTheory/Commutator/Finite.lean

@@ -4,16 +4,21 @@ 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.Finiteness
+import Mathlib.GroupTheory.GroupAction.Quotient
 import Mathlib.GroupTheory.Index
 
 /-!
+# 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.
 -/
@@ -34,7 +39,34 @@ theorem commutator_pi_pi_of_finite {η : Type*} [Finite η] {Gs : η → Type*}
           simpa using hx
         · simp [h, one_mem]
 
-variable (G : Type*) [Group G] [Group.FG G] [Finite (commutatorSet G)]
+/-- 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
+
+variable [Group.FG G] [Finite (commutatorSet G)]
 
 instance finiteIndex_center : FiniteIndex (center G) := by
   obtain ⟨S, -, hS⟩ := Group.rank_spec G