GroupTheory.GroupAction.Quotient no field

Mathlib/GroupTheory/Commutator/Basic.lean

@@ -3,6 +3,7 @@ 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
 
@@ -210,3 +211,36 @@ 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/GroupAction/Quotient.lean

@@ -4,10 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Thomas Browning
 -/
 import Mathlib.Algebra.Group.Subgroup.Actions
-import Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
 import Mathlib.Data.Fintype.BigOperators
 import Mathlib.Dynamics.PeriodicPts.Lemmas
-import Mathlib.GroupTheory.Commutator.Basic
 import Mathlib.GroupTheory.Coset.Basic
 import Mathlib.GroupTheory.GroupAction.Basic
 import Mathlib.GroupTheory.GroupAction.ConjAct
@@ -24,6 +22,8 @@ This file proves properties of group actions which use the quotient group constr
 as well as their analogues for additive groups.
 -/
 
+assert_not_exists Field
+
 universe u v w
 
 variable {α : Type u} {β : Type v} {γ : Type w}
@@ -483,33 +483,4 @@ theorem normalCore_eq_ker : H.normalCore = (MulAction.toPermHom G (G ⧸ H)).ker
     rw [← H.inv_mem_iff, ← mul_one g⁻¹, ← QuotientGroup.eq, ← mul_one g]
     exact (MulAction.Quotient.smul_mk H g 1).symm.trans (Equiv.Perm.ext_iff.mp hg (1 : G))
 
-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