chore(GroupTheory/Subgroup/Centralizer): replace centralizer (zpowers s) with centralizer {s} (#30768)

This PR fixes some lingering technical debt from two years ago: leanprover-community/mathlib3#18965

Co-authored-by: tb65536 <thomas.l.browning@gmail.com>

Author: tb65536

Mathlib/Algebra/Group/Subgroup/Pointwise.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.Group.Action.End
 public import Mathlib.Algebra.Group.Pointwise.Set.Lattice
 public import Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
+public import Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
 public import Mathlib.Algebra.Group.Submonoid.Pointwise
 public import Mathlib.GroupTheory.GroupAction.ConjAct
 

Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean

@@ -5,10 +5,10 @@ Authors: Chris Hughes
 -/
 module
 
+public import Mathlib.Algebra.Group.Subgroup.Ker
 public import Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
 public import Mathlib.Data.Countable.Basic
 public import Mathlib.Data.Int.Cast.Lemmas
-public import Mathlib.GroupTheory.Subgroup.Centralizer
 
 /-!
 # Subgroups generated by an element
@@ -59,28 +59,3 @@ end AddSubgroup
     (Int.castAddHom A).range = AddSubgroup.zmultiples 1 := by
   ext a
   simp_rw [AddMonoidHom.mem_range, Int.coe_castAddHom, AddSubgroup.mem_zmultiples_iff, zsmul_one]
-
-namespace Subgroup
-
-variable {s : Set G} {g : G}
-
-@[to_additive]
-theorem centralizer_closure (S : Set G) :
-    centralizer (closure S : Set G) = ⨅ g ∈ S, centralizer (zpowers g : Set G) :=
-  le_antisymm
-      (le_iInf fun _ => le_iInf fun hg => centralizer_le <| zpowers_le.2 <| subset_closure hg) <|
-    le_centralizer_iff.1 <|
-      (closure_le _).2 fun g =>
-        SetLike.mem_coe.2 ∘ zpowers_le.1 ∘ le_centralizer_iff.1 ∘ iInf_le_of_le g ∘ iInf_le _
-
-@[to_additive]
-theorem center_eq_iInf (S : Set G) (hS : closure S = ⊤) :
-    center G = ⨅ g ∈ S, centralizer (zpowers g) := by
-  rw [← centralizer_univ, ← coe_top, ← hS, centralizer_closure]
-
-@[to_additive]
-theorem center_eq_infi' (S : Set G) (hS : closure S = ⊤) :
-    center G = ⨅ g : S, centralizer (zpowers (g : G)) := by
-  rw [center_eq_iInf S hS, ← iInf_subtype'']
-
-end Subgroup

Mathlib/GroupTheory/Finiteness.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Algebra.Group.Pointwise.Set.Finite
 public import Mathlib.Algebra.Group.Subgroup.Pointwise
+import Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
 public import Mathlib.Algebra.Group.Submonoid.BigOperators
 public import Mathlib.GroupTheory.FreeGroup.Basic
 public import Mathlib.GroupTheory.QuotientGroup.Defs

Mathlib/GroupTheory/GroupAction/ConjAct.lean

@@ -5,7 +5,6 @@ Authors: Chris Hughes
 -/
 module
 
-public import Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
 public import Mathlib.Data.Fintype.Card
 public import Mathlib.GroupTheory.GroupAction.Defs
 public import Mathlib.GroupTheory.Subgroup.Centralizer
@@ -207,9 +206,9 @@ theorem orbit_eq_carrier_conjClasses (g : G) :
   rw [ConjClasses.mem_carrier_iff_mk_eq, ConjClasses.mk_eq_mk_iff_isConj, mem_orbit_conjAct]
 
 theorem stabilizer_eq_centralizer (g : G) :
-    stabilizer (ConjAct G) g = centralizer (zpowers (toConjAct g) : Set (ConjAct G)) :=
-  le_antisymm (le_centralizer_iff.mp (zpowers_le.mpr fun _ => mul_inv_eq_iff_eq_mul.mp)) fun _ h =>
-    mul_inv_eq_of_eq_mul (h g (mem_zpowers g)).symm
+    stabilizer (ConjAct G) g = centralizer {toConjAct g} :=
+  le_antisymm (fun _ hg _ h ↦ h ▸ eq_mul_inv_iff_mul_eq.mp hg.symm) fun _ h =>
+    mul_inv_eq_of_eq_mul (h g rfl).symm
 
 theorem _root_.Subgroup.centralizer_eq_comap_stabilizer (g : G) :
     Subgroup.centralizer {g} = Subgroup.comap ConjAct.toConjAct.toMonoidHom

Mathlib/GroupTheory/GroupAction/Quotient.lean

@@ -6,14 +6,14 @@ Authors: Chris Hughes, Thomas Browning
 module
 
 public import Mathlib.Algebra.Group.Subgroup.Actions
-public import Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
 public import Mathlib.Data.Fintype.BigOperators
 public import Mathlib.Dynamics.PeriodicPts.Defs
 public import Mathlib.GroupTheory.Commutator.Basic
 public import Mathlib.GroupTheory.Coset.Basic
 public import Mathlib.GroupTheory.GroupAction.Basic
 public import Mathlib.GroupTheory.GroupAction.ConjAct
 public import Mathlib.GroupTheory.GroupAction.Hom
+public import Mathlib.GroupTheory.Subgroup.Centralizer
 
 /-!
 # Properties of group actions involving quotient groups
@@ -435,7 +435,7 @@ 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 :=
+    G ⧸ centralizer {g} ↪ commutatorSet G :=
   ((MulAction.orbitEquivQuotientStabilizer (ConjAct G) g).trans
             (quotientEquivOfEq (ConjAct.stabilizer_eq_centralizer g))).symm.toEmbedding.trans
     ⟨fun x =>
@@ -452,7 +452,7 @@ theorem quotientCentralizerEmbedding_apply (g : G) (x : G) :
 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
+  (quotientEquivOfEq (center_eq_infi' hS)).toEmbedding.trans
     ((quotientiInfEmbedding _).trans
       (Function.Embedding.piCongrRight fun g => quotientCentralizerEmbedding (g : G)))
 

Mathlib/GroupTheory/Index.lean

@@ -6,6 +6,7 @@ Authors: Thomas Browning
 module
 
 public import Mathlib.Algebra.BigOperators.GroupWithZero.Finset
+public import Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
 public import Mathlib.Algebra.GroupWithZero.Subgroup
 public import Mathlib.Data.Finite.Card
 public import Mathlib.Data.Finite.Prod

Mathlib/GroupTheory/Subgroup/Centralizer.lean

@@ -102,6 +102,26 @@ lemma closure_le_centralizer_centralizer (s : Set G) :
     closure s ≤ centralizer (centralizer s) :=
   closure_le _ |>.mpr Set.subset_centralizer_centralizer
 
+@[to_additive]
+theorem centralizer_closure (s : Set G) : centralizer (closure s) = centralizer s :=
+  le_antisymm (centralizer_le subset_closure)
+    (le_centralizer_iff.mp (closure_le_centralizer_centralizer s))
+
+@[to_additive]
+theorem centralizer_eq_iInf (s : Set G) : centralizer s = ⨅ g ∈ s, centralizer {g} :=
+  le_antisymm (le_iInf₂ fun g hg ↦ centralizer_le (Set.singleton_subset_iff.mpr hg)) fun x hx ↦ by
+    simpa only [mem_iInf, mem_centralizer_singleton_iff, eq_comm (a := x * _)] using hx
+
+@[to_additive]
+theorem center_eq_iInf {s : Set G} (hs : closure s = ⊤) :
+    center G = ⨅ g ∈ s, centralizer {g} := by
+  rw [← centralizer_univ, ← coe_top, ← hs, centralizer_closure, centralizer_eq_iInf]
+
+@[to_additive]
+theorem center_eq_infi' {s : Set G} (hs : closure s = ⊤) :
+    center G = ⨅ g : s, centralizer {(g : G)} := by
+  rw [center_eq_iInf hs, ← iInf_subtype'']
+
 /-- If all the elements of a set `s` commute, then `closure s` is a commutative group. -/
 @[to_additive
 /-- If all the elements of a set `s` commute, then `closure s` is an additive commutative group. -/]

Mathlib/RingTheory/Ideal/Operations.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.Algebra.Operations
 public import Mathlib.Algebra.Module.BigOperators
 public import Mathlib.Data.Fintype.Lattice
+public import Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
 public import Mathlib.RingTheory.Coprime.Lemmas
 public import Mathlib.RingTheory.Ideal.Basic
 public import Mathlib.RingTheory.Nilpotent.Defs

Mathlib/Topology/Algebra/Group/SubmonoidClosure.lean

@@ -5,6 +5,7 @@ Authors: Yury Kudryashov
 -/
 module
 
+public import Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
 public import Mathlib.Order.Filter.AtTopBot.Group
 public import Mathlib.Topology.Algebra.Group.Basic
 

Mathlib/Topology/Instances/AddCircle/Defs.lean

@@ -403,7 +403,7 @@ instance : DivisibleBy (AddCircle p) ℤ where
 
 omit [IsStrictOrderedRing 𝕜] in
 @[simp] lemma coe_fract (x : 𝕜) : (↑(Int.fract x) : AddCircle (1 : 𝕜)) = x := by
-  simp [← Int.self_sub_floor]
+  simp [← Int.self_sub_floor, mem_zmultiples_iff]
 
 end FloorRing