feat: the bicentralizer of a commutative set is commutative (#18700)

This shows that the bicentralizer (a.k.a. bicommutant) of a commutative set is commutative. Moreover, since `s ⊆ s.centralizer.centralizer`, if `s` is a commutative set, then `closure s ≤ centralizer (centralizer s)` for various subobject closures. Consequently, we obtain simplified proofs that if `s` is commutative, then so is `closure s`.



Co-authored-by: ADedecker <anatolededecker@gmail.com>

Author: j-loreaux

Mathlib/Algebra/Group/Center.lean

@@ -138,6 +138,10 @@ theorem mul_mem_center {z₁ z₂ : M} (hz₁ : z₁ ∈ Set.center M) (hz₂ :
 lemma center_subset_centralizer (S : Set M) : Set.center M ⊆ S.centralizer :=
   fun _ hx m _ ↦ (hx.comm m).symm
 
+@[to_additive addCentralizer_union]
+lemma centralizer_union : centralizer (S ∪ T) = centralizer S ∩ centralizer T := by
+  simp [centralizer, or_imp, forall_and, setOf_and]
+
 @[to_additive (attr := gcongr) addCentralizer_subset]
 lemma centralizer_subset (h : S ⊆ T) : centralizer T ⊆ centralizer S := fun _ ht s hs ↦ ht s (h hs)
 
@@ -161,6 +165,11 @@ lemma centralizer_centralizer_centralizer (S : Set M) :
 instance decidableMemCentralizer [∀ a : M, Decidable <| ∀ b ∈ S, b * a = a * b] :
     DecidablePred (· ∈ centralizer S) := fun _ ↦ decidable_of_iff' _ mem_centralizer_iff
 
+@[to_additive addCentralizer_addCentralizer_comm_of_comm]
+lemma centralizer_centralizer_comm_of_comm (h_comm : ∀ x ∈ S, ∀ y ∈ S, x * y = y * x) :
+    ∀ x ∈ S.centralizer.centralizer, ∀ y ∈ S.centralizer.centralizer, x * y = y * x :=
+  fun _ h₁ _ h₂ ↦ h₂ _ fun _ h₃ ↦ h₁ _ fun _ h₄ ↦ h_comm _ h₄ _ h₃
+
 end Mul
 
 section Semigroup

Mathlib/Algebra/Group/Subgroup/Basic.lean

@@ -436,27 +436,6 @@ theorem closure_closure_coe_preimage {k : Set G} : closure (((↑) : closure k 
     closure_induction (fun _ h ↦ subset_closure h) (one_mem _) (fun _ _ _ _ ↦ mul_mem)
       (fun _ _ ↦ inv_mem) hx'
 
-/-- 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."]
-def closureCommGroupOfComm {k : Set G} (hcomm : ∀ x ∈ k, ∀ y ∈ k, x * y = y * x) :
-    CommGroup (closure k) :=
-  { (closure k).toGroup with
-    mul_comm := fun ⟨x, hx⟩ ⟨y, hy⟩ => by
-      ext
-      simp only [Subgroup.coe_mul]
-      induction hx, hy using closure_induction₂ with
-      | mem x y hx hy => exact hcomm x hx y hy
-      | one_left x _ => exact Commute.one_left x
-      | one_right x _ => exact Commute.one_right x
-      | mul_left _ _ _ _ _ _ h₁ h₂ => exact Commute.mul_left h₁ h₂
-      | mul_right _ _ _ _ _ _ h₁ h₂ => exact Commute.mul_right h₁ h₂
-      | inv_left _ _ _ _ h => -- `Commute.inv_left` is not imported
-        rw [inv_mul_eq_iff_eq_mul, ← mul_assoc, h, mul_assoc, mul_inv_cancel, mul_one]
-      | inv_right _ _ _ _ h =>
-        rw [mul_inv_eq_iff_eq_mul, mul_assoc, h, ← mul_assoc, inv_mul_cancel, one_mul] }
-
 variable (G)
 
 /-- `closure` forms a Galois insertion with the coercion to set. -/

Mathlib/Algebra/Group/Submonoid/Membership.lean

@@ -494,20 +494,6 @@ theorem map_powers {N : Type*} {F : Type*} [Monoid N] [FunLike F M N] [MonoidHom
     (powers m).map f = powers (f m) := by
   simp only [powers_eq_closure, map_mclosure f, Set.image_singleton]
 
-/-- If all the elements of a set `s` commute, then `closure s` is a commutative monoid. -/
-@[to_additive
-      "If all the elements of a set `s` commute, then `closure s` forms an additive
-      commutative monoid."]
-def closureCommMonoidOfComm {s : Set M} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) :
-    CommMonoid (closure s) :=
-  { (closure s).toMonoid with
-    mul_comm := fun x y => by
-      ext
-      simp only [Submonoid.coe_mul]
-      exact closure_induction₂ (fun _ _ h₁ h₂ ↦ hcomm _ h₁ _ h₂) (fun _ _ ↦ Commute.one_left _)
-        (fun _ _ ↦ Commute.one_right _) (fun _ _ _ _ _ _ ↦ Commute.mul_left)
-        (fun _ _ _ _ _ _ ↦ Commute.mul_right) x.prop y.prop }
-
 end Submonoid
 
 @[to_additive]

Mathlib/Algebra/Ring/Subring/Basic.lean

@@ -548,25 +548,17 @@ theorem mem_closure_iff {s : Set R} {x} :
       | mul _ _ _ _ h₁ h₂ => exact add_mem h₁ h₂
       | inv _ _ h => exact neg_mem h⟩
 
+lemma closure_le_centralizer_centralizer (s : Set R) :
+    closure s ≤ centralizer (centralizer s) :=
+  closure_le.mpr Set.subset_centralizer_centralizer
+
 /-- If all elements of `s : Set A` commute pairwise, then `closure s` is a commutative ring. -/
-def closureCommRingOfComm {s : Set R} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) :
+abbrev closureCommRingOfComm {s : Set R} (hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x) :
     CommRing (closure s) :=
   { (closure s).toRing with
-    mul_comm := fun ⟨x, hx⟩ ⟨y, hy⟩ => by
-      ext
-      simp only [MulMemClass.mk_mul_mk]
-      induction hx, hy using closure_induction₂ with
-      | mem_mem x y hx hy => exact hcomm x hx y hy
-      | zero_left x _ => exact Commute.zero_left x
-      | zero_right x _ => exact Commute.zero_right x
-      | one_left x _ => exact Commute.one_left x
-      | one_right x _ => exact Commute.one_right x
-      | mul_left _ _ _ _ _ _ h₁ h₂ => exact Commute.mul_left h₁ h₂
-      | mul_right _ _ _ _ _ _ h₁ h₂ => exact Commute.mul_right h₁ h₂
-      | add_left _ _ _ _ _ _ h₁ h₂ => exact Commute.add_left h₁ h₂
-      | add_right _ _ _ _ _ _ h₁ h₂ => exact Commute.add_right h₁ h₂
-      | neg_left _ _ _ _ h => exact Commute.neg_left h
-      | neg_right _ _ _ _ h => exact Commute.neg_right h }
+    mul_comm := fun ⟨_, h₁⟩ ⟨_, h₂⟩ ↦
+      have := closure_le_centralizer_centralizer s
+      Subtype.ext <| Set.centralizer_centralizer_comm_of_comm hcomm _ (this h₁) _ (this h₂) }
 
 theorem exists_list_of_mem_closure {s : Set R} {x : R} (hx : x ∈ closure s) :
     ∃ L : List (List R), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = (-1 : R)) ∧ (L.map List.prod).sum = x := by

Mathlib/Algebra/Ring/Subsemiring/Basic.lean

@@ -886,23 +886,17 @@ instance center.smulCommClass_left : SMulCommClass (center R') R' R' :=
 instance center.smulCommClass_right : SMulCommClass R' (center R') R' :=
   Submonoid.center.smulCommClass_right
 
-/-- If all the elements of a set `s` commute, then `closure s` is a commutative monoid. -/
-def closureCommSemiringOfComm {s : Set R'} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) :
+lemma closure_le_centralizer_centralizer (s : Set R') :
+    closure s ≤ centralizer (centralizer s) :=
+  closure_le.mpr Set.subset_centralizer_centralizer
+
+/-- If all the elements of a set `s` commute, then `closure s` is a commutative semiring. -/
+abbrev closureCommSemiringOfComm {s : Set R'} (hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x) :
     CommSemiring (closure s) :=
   { (closure s).toSemiring with
-    mul_comm := fun ⟨x, hx⟩ ⟨y, hy⟩ => by
-      ext
-      simp only [MulMemClass.mk_mul_mk]
-      induction hx, hy using closure_induction₂ with
-      | mem_mem x y hx hy => exact hcomm x hx y hy
-      | zero_left x _ => exact Commute.zero_left x
-      | zero_right x _ => exact Commute.zero_right x
-      | one_left x _ => exact Commute.one_left x
-      | one_right x _ => exact Commute.one_right x
-      | mul_left _ _ _ _ _ _ h₁ h₂ => exact Commute.mul_left h₁ h₂
-      | mul_right _ _ _ _ _ _ h₁ h₂ => exact Commute.mul_right h₁ h₂
-      | add_left _ _ _ _ _ _ h₁ h₂ => exact Commute.add_left h₁ h₂
-      | add_right _ _ _ _ _ _ h₁ h₂ => exact Commute.add_right h₁ h₂ }
+    mul_comm := fun ⟨_, h₁⟩ ⟨_, h₂⟩ ↦
+      have := closure_le_centralizer_centralizer s
+      Subtype.ext <| Set.centralizer_centralizer_comm_of_comm hcomm _ (this h₁) _ (this h₂) }
 
 end Subsemiring
 

Mathlib/Algebra/Star/Center.lean

@@ -33,6 +33,19 @@ theorem Set.star_mem_center (ha : a ∈ Set.center R) : star a ∈ Set.center R
     _ = b * star (a * star c) := by rw [star_mul, star_star]
     _ = b * (c * star a) := by rw [star_mul, star_star]
 
+theorem Set.star_centralizer : star s.centralizer = (star s).centralizer := by
+  simp_rw [centralizer, ← commute_iff_eq]
+  conv_lhs => simp only [← star_preimage, preimage_setOf_eq, ← commute_star_comm]
+  conv_rhs => simp only [← image_star, forall_mem_image]
+
+theorem Set.union_star_self_comm (hcomm : ∀ x ∈ s, ∀ y ∈ s, y * x = x * y)
+    (hcomm_star : ∀ x ∈ s, ∀ y ∈ s, y * star x = star x * y) :
+    ∀ x ∈ s ∪ star s, ∀ y ∈ s ∪ star s, y * x = x * y := by
+  change s ∪ star s ⊆ (s ∪ star s).centralizer
+  simp_rw [centralizer_union, ← star_centralizer, union_subset_iff, subset_inter_iff,
+    star_subset_star, star_subset]
+  exact ⟨⟨hcomm, hcomm_star⟩, ⟨hcomm_star, hcomm⟩⟩
+
 theorem Set.star_mem_centralizer' (h : ∀ a : R, a ∈ s → star a ∈ s) (ha : a ∈ Set.centralizer s) :
     star a ∈ Set.centralizer s := fun y hy => by simpa using congr_arg star (ha _ (h _ hy)).symm
 

Mathlib/Algebra/Star/Subalgebra.lean

@@ -265,16 +265,22 @@ def centralizer (s : Set A) : StarSubalgebra R A where
 theorem coe_centralizer (s : Set A) : (centralizer R s : Set A) = (s ∪ star s).centralizer :=
   rfl
 
-theorem mem_centralizer_iff {s : Set A} {z : A} :
+open Set in
+nonrec theorem mem_centralizer_iff {s : Set A} {z : A} :
     z ∈ centralizer R s ↔ ∀ g ∈ s, g * z = z * g ∧ star g * z = z * star g := by
-  show (∀ g ∈ s ∪ star s, g * z = z * g) ↔ ∀ g ∈ s, g * z = z * g ∧ star g * z = z * star g
-  simp only [Set.mem_union, or_imp, forall_and, and_congr_right_iff]
-  exact fun _ =>
-    ⟨fun hz a ha => hz _ (Set.star_mem_star.mpr ha), fun hz a ha => star_star a ▸ hz _ ha⟩
+  simp [← SetLike.mem_coe, centralizer_union, ← image_star, mem_centralizer_iff, forall_and]
 
 theorem centralizer_le (s t : Set A) (h : s ⊆ t) : centralizer R t ≤ centralizer R s :=
   Set.centralizer_subset (Set.union_subset_union h <| Set.preimage_mono h)
 
+theorem centralizer_toSubalgebra (s : Set A) :
+    (centralizer R s).toSubalgebra = Subalgebra.centralizer R (s ∪ star s):=
+  rfl
+
+theorem coe_centralizer_centralizer (s : Set A) :
+    (centralizer R (centralizer R s : Set A)) = (s ∪ star s).centralizer.centralizer := by
+  rw [coe_centralizer, StarMemClass.star_coe_eq, Set.union_self, coe_centralizer]
+
 end Centralizer
 
 end StarSubalgebra
@@ -503,28 +509,29 @@ theorem adjoin_induction_subtype {s : Set A} {p : adjoin R s → Prop} (a : adjo
 
 variable (R)
 
+lemma adjoin_le_centralizer_centralizer (s : Set A) :
+    adjoin R s ≤ centralizer R (centralizer R s) := by
+  rw [← toSubalgebra_le_iff, centralizer_toSubalgebra, adjoin_toSubalgebra]
+  convert Algebra.adjoin_le_centralizer_centralizer R (s ∪ star s)
+  rw [StarMemClass.star_coe_eq]
+  simp
+
 /-- If all elements of `s : Set A` commute pairwise and also commute pairwise with elements of
 `star s`, then `StarSubalgebra.adjoin R s` is commutative. See note [reducible non-instances]. -/
 abbrev adjoinCommSemiringOfComm {s : Set A}
-    (hcomm : ∀ a : A, a ∈ s → ∀ b : A, b ∈ s → a * b = b * a)
-    (hcomm_star : ∀ a : A, a ∈ s → ∀ b : A, b ∈ s → a * star b = star b * a) :
+    (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a)
+    (hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a) :
     CommSemiring (adjoin R s) :=
-  { (adjoin R s).toSubalgebra.toSemiring with
-    mul_comm := by
-      rintro ⟨x, hx⟩ ⟨y, hy⟩
-      ext
-      simp only [MulMemClass.mk_mul_mk]
-      rw [← mem_toSubalgebra, adjoin_toSubalgebra] at hx hy
-      letI : CommSemiring (Algebra.adjoin R (s ∪ star s)) :=
-        Algebra.adjoinCommSemiringOfComm R
-          (by
-            intro a ha b hb
-            cases' ha with ha ha <;> cases' hb with hb hb
-            · exact hcomm _ ha _ hb
-            · exact star_star b ▸ hcomm_star _ ha _ hb
-            · exact star_star a ▸ (hcomm_star _ hb _ ha).symm
-            · simpa only [star_mul, star_star] using congr_arg star (hcomm _ hb _ ha))
-      exact congr_arg Subtype.val (mul_comm (⟨x, hx⟩ : Algebra.adjoin R (s ∪ star s)) ⟨y, hy⟩) }
+  { (adjoin R s).toSemiring with
+    mul_comm := fun ⟨_, h₁⟩ ⟨_, h₂⟩ ↦ by
+      have hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a := fun a ha b hb ↦
+        Set.union_star_self_comm (fun _ ha _ hb ↦ hcomm _ hb _ ha)
+          (fun _ ha _ hb ↦ hcomm_star _ hb _ ha) b hb a ha
+      have := adjoin_le_centralizer_centralizer R s
+      apply this at h₁
+      apply this at h₂
+      rw [← SetLike.mem_coe, coe_centralizer_centralizer] at h₁ h₂
+      exact Subtype.ext <| Set.centralizer_centralizer_comm_of_comm hcomm _ h₁ _ h₂ }
 
 /-- If all elements of `s : Set A` commute pairwise and also commute pairwise with elements of
 `star s`, then `StarSubalgebra.adjoin R s` is commutative. See note [reducible non-instances]. -/

Mathlib/GroupTheory/Subgroup/Centralizer.lean

@@ -77,4 +77,21 @@ variable (H)
 theorem le_centralizer [h : H.IsCommutative] : H ≤ centralizer H :=
   le_centralizer_iff_isCommutative.mpr h
 
+variable {H} in
+@[to_additive]
+lemma closure_le_centralizer_centralizer (s : Set G) :
+    closure s ≤ centralizer (centralizer s) :=
+  closure_le _ |>.mpr Set.subset_centralizer_centralizer
+
+/-- 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."]
+abbrev closureCommGroupOfComm {k : Set G} (hcomm : ∀ x ∈ k, ∀ y ∈ k, x * y = y * x) :
+    CommGroup (closure k) :=
+  { (closure k).toGroup with
+    mul_comm := fun ⟨_, h₁⟩ ⟨_, h₂⟩ ↦
+      have := closure_le_centralizer_centralizer k
+      Subtype.ext <| Set.centralizer_centralizer_comm_of_comm hcomm _ (this h₁) _ (this h₂) }
+
 end Subgroup

Mathlib/GroupTheory/Submonoid/Centralizer.lean

@@ -88,6 +88,23 @@ lemma centralizer_centralizer_centralizer {s : Set M} :
   apply SetLike.coe_injective
   simp only [coe_centralizer, Set.centralizer_centralizer_centralizer]
 
+variable {M} in
+@[to_additive]
+lemma closure_le_centralizer_centralizer (s : Set M) :
+    closure s ≤ centralizer (centralizer s) :=
+  closure_le.mpr Set.subset_centralizer_centralizer
+
+/-- If all the elements of a set `s` commute, then `closure s` is a commutative monoid. -/
+@[to_additive
+      "If all the elements of a set `s` commute, then `closure s` forms an additive
+      commutative monoid."]
+abbrev closureCommMonoidOfComm {s : Set M} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) :
+    CommMonoid (closure s) :=
+  { (closure s).toMonoid with
+    mul_comm := fun ⟨_, h₁⟩ ⟨_, h₂⟩ ↦
+      have := closure_le_centralizer_centralizer s
+      Subtype.ext <| Set.centralizer_centralizer_comm_of_comm hcomm _ (this h₁) _ (this h₂) }
+
 end
 
 end Submonoid

Mathlib/GroupTheory/Subsemigroup/Centralizer.lean

@@ -67,6 +67,23 @@ variable (M)
 theorem centralizer_univ : centralizer Set.univ = center M :=
   SetLike.ext' (Set.centralizer_univ M)
 
+variable {M} in
+@[to_additive]
+lemma closure_le_centralizer_centralizer (s : Set M) :
+    closure s ≤ centralizer (centralizer s) :=
+  closure_le.mpr Set.subset_centralizer_centralizer
+
+/-- If all the elements of a set `s` commute, then `closure s` is a commutative semigroup. -/
+@[to_additive
+      "If all the elements of a set `s` commute, then `closure s` forms an additive
+      commutative semigroup."]
+abbrev closureCommSemigroupOfComm {s : Set M} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) :
+    CommSemigroup (closure s) :=
+  { MulMemClass.toSemigroup (closure s) with
+    mul_comm := fun ⟨_, h₁⟩ ⟨_, h₂⟩ ↦
+      have := closure_le_centralizer_centralizer s
+      Subtype.ext <| Set.centralizer_centralizer_comm_of_comm hcomm _ (this h₁) _ (this h₂) }
+
 end
 
 end Subsemigroup