fix(group_theory/subgroup/basic): generalize centralizer from `subg…

…roup G` to `set G` (#18965)


This is consistent with all the other `sub<foo>.centralizer` definitions.

This generalization reveals that a lot of downstream results are rather strangely stated about `zpowers`.
This does not attempt to change these, instead leaving the work for a follow up (either in a later mathlib3 PR or in mathlib4).

src/group_theory/abelianization.lean

@@ -32,6 +32,8 @@ universes u v w
 -- Let G be a group.
 variables (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⁻¹`. -/
 @[derive subgroup.normal]
@@ -64,12 +66,13 @@ begin
 end
 
 lemma commutator_centralizer_commutator_le_center :
-  ⁅(commutator G).centralizer, (commutator G).centralizer⁆ ≤ subgroup.center G :=
+  ⁅centralizer (commutator G : set G), centralizer (commutator G : set G)⁆ ≤ subgroup.center G :=
 begin
-  rw [←subgroup.centralizer_top, ←subgroup.commutator_eq_bot_iff_le_centralizer],
-  suffices : ⁅⁅⊤, (commutator G).centralizer⁆, (commutator G).centralizer⁆ = ⊥,
+  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)⁆ = ⊥,
   { 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),
 end

src/group_theory/commutator.lean

@@ -75,7 +75,7 @@ H₃.closure_le.trans ⟨λ h a b c d, h ⟨a, b, c, d, rfl⟩, λ h g ⟨a, b,
 lemma commutator_mono (h₁ : H₁ ≤ K₁) (h₂ : H₂ ≤ K₂) : ⁅H₁, H₂⁆ ≤ ⁅K₁, K₂⁆ :=
 commutator_le.mpr (λ g₁ hg₁ g₂ hg₂, commutator_mem_commutator (h₁ hg₁) (h₂ hg₂))
 
-lemma commutator_eq_bot_iff_le_centralizer : ⁅H₁, H₂⁆ = ⊥ ↔ H₁ ≤ H₂.centralizer :=
+lemma commutator_eq_bot_iff_le_centralizer : ⁅H₁, H₂⁆ = ⊥ ↔ H₁ ≤ centralizer H₂ :=
 begin
   rw [eq_bot_iff, commutator_le],
   refine forall_congr (λ p, forall_congr (λ hp, forall_congr (λ q, forall_congr (λ hq, _)))),

src/group_theory/group_action/conj_act.lean

@@ -193,7 +193,8 @@ by { rw [is_conj_comm, is_conj_iff, mem_orbit_iff], refl }
 lemma orbit_rel_conj_act : (orbit_rel (conj_act G) G).rel = is_conj :=
 funext₂ $ λ g h, by rw [orbit_rel_apply, mem_orbit_conj_act]
 
-lemma stabilizer_eq_centralizer (g : G) : stabilizer (conj_act G) g = (zpowers g).centralizer :=
+lemma stabilizer_eq_centralizer (g : G) :
+  stabilizer (conj_act G) g = centralizer (zpowers (to_conj_act g) : set (conj_act G)) :=
 le_antisymm (le_centralizer_iff.mp (zpowers_le.mpr (λ x, mul_inv_eq_iff_eq_mul.mp)))
   (λ x h, mul_inv_eq_of_eq_mul (h g (mem_zpowers g)).symm)
 

src/group_theory/group_action/quotient.lean

@@ -290,7 +290,7 @@ open quotient_group
 
 /-- Cosets of the centralizer of an element embed into the set of commutators. -/
 noncomputable def quotient_centralizer_embedding (g : G) :
-  G ⧸ centralizer (zpowers (g : G)) ↪ commutator_set G :=
+  G ⧸ centralizer (zpowers (g : G) : set G) ↪ commutator_set G :=
 ((mul_action.orbit_equiv_quotient_stabilizer (conj_act G) g).trans (quotient_equiv_of_eq
   (conj_act.stabilizer_eq_centralizer g))).symm.to_embedding.trans ⟨λ x, ⟨x * g⁻¹,
   let ⟨_, x, rfl⟩ := x in ⟨x, g, rfl⟩⟩, λ x y, subtype.ext ∘ mul_right_cancel ∘ subtype.ext_iff.mp⟩

src/group_theory/subgroup/basic.lean

@@ -1580,41 +1580,42 @@ normalizer_eq_top.mp (hmax.2 _ (hnc H (lt_top_iff_ne_top.mpr hmax.1)))
 end normalizer
 
 section centralizer
+variables {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 :=
-{ carrier := set.centralizer H,
+def centralizer (s : set G) : subgroup G :=
+{ carrier := set.centralizer s,
   inv_mem' := λ g, set.inv_mem_centralizer,
-  .. submonoid.centralizer ↑H }
-
-variables {H}
+  .. submonoid.centralizer s }
 
-@[to_additive] lemma mem_centralizer_iff {g : G} : g ∈ H.centralizer ↔ ∀ h ∈ H, h * g = g * h :=
+@[to_additive] lemma mem_centralizer_iff {g : G} {s : set G} :
+  g ∈ centralizer s ↔ ∀ h ∈ s, h * g = g * h :=
 iff.rfl
 
-@[to_additive] lemma mem_centralizer_iff_commutator_eq_one {g : G} :
-  g ∈ H.centralizer ↔ ∀ h ∈ H, h * g * h⁻¹ * g⁻¹ = 1 :=
+@[to_additive] lemma 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]
 
-@[to_additive] lemma centralizer_top : centralizer ⊤ = center G :=
+@[to_additive] lemma centralizer_univ : centralizer set.univ = center G :=
 set_like.ext' (set.centralizer_univ G)
 
-@[to_additive] lemma le_centralizer_iff : H ≤ K.centralizer ↔ K ≤ H.centralizer :=
+@[to_additive] lemma le_centralizer_iff : H ≤ centralizer K ↔ K ≤ centralizer H :=
 ⟨λ h x hx y hy, (h hy x hx).symm, λ h x hx y hy, (h hy x hx).symm⟩
 
 @[to_additive] lemma center_le_centralizer (s) : center G ≤ centralizer s :=
 set.center_subset_centralizer s
 
-@[to_additive] lemma centralizer_le (h : H ≤ K) : centralizer K ≤ centralizer H :=
+@[to_additive] lemma centralizer_le {s t : set G} (h : s ⊆ t) : centralizer t ≤ centralizer s :=
 submonoid.centralizer_le h
 
-@[simp, to_additive] lemma centralizer_eq_top_iff_subset {s} : centralizer s = ⊤ ↔ s ≤ center G :=
+@[simp, to_additive] lemma centralizer_eq_top_iff_subset {s : set G} :
+  centralizer s = ⊤ ↔ s ⊆ center G :=
 set_like.ext'_iff.trans set.centralizer_eq_top_iff_subset
 
 @[to_additive] instance subgroup.centralizer.characteristic [hH : H.characteristic] :
-  H.centralizer.characteristic :=
+  (centralizer (H : set G)).characteristic :=
 begin
   refine subgroup.characteristic_iff_comap_le.mpr (λ ϕ g hg h hh, ϕ.injective _),
   rw [map_mul, map_mul],
@@ -1663,10 +1664,10 @@ end⟩⟩
   (H.subgroup_of K).is_commutative :=
 H.comap_injective_is_commutative subtype.coe_injective
 
-@[to_additive] lemma le_centralizer_iff_is_commutative : K ≤ K.centralizer ↔ K.is_commutative :=
+@[to_additive] lemma le_centralizer_iff_is_commutative : K ≤ centralizer K ↔ K.is_commutative :=
 ⟨λ h, ⟨⟨λ x y, subtype.ext (h y.2 x x.2)⟩⟩, λ h x hx y hy, congr_arg coe (h.1.1 ⟨y, hy⟩ ⟨x, hx⟩)⟩
 
-@[to_additive] lemma le_centralizer [h : H.is_commutative] : H ≤ H.centralizer :=
+@[to_additive] lemma le_centralizer [h : H.is_commutative] : H ≤ centralizer H :=
 le_centralizer_iff_is_commutative.mpr h
 
 end subgroup

src/group_theory/subgroup/zpowers.lean

@@ -166,17 +166,19 @@ zpowers_eq_bot.not
 subgroup.zpowers_eq_bot.mpr rfl
 
 @[to_additive] lemma centralizer_closure (S : set G) :
-  (closure S).centralizer = ⨅ g ∈ S, (zpowers g).centralizer :=
-le_antisymm (le_infi $ λ g, le_infi $ λ hg, centralizer_le $ zpowers_le.2 $ subset_closure hg)
+  centralizer (closure S : set G) = ⨅ g ∈ S, centralizer (zpowers g : set G) :=
+le_antisymm
+  (le_infi $ λ g, le_infi $ λ hg, centralizer_le $ set_like.coe_subset_coe.2 $
+    zpowers_le.2 $ subset_closure hg)
   $ le_centralizer_iff.1 $ (closure_le _).2
   $ λ g, set_like.mem_coe.2 ∘ zpowers_le.1 ∘ le_centralizer_iff.1 ∘ infi_le_of_le g ∘ infi_le _
 
 @[to_additive] lemma center_eq_infi (S : set G) (hS : closure S = ⊤) :
   center G = ⨅ g ∈ S, centralizer (zpowers g) :=
-by rw [←centralizer_top, ←hS, centralizer_closure]
+by rw [←centralizer_univ, ←coe_top, ←hS, centralizer_closure]
 
 @[to_additive] lemma center_eq_infi' (S : set G) (hS : closure S = ⊤) :
-  center G = ⨅ g : S, centralizer (zpowers g) :=
+  center G = ⨅ g : S, centralizer (zpowers (g : G) : set G) :=
 by rw [center_eq_infi S hS, ←infi_subtype'']
 
 end subgroup

src/group_theory/sylow.lean

@@ -302,18 +302,19 @@ ext (λ g, sylow.smul_eq_iff_mem_normalizer)
 
 lemma 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) :
+  (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 :=
 begin
-  have h1 : ↑P ≤ (zpowers x).centralizer,
+  have h1 : ↑P ≤ centralizer (zpowers x : set G),
   { rwa [le_centralizer_iff, zpowers_le] },
-  have h2 : ↑(g • P) ≤ (zpowers x).centralizer,
+  have h2 : ↑(g • P) ≤ centralizer (zpowers x : set G),
   { rw [le_centralizer_iff, zpowers_le],
     rintros - ⟨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, 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]
@@ -322,7 +323,8 @@ end
 lemma sylow.conj_eq_normalizer_conj_of_mem [fact p.prime] [finite (sylow p G)] (P : sylow p G)
   [hP : (P : subgroup G).is_commutative] (x g : G) (hx : x ∈ P) (hy : g⁻¹ * x * g ∈ P) :
   ∃ n ∈ (P : subgroup G).normalizer, g⁻¹ * x * g = n⁻¹ * x * n :=
-P.conj_eq_normalizer_conj_of_mem_centralizer x g (le_centralizer P hx) (le_centralizer P hy)
+P.conj_eq_normalizer_conj_of_mem_centralizer x g
+  (le_centralizer (P : subgroup G) hx : _) (le_centralizer (P : subgroup G) hy : _)
 
 /-- Sylow `p`-subgroups are in bijection with cosets of the normalizer of a Sylow `p`-subgroup -/
 noncomputable def sylow.equiv_quotient_normalizer [fact p.prime] [fintype (sylow p G)]

src/group_theory/transfer.lean

@@ -172,7 +172,7 @@ rfl
 
 section burnside_transfer
 
-variables {p : ℕ} (P : sylow p G) (hP : (P : subgroup G).normalizer ≤ (P : subgroup G).centralizer)
+variables {p : ℕ} (P : sylow p G) (hP : (P : subgroup G).normalizer ≤ centralizer (P : set G))
 
 include hP