[Merged by Bors] - chore(GroupTheory): forward-port leanprover-community/mathlib#18965

Mathlib/GroupTheory/Abelianization.lean

@@ -7,7 +7,7 @@
 import Mathlib.GroupTheory.Commutator
 import Mathlib.GroupTheory.Finiteness
 
-#align_import group_theory.abelianization from "leanprover-community/mathlib"@"dc6c365e751e34d100e80fe6e314c3c3e0fd2988"
+#align_import group_theory.abelianization from "leanprover-community/mathlib"@"4be589053caf347b899a494da75410deb55fb3ef"
 
 /-!
 # The abelianization of a group
@@ -32,6 +32,8 @@
 -- Let G be a group.
 variable (G : Type u) [Group G]
 
+open Subgroup (centralizer)
+
 /-- The commutator subgroup of a group G is the normal subgroup
   generated by the commutators [p,q]=`p*q*p⁻¹*q⁻¹`. -/
 def commutator : Subgroup G := ⁅(⊤ : Subgroup G), ⊤⁆
@@ -67,11 +69,12 @@
 #align rank_commutator_le_card rank_commutator_le_card
 
 theorem commutator_centralizer_commutator_le_center :
-    ⁅(commutator G).centralizer, (commutator G).centralizer⁆ ≤ Subgroup.center G := by
-  rw [← Subgroup.centralizer_top, ← Subgroup.commutator_eq_bot_iff_le_centralizer]
-  suffices ⁅⁅⊤, (commutator G).centralizer⁆, (commutator G).centralizer⁆ = ⊥ by
+    ⁅centralizer (commutator G : Set G), centralizer (commutator G)⁆ ≤ Subgroup.center G := by
+  rw [← Subgroup.centralizer_univ, ← Subgroup.coe_top, ←
+    Subgroup.commutator_eq_bot_iff_le_centralizer]
+  suffices ⁅⁅⊤, centralizer (commutator G : Set G)⁆, centralizer (commutator G : Set G)⁆ = ⊥ by
     refine' Subgroup.commutator_commutator_eq_bot_of_rotate _ this
-    rwa [Subgroup.commutator_comm (commutator G).centralizer]
+    rwa [Subgroup.commutator_comm (centralizer (commutator G : Set G))]
   rw [Subgroup.commutator_comm, Subgroup.commutator_eq_bot_iff_le_centralizer]
   exact Set.centralizer_subset (Subgroup.commutator_mono le_top le_top)
 #align commutator_centralizer_commutator_le_center commutator_centralizer_commutator_le_center

Mathlib/GroupTheory/Commutator.lean

@@ -8,7 +8,7 @@
 import Mathlib.GroupTheory.Subgroup.Finite
 import Mathlib.Tactic.Group
 
-#align_import group_theory.commutator from "leanprover-community/mathlib"@"0a0ec35061ed9960bf0e7ffb0335f44447b58977"
+#align_import group_theory.commutator from "leanprover-community/mathlib"@"4be589053caf347b899a494da75410deb55fb3ef"
 
 /-!
 # Commutators of Subgroups
@@ -95,7 +95,7 @@
   commutator_le.mpr fun _g₁ hg₁ _g₂ hg₂ => commutator_mem_commutator (h₁ hg₁) (h₂ hg₂)
 #align subgroup.commutator_mono Subgroup.commutator_mono
 
-theorem commutator_eq_bot_iff_le_centralizer : ⁅H₁, H₂⁆ = ⊥ ↔ H₁ ≤ H₂.centralizer := by
+theorem commutator_eq_bot_iff_le_centralizer : ⁅H₁, H₂⁆ = ⊥ ↔ H₁ ≤ centralizer H₂ := by
   rw [eq_bot_iff, commutator_le]
   refine'
     forall_congr' fun p => forall_congr' fun _hp => forall_congr' fun q => forall_congr' fun hq => _

Mathlib/GroupTheory/GroupAction/ConjAct.lean

@@ -7,7 +7,7 @@
 import Mathlib.GroupTheory.Subgroup.ZPowers
 import Mathlib.Algebra.GroupRingAction.Basic
 
-#align_import group_theory.group_action.conj_act from "leanprover-community/mathlib"@"d30d31261cdb4d2f5e612eabc3c4bf45556350d5"
+#align_import group_theory.group_action.conj_act from "leanprover-community/mathlib"@"4be589053caf347b899a494da75410deb55fb3ef"
 
 /-!
 # Conjugation action of a group on itself
@@ -279,10 +279,6 @@
     simp only [smul_def]
     simp only [map_mul, mul_assoc, mul_inv_rev, forall_const, «forall»]
 
--- porting note: type class inference fails on `stabilizer_eq_centralizer` below without this
--- shortcut instance
-instance : MulAction (ConjAct G) G := MulDistribMulAction.toMulAction
-
 instance smulCommClass [SMul α G] [SMulCommClass α G G] [IsScalarTower α G G] :
     SMulCommClass α (ConjAct G) G
     where smul_comm a ug g := by rw [smul_def, smul_def, mul_smul_comm, smul_mul_assoc]
@@ -313,7 +309,8 @@
   funext₂ fun g h => by rw [orbitRel_apply, mem_orbit_conjAct]
 #align conj_act.orbit_rel_conj_act ConjAct.orbitRel_conjAct
 
-theorem stabilizer_eq_centralizer (g : G) : stabilizer (ConjAct G) g = (zpowers g).centralizer :=
+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
 #align conj_act.stabilizer_eq_centralizer ConjAct.stabilizer_eq_centralizer

Mathlib/GroupTheory/GroupAction/Quotient.lean

@@ -10,7 +10,7 @@
 import Mathlib.GroupTheory.Commutator
 import Mathlib.GroupTheory.Coset
 
-#align_import group_theory.group_action.quotient from "leanprover-community/mathlib"@"dc6c365e751e34d100e80fe6e314c3c3e0fd2988"
+#align_import group_theory.group_action.quotient from "leanprover-community/mathlib"@"4be589053caf347b899a494da75410deb55fb3ef"
 
 /-!
 # Properties of group actions involving quotient groups

Mathlib/GroupTheory/Subgroup/Basic.lean

@@ -12,7 +12,7 @@
 import Mathlib.Order.Atoms
 import Mathlib.Tactic.ApplyFun
 
-#align_import group_theory.subgroup.basic from "leanprover-community/mathlib"@"d30d31261cdb4d2f5e612eabc3c4bf45556350d5"
+#align_import group_theory.subgroup.basic from "leanprover-community/mathlib"@"4be589053caf347b899a494da75410deb55fb3ef"
 
 /-!
 # Subgroups
@@ -2260,65 +2260,64 @@
 
 section Centralizer
 
+variable {H}
+
 /-- The `centralizer` of `H` is the subgroup of `g : G` commuting with every `h : H`. -/
 @[to_additive
-      "The `centralizer` of `H` is the additive subgroup of `g : G` commuting with
-      every `h : H`."]
-def centralizer : Subgroup G :=
-  { Submonoid.centralizer (H : Set G) with
-    carrier := Set.centralizer H
+      "The `centralizer` of `H` is the additive subgroup of `g : G` commuting with\nevery `h : H`."]
+def centralizer (s : Set G) : Subgroup G :=
+  { Submonoid.centralizer s with
+    carrier := Set.centralizer s
     inv_mem' := Set.inv_mem_centralizer }
 #align subgroup.centralizer Subgroup.centralizer
 #align add_subgroup.centralizer AddSubgroup.centralizer
 
-variable {H}
-
 @[to_additive]
-theorem mem_centralizer_iff {g : G} : g ∈ H.centralizer ↔ ∀ h ∈ H, h * g = g * h :=
+theorem mem_centralizer_iff {g : G} {s : Set G} : g ∈ centralizer s ↔ ∀ h ∈ s, h * g = g * h :=
   Iff.rfl
 #align subgroup.mem_centralizer_iff Subgroup.mem_centralizer_iff
 #align add_subgroup.mem_centralizer_iff AddSubgroup.mem_centralizer_iff
 
 @[to_additive]
-theorem mem_centralizer_iff_commutator_eq_one {g : G} :
-    g ∈ H.centralizer ↔ ∀ h ∈ H, h * g * h⁻¹ * g⁻¹ = 1 := by
+theorem mem_centralizer_iff_commutator_eq_one {g : G} {s : Set G} :
+    g ∈ centralizer s ↔ ∀ h ∈ s, h * g * h⁻¹ * g⁻¹ = 1 := by
   simp only [mem_centralizer_iff, mul_inv_eq_iff_eq_mul, one_mul]
 #align subgroup.mem_centralizer_iff_commutator_eq_one Subgroup.mem_centralizer_iff_commutator_eq_one
 #align add_subgroup.mem_centralizer_iff_commutator_eq_zero AddSubgroup.mem_centralizer_iff_commutator_eq_zero
 
 @[to_additive]
-theorem centralizer_top : centralizer ⊤ = center G :=
+theorem centralizer_univ : centralizer Set.univ = center G :=
   SetLike.ext' (Set.centralizer_univ G)
-#align subgroup.centralizer_top Subgroup.centralizer_top
-#align add_subgroup.centralizer_top AddSubgroup.centralizer_top
+#align subgroup.centralizer_univ Subgroup.centralizer_univ
+#align add_subgroup.centralizer_univ AddSubgroup.centralizer_univ
 
 @[to_additive]
-theorem le_centralizer_iff : H ≤ K.centralizer ↔ K ≤ H.centralizer :=
+theorem le_centralizer_iff : H ≤ centralizer K ↔ K ≤ centralizer H :=
   ⟨fun h x hx _y hy => (h hy x hx).symm, fun h x hx _y hy => (h hy x hx).symm⟩
 #align subgroup.le_centralizer_iff Subgroup.le_centralizer_iff
 #align add_subgroup.le_centralizer_iff AddSubgroup.le_centralizer_iff
 
 @[to_additive]
 theorem center_le_centralizer (s) : center G ≤ centralizer s :=
-  Set.center_subset_centralizer (s : Set G)
+  Set.center_subset_centralizer s
 #align subgroup.center_le_centralizer Subgroup.center_le_centralizer
 #align add_subgroup.center_le_centralizer AddSubgroup.center_le_centralizer
 
 @[to_additive]
-theorem centralizer_le (h : H ≤ K) : centralizer K ≤ centralizer H :=
+theorem centralizer_le {s t : Set G} (h : s ⊆ t) : centralizer t ≤ centralizer s :=
   Submonoid.centralizer_le h
 #align subgroup.centralizer_le Subgroup.centralizer_le
 #align add_subgroup.centralizer_le AddSubgroup.centralizer_le
 
 @[to_additive (attr := simp)]
-theorem centralizer_eq_top_iff_subset {s} : centralizer s = ⊤ ↔ s ≤ center G :=
+theorem centralizer_eq_top_iff_subset {s : Set G} : centralizer s = ⊤ ↔ s ⊆ center G :=
   SetLike.ext'_iff.trans Set.centralizer_eq_top_iff_subset
 #align subgroup.centralizer_eq_top_iff_subset Subgroup.centralizer_eq_top_iff_subset
 #align add_subgroup.centralizer_eq_top_iff_subset AddSubgroup.centralizer_eq_top_iff_subset
 
 @[to_additive]
 instance Centralizer.characteristic [hH : H.Characteristic] :
-    H.centralizer.Characteristic := by
+    (centralizer (H : Set G)).Characteristic := by
   refine' Subgroup.characteristic_iff_comap_le.mpr fun ϕ g hg h hh => ϕ.injective _
   rw [map_mul, map_mul]
   exact hg (ϕ h) (Subgroup.characteristic_iff_le_comap.mp hH ϕ hh)
@@ -2384,14 +2383,14 @@
 #align add_subgroup.add_subgroup_of_is_commutative AddSubgroup.addSubgroupOf_isCommutative
 
 @[to_additive]
-theorem le_centralizer_iff_isCommutative : K ≤ K.centralizer ↔ K.IsCommutative :=
+theorem le_centralizer_iff_isCommutative : K ≤ centralizer K ↔ K.IsCommutative :=
   ⟨fun h => ⟨⟨fun x y => Subtype.ext (h y.2 x x.2)⟩⟩,
     fun h x hx y hy => congr_arg Subtype.val (h.1.1 ⟨y, hy⟩ ⟨x, hx⟩)⟩
 #align subgroup.le_centralizer_iff_is_commutative Subgroup.le_centralizer_iff_isCommutative
 #align add_subgroup.le_centralizer_iff_is_commutative AddSubgroup.le_centralizer_iff_isCommutative
 
 @[to_additive]
-theorem le_centralizer [h : H.IsCommutative] : H ≤ H.centralizer :=
+theorem le_centralizer [h : H.IsCommutative] : H ≤ centralizer H :=
   le_centralizer_iff_isCommutative.mpr h
 #align subgroup.le_centralizer Subgroup.le_centralizer
 #align add_subgroup.le_centralizer AddSubgroup.le_centralizer

Mathlib/GroupTheory/Subgroup/ZPowers.lean

@@ -5,7 +5,7 @@
 -/
 import Mathlib.GroupTheory.Subgroup.Basic
 
-#align_import group_theory.subgroup.zpowers from "leanprover-community/mathlib"@"e655e4ea5c6d02854696f97494997ba4c31be802"
+#align_import group_theory.subgroup.zpowers from "leanprover-community/mathlib"@"4be589053caf347b899a494da75410deb55fb3ef"
 
 /-!
 # Subgroups generated by an element
@@ -225,7 +225,7 @@
 
 @[to_additive]
 theorem centralizer_closure (S : Set G) :
-    (closure S).centralizer = ⨅ g ∈ S, (zpowers g).centralizer :=
+    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 <|
@@ -237,7 +237,7 @@
 @[to_additive]
 theorem center_eq_iInf (S : Set G) (hS : closure S = ⊤) :
     center G = ⨅ g ∈ S, centralizer (zpowers g) := by
-  rw [← centralizer_top, ← hS, centralizer_closure]
+  rw [← centralizer_univ, ← coe_top, ← hS, centralizer_closure]
 #align subgroup.center_eq_infi Subgroup.center_eq_iInf
 #align add_subgroup.center_eq_infi AddSubgroup.center_eq_iInf
 

Mathlib/GroupTheory/Sylow.lean

@@ -10,7 +10,7 @@
 import Mathlib.GroupTheory.NoncommPiCoprod
 import Mathlib.Order.Atoms.Finite
 
-#align_import group_theory.sylow from "leanprover-community/mathlib"@"bd365b1a4901dbd878e86cb146c2bd86533df468"
+#align_import group_theory.sylow from "leanprover-community/mathlib"@"4be589053caf347b899a494da75410deb55fb3ef"
 
 /-!
 # Sylow theorems
@@ -370,17 +370,18 @@
 #align sylow.stabilizer_eq_normalizer Sylow.stabilizer_eq_normalizer
 
 theorem Sylow.conj_eq_normalizer_conj_of_mem_centralizer [Fact p.Prime] [Finite (Sylow p G)]
-    (P : Sylow p G) (x g : G) (hx : x ∈ (P : Subgroup G).centralizer)
-    (hy : g⁻¹ * x * g ∈ (P : Subgroup G).centralizer) :
+    (P : Sylow p G) (x g : G) (hx : x ∈ centralizer (P : Set G))
+    (hy : g⁻¹ * x * g ∈ centralizer (P : Set G)) :
     ∃ n ∈ (P : Subgroup G).normalizer, g⁻¹ * x * g = n⁻¹ * x * n := by
-  have h1 : ↑P ≤ (zpowers x).centralizer := by rwa [le_centralizer_iff, zpowers_le]
-  have h2 : ↑(g • P) ≤ (zpowers x).centralizer := by
+  have h1 : ↑P ≤ centralizer (zpowers x : Set G) := by rwa [le_centralizer_iff, zpowers_le]
+  have h2 : ↑(g • P) ≤ centralizer (zpowers x : Set G) := by
     rw [le_centralizer_iff, zpowers_le]
     rintro - ⟨z, hz, rfl⟩
     specialize hy z hz
     rwa [← mul_assoc, ← eq_mul_inv_iff_mul_eq, mul_assoc, mul_assoc, mul_assoc, ← mul_assoc,
       eq_inv_mul_iff_mul_eq, ← mul_assoc, ← mul_assoc] at hy
-  obtain ⟨h, hh⟩ := exists_smul_eq (zpowers x).centralizer ((g • P).subtype h2) (P.subtype h1)
+  obtain ⟨h, hh⟩ :=
+    exists_smul_eq (centralizer (zpowers x : Set G)) ((g • P).subtype h2) (P.subtype h1)
   simp_rw [Sylow.smul_subtype, Subgroup.smul_def, smul_smul] at hh
   refine' ⟨h * g, Sylow.smul_eq_iff_mem_normalizer.mp (Sylow.subtype_injective hh), _⟩
   rw [← mul_assoc, Commute.right_comm (h.prop x (mem_zpowers x)), mul_inv_rev, inv_mul_cancel_right]

Mathlib/GroupTheory/Transfer.lean

@@ -6,7 +6,7 @@
 import Mathlib.GroupTheory.Complement
 import Mathlib.GroupTheory.Sylow
 
-#align_import group_theory.transfer from "leanprover-community/mathlib"@"56489b558d42c30f6aac5947cafc9a594f60813b"
+#align_import group_theory.transfer from "leanprover-community/mathlib"@"4be589053caf347b899a494da75410deb55fb3ef"
 
 /-!
 # The Transfer Homomorphism
@@ -209,7 +209,7 @@
 
 section BurnsideTransfer
 
-variable {p : ℕ} (P : Sylow p G) (hP : (P : Subgroup G).normalizer ≤ (P : Subgroup G).centralizer)
+variable {p : ℕ} (P : Sylow p G) (hP : (P : Subgroup G).normalizer ≤ centralizer (P : Set G))
 
 /-- The homomorphism `G →* P` in Burnside's transfer theorem. -/
 noncomputable def transferSylow [FiniteIndex (P : Subgroup G)] : G →* (P : Subgroup G) :=