feat: port GroupTheory.Submonoid.Center (#1315)

Also includes fixes in other files as well (`Set.Center` to `Set.center` and a few more like that).

Mathlib.lean

@@ -354,6 +354,7 @@ import Mathlib.GroupTheory.GroupAction.Units
 import Mathlib.GroupTheory.Perm.Basic
 import Mathlib.GroupTheory.Perm.ViaEmbedding
 import Mathlib.GroupTheory.Submonoid.Basic
+import Mathlib.GroupTheory.Submonoid.Center
 import Mathlib.GroupTheory.Submonoid.Operations
 import Mathlib.GroupTheory.Subsemigroup.Basic
 import Mathlib.GroupTheory.Subsemigroup.Center

Mathlib/GroupTheory/Submonoid/Center.lean

@@ -0,0 +1,113 @@
+/-
+Copyright (c) 2021 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+
+! This file was ported from Lean 3 source module group_theory.submonoid.center
+! leanprover-community/mathlib commit 6cb77a8eaff0ddd100e87b1591c6d3ad319514ff
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.GroupTheory.Submonoid.Operations
+import Mathlib.GroupTheory.Subsemigroup.Center
+
+/-!
+# Centers of monoids
+
+## Main definitions
+
+* `Submonoid.center`: the center of a monoid
+* `AddSubmonoid.center`: the center of an additive monoid
+
+We provide `Subgroup.center`, `AddSubgroup.center`, `Subsemiring.center`, and `Subring.center` in
+other files.
+-/
+
+
+namespace Submonoid
+
+section
+
+variable (M : Type _) [Monoid M]
+
+/-- The center of a monoid `M` is the set of elements that commute with everything in `M` -/
+@[to_additive
+      "The center of a monoid `M` is the set of elements that commute with everything in `M`"]
+def center : Submonoid M where
+  carrier := Set.center M
+  one_mem' := Set.one_mem_center M
+  mul_mem' := Set.mul_mem_center
+#align submonoid.center Submonoid.center
+#align add_submonoid.center AddSubmonoid.center
+
+@[to_additive]
+theorem coe_center : ↑(center M) = Set.center M :=
+  rfl
+#align submonoid.coe_center Submonoid.coe_center
+#align add_submonoid.coe_center AddSubmonoid.coe_center
+
+@[simp]
+theorem center_toSubsemigroup : (center M).toSubsemigroup = Subsemigroup.center M :=
+  rfl
+#align submonoid.center_to_subsemigroup Submonoid.center_toSubsemigroup
+
+theorem _root_.AddSubmonoid.center_toAddSubsemigroup (M) [AddMonoid M] :
+    (AddSubmonoid.center M).toAddSubsemigroup = AddSubsemigroup.center M :=
+  rfl
+#align add_submonoid.center_to_add_subsemigroup AddSubmonoid.center_toAddSubsemigroup
+
+attribute [to_additive AddSubmonoid.center_to_add_subsemigroup] Submonoid.center_toSubsemigroup
+
+variable {M}
+
+@[to_additive]
+theorem mem_center_iff {z : M} : z ∈ center M ↔ ∀ g, g * z = z * g :=
+  Iff.rfl
+#align submonoid.mem_center_iff Submonoid.mem_center_iff
+#align add_submonoid.mem_center_iff AddSubmonoid.mem_center_iff
+
+@[to_additive]
+instance decidableMemCenter (a) [Decidable <| ∀ b : M, b * a = a * b] : Decidable (a ∈ center M) :=
+  decidable_of_iff' _ mem_center_iff
+#align submonoid.decidable_mem_center Submonoid.decidableMemCenter
+#align add_submonoid.decidable_mem_center AddSubmonoid.decidableMemCenter
+
+/-- The center of a monoid is commutative. -/
+instance : CommMonoid (center M) :=
+  { (center M).toMonoid with
+    mul_comm := fun _ b => Subtype.ext <| b.prop _ }
+
+/-- The center of a monoid acts commutatively on that monoid. -/
+instance center.smulCommClass_left : SMulCommClass (center M) M M
+    where smul_comm m x y := (Commute.left_comm (m.prop x) y).symm
+#align submonoid.center.smul_comm_class_left Submonoid.center.smulCommClass_left
+
+/-- The center of a monoid acts commutatively on that monoid. -/
+instance center.smulCommClass_right : SMulCommClass M (center M) M :=
+  SMulCommClass.symm _ _ _
+#align submonoid.center.smul_comm_class_right Submonoid.center.smulCommClass_right
+
+/-! Note that `smulCommClass (center M) (center M) M` is already implied by
+`Submonoid.smulCommClass_right` -/
+
+
+example : SMulCommClass (center M) (center M) M := by infer_instance
+
+end
+
+section
+
+variable (M : Type _) [CommMonoid M]
+
+@[simp]
+theorem center_eq_top : center M = ⊤ :=
+  SetLike.coe_injective (Set.center_eq_univ M)
+#align submonoid.center_eq_top Submonoid.center_eq_top
+
+end
+
+end Submonoid
+
+-- Porting note: `assert_not_exists` is not ported yet
+-- Guard against import creep
+--assert_not_exists finset

Mathlib/GroupTheory/Subsemigroup/Center.lean

@@ -16,13 +16,13 @@ import Mathlib.GroupTheory.Subsemigroup.Operations
 
 ## Main definitions
 
-* `Set.Center`: the center of a magma
-* `Subsemigroup.Center`: the center of a semigroup
-* `Set.AddCenter`: the center of an additive magma
-* `AddSubsemigroup.Center`: the center of an additive semigroup
+* `Set.center`: the center of a magma
+* `Subsemigroup.center`: the center of a semigroup
+* `Set.addCenter`: the center of an additive magma
+* `AddSubsemigroup.center`: the center of an additive semigroup
 
-We provide `Submonoid.Center`, `AddSubmonoid.Center`, `Subgroup.Center`, `AddSubgroup.Center`,
-`Subsemiring.Center`, and `Subring.Center` in other files.
+We provide `Submonoid.center`, `AddSubmonoid.center`, `Subgroup.center`, `AddSubgroup.center`,
+`Subsemiring.center`, and `Subring.center` in other files.
 -/
 
 
@@ -33,77 +33,77 @@ namespace Set
 variable (M)
 
 /-- The center of a magma. -/
-@[to_additive AddCenter " The center of an additive magma. "]
-def Center [Mul M] : Set M :=
+@[to_additive addCenter " The center of an additive magma. "]
+def center [Mul M] : Set M :=
   { z | ∀ m, m * z = z * m }
-#align set.center Set.Center
-#align set.add_center Set.AddCenter
+#align set.center Set.center
+#align set.add_center Set.addCenter
 
--- porting note: The `to_additive` version used to be `mem_add_center` without the iff
+-- porting note: The `to_additive` version used to be `mem_addCenter` without the iff
 @[to_additive mem_addCenter_iff]
-theorem mem_center_iff [Mul M] {z : M} : z ∈ Center M ↔ ∀ g, g * z = z * g :=
+theorem mem_center_iff [Mul M] {z : M} : z ∈ center M ↔ ∀ g, g * z = z * g :=
   Iff.rfl
 #align set.mem_center_iff Set.mem_center_iff
 #align set.mem_add_center Set.mem_addCenter_iff
 
 instance decidableMemCenter [Mul M] [∀ a : M, Decidable <| ∀ b : M, b * a = a * b] :
-    DecidablePred (· ∈ Center M) := fun _ => decidable_of_iff' _ (mem_center_iff M)
+    DecidablePred (· ∈ center M) := fun _ => decidable_of_iff' _ (mem_center_iff M)
 #align set.decidable_mem_center Set.decidableMemCenter
 
 @[simp, to_additive zero_mem_addCenter]
-theorem one_mem_center [MulOneClass M] : (1 : M) ∈ Set.Center M := by simp [mem_center_iff]
+theorem one_mem_center [MulOneClass M] : (1 : M) ∈ Set.center M := by simp [mem_center_iff]
 #align set.one_mem_center Set.one_mem_center
 #align set.zero_mem_add_center Set.zero_mem_addCenter
 
 @[simp]
-theorem zero_mem_center [MulZeroClass M] : (0 : M) ∈ Set.Center M := by simp [mem_center_iff]
+theorem zero_mem_center [MulZeroClass M] : (0 : M) ∈ Set.center M := by simp [mem_center_iff]
 #align set.zero_mem_center Set.zero_mem_center
 
 variable {M}
 
 @[simp, to_additive add_mem_addCenter]
-theorem mul_mem_center [Semigroup M] {a b : M} (ha : a ∈ Set.Center M) (hb : b ∈ Set.Center M) :
-    a * b ∈ Set.Center M := fun g => by rw [mul_assoc, ← hb g, ← mul_assoc, ha g, mul_assoc]
+theorem mul_mem_center [Semigroup M] {a b : M} (ha : a ∈ Set.center M) (hb : b ∈ Set.center M) :
+    a * b ∈ Set.center M := fun g => by rw [mul_assoc, ← hb g, ← mul_assoc, ha g, mul_assoc]
 #align set.mul_mem_center Set.mul_mem_center
 #align set.add_mem_add_center Set.add_mem_addCenter
 
 @[simp, to_additive neg_mem_addCenter]
-theorem inv_mem_center [Group M] {a : M} (ha : a ∈ Set.Center M) :
-    a⁻¹ ∈ Set.Center M := fun g => by
+theorem inv_mem_center [Group M] {a : M} (ha : a ∈ Set.center M) :
+    a⁻¹ ∈ Set.center M := fun g => by
   rw [← inv_inj, mul_inv_rev, inv_inv, ← ha, mul_inv_rev, inv_inv]
 #align set.inv_mem_center Set.inv_mem_center
 #align set.neg_mem_add_center Set.neg_mem_addCenter
 
 @[simp]
-theorem add_mem_center [Distrib M] {a b : M} (ha : a ∈ Set.Center M) (hb : b ∈ Set.Center M) :
-    a + b ∈ Set.Center M := fun c => by rw [add_mul, mul_add, ha c, hb c]
+theorem add_mem_center [Distrib M] {a b : M} (ha : a ∈ Set.center M) (hb : b ∈ Set.center M) :
+    a + b ∈ Set.center M := fun c => by rw [add_mul, mul_add, ha c, hb c]
 #align set.add_mem_center Set.add_mem_center
 
 @[simp]
-theorem neg_mem_center [Ring M] {a : M} (ha : a ∈ Set.Center M) : -a ∈ Set.Center M := fun c => by
+theorem neg_mem_center [Ring M] {a : M} (ha : a ∈ Set.center M) : -a ∈ Set.center M := fun c => by
   rw [← neg_mul_comm, ha (-c), neg_mul_comm]
 #align set.neg_mem_center Set.neg_mem_center
 
 @[to_additive subset_addCenter_add_units]
-theorem subset_center_units [Monoid M] : ((↑) : Mˣ → M) ⁻¹' Center M ⊆ Set.Center Mˣ :=
+theorem subset_center_units [Monoid M] : ((↑) : Mˣ → M) ⁻¹' center M ⊆ Set.center Mˣ :=
   fun _ ha _ => Units.ext <| ha _
 #align set.subset_center_units Set.subset_center_units
 #align set.subset_add_center_add_units Set.subset_addCenter_add_units
 
-theorem center_units_subset [GroupWithZero M] : Set.Center Mˣ ⊆ ((↑) : Mˣ → M) ⁻¹' Center M :=
+theorem center_units_subset [GroupWithZero M] : Set.center Mˣ ⊆ ((↑) : Mˣ → M) ⁻¹' center M :=
   fun a ha b => by
   obtain rfl | hb := eq_or_ne b 0
   · rw [zero_mul, mul_zero]
   · exact Units.ext_iff.mp (ha (Units.mk0 _ hb))
 #align set.center_units_subset Set.center_units_subset
 
 /-- In a group with zero, the center of the units is the preimage of the center. -/
-theorem center_units_eq [GroupWithZero M] : Set.Center Mˣ = ((↑) : Mˣ → M) ⁻¹' Center M :=
+theorem center_units_eq [GroupWithZero M] : Set.center Mˣ = ((↑) : Mˣ → M) ⁻¹' center M :=
   Subset.antisymm center_units_subset subset_center_units
 #align set.center_units_eq Set.center_units_eq
 
 @[simp]
-theorem inv_mem_center₀ [GroupWithZero M] {a : M} (ha : a ∈ Set.Center M) : a⁻¹ ∈ Set.Center M :=
+theorem inv_mem_center₀ [GroupWithZero M] {a : M} (ha : a ∈ Set.center M) : a⁻¹ ∈ Set.center M :=
   by
   obtain rfl | ha0 := eq_or_ne a 0
   · rw [inv_zero]
@@ -114,16 +114,16 @@ theorem inv_mem_center₀ [GroupWithZero M] {a : M} (ha : a ∈ Set.Center M) :
 #align set.inv_mem_center₀ Set.inv_mem_center₀
 
 @[simp, to_additive sub_mem_addCenter]
-theorem div_mem_center [Group M] {a b : M} (ha : a ∈ Set.Center M) (hb : b ∈ Set.Center M) :
-    a / b ∈ Set.Center M := by
+theorem div_mem_center [Group M] {a b : M} (ha : a ∈ Set.center M) (hb : b ∈ Set.center M) :
+    a / b ∈ Set.center M := by
   rw [div_eq_mul_inv]
   exact mul_mem_center ha (inv_mem_center hb)
 #align set.div_mem_center Set.div_mem_center
 #align set.sub_mem_add_center Set.sub_mem_addCenter
 
 @[simp]
-theorem div_mem_center₀ [GroupWithZero M] {a b : M} (ha : a ∈ Set.Center M)
-    (hb : b ∈ Set.Center M) : a / b ∈ Set.Center M :=
+theorem div_mem_center₀ [GroupWithZero M] {a b : M} (ha : a ∈ Set.center M)
+    (hb : b ∈ Set.center M) : a / b ∈ Set.center M :=
   by
   rw [div_eq_mul_inv]
   exact mul_mem_center ha (inv_mem_center₀ hb)
@@ -132,7 +132,7 @@ theorem div_mem_center₀ [GroupWithZero M] {a b : M} (ha : a ∈ Set.Center M)
 variable (M)
 
 @[simp, to_additive addCenter_eq_univ]
-theorem center_eq_univ [CommSemigroup M] : Center M = Set.univ :=
+theorem center_eq_univ [CommSemigroup M] : center M = Set.univ :=
   (Subset.antisymm (subset_univ _)) fun x _ y => mul_comm y x
 #align set.center_eq_univ Set.center_eq_univ
 #align set.add_center_eq_univ Set.addCenter_eq_univ
@@ -148,11 +148,11 @@ variable (M) [Semigroup M]
 /-- The center of a semigroup `M` is the set of elements that commute with everything in `M` -/
 @[to_additive
       "The center of a semigroup `M` is the set of elements that commute with everything in `M`"]
-def Center : Subsemigroup M where
-  carrier := Set.Center M
+def center : Subsemigroup M where
+  carrier := Set.center M
   mul_mem':= Set.mul_mem_center
-#align subsemigroup.center Subsemigroup.Center
-#align add_subsemigroup.center AddSubsemigroup.Center
+#align subsemigroup.center Subsemigroup.center
+#align add_subsemigroup.center AddSubsemigroup.center
 
 -- porting note: `coe_center` is now redundant
 #noalign subsemigroup.coe_center
@@ -161,21 +161,21 @@ def Center : Subsemigroup M where
 variable {M}
 
 @[to_additive]
-theorem mem_center_iff {z : M} : z ∈ Center M ↔ ∀ g, g * z = z * g :=
+theorem mem_center_iff {z : M} : z ∈ center M ↔ ∀ g, g * z = z * g :=
   Iff.rfl
 #align subsemigroup.mem_center_iff Subsemigroup.mem_center_iff
 #align add_subsemigroup.mem_center_iff AddSubsemigroup.mem_center_iff
 
 @[to_additive]
-instance decidableMemCenter (a) [Decidable <| ∀ b : M, b * a = a * b] : Decidable (a ∈ Center M) :=
+instance decidableMemCenter (a) [Decidable <| ∀ b : M, b * a = a * b] : Decidable (a ∈ center M) :=
   decidable_of_iff' _ mem_center_iff
 #align subsemigroup.decidable_mem_center Subsemigroup.decidableMemCenter
 #align add_subsemigroup.decidable_mem_center AddSubsemigroup.decidableMemCenter
 
 /-- The center of a semigroup is commutative. -/
 @[to_additive "The center of an additive semigroup is commutative."]
-instance : CommSemigroup (Center M) :=
-  { MulMemClass.toSemigroup (Center M) with mul_comm := fun _ b => Subtype.ext <| b.2 _ }
+instance : CommSemigroup (center M) :=
+  { MulMemClass.toSemigroup (center M) with mul_comm := fun _ b => Subtype.ext <| b.2 _ }
 
 end
 
@@ -184,7 +184,7 @@ section
 variable (M) [CommSemigroup M]
 
 @[to_additive, simp]
-theorem center_eq_top : Center M = ⊤ :=
+theorem center_eq_top : center M = ⊤ :=
   SetLike.coe_injective (Set.center_eq_univ M)
 #align subsemigroup.center_eq_top Subsemigroup.center_eq_top
 #align add_subsemigroup.center_eq_top AddSubsemigroup.center_eq_top

Mathlib/GroupTheory/Subsemigroup/Centralizer.lean

@@ -125,7 +125,7 @@ theorem centralizer_subset [Mul M] (h : S ⊆ T) : centralizer T ⊆ centralizer
 variable (M)
 
 @[simp, to_additive add_centralizer_univ]
-theorem centralizer_univ [Mul M] : centralizer univ = Center M :=
+theorem centralizer_univ [Mul M] : centralizer univ = center M :=
   Subset.antisymm (fun _ ha b => ha b (Set.mem_univ b)) fun _ ha b _ => ha b
 #align set.centralizer_univ Set.centralizer_univ
 #align set.add_centralizer_univ Set.add_centralizer_univ
@@ -183,7 +183,7 @@ theorem centralizer_le (h : S ⊆ T) : centralizer T ≤ centralizer S :=
 
 variable (M)
 @[simp, to_additive]
-theorem centralizer_univ : centralizer Set.univ = Center M :=
+theorem centralizer_univ : centralizer Set.univ = center M :=
   SetLike.ext' (Set.centralizer_univ M)
 #align subsemigroup.centralizer_univ Subsemigroup.centralizer_univ
 #align add_subsemigroup.centralizer_univ AddSubsemigroup.centralizer_univ
@@ -195,4 +195,3 @@ end Subsemigroup
 -- porting note: This does not exist yet, however it is not relevant for functionality
 -- Guard against import creep
 -- assert_not_exists finset
-