# Centers of magmas and semigroups #

## Main definitions #

• Set.center: the center of a magma
• Set.addCenter: the center of an additive magma
• Set.centralizer: the centralizer of a subset of a magma
• Set.addCentralizer: the centralizer of a subset of an additive magma

See Mathlib.GroupTheory.Subsemigroup.Center for the definition of the center as a subsemigroup:

• Subsemigroup.center: the center of a semigroup
• 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.

See Mathlib.GroupTheory.Subsemigroup.Centralizer for the definition of the centralizer as a subsemigroup:

• Subsemigroup.centralizer: the centralizer of a subset of a semigroup
• AddSubsemigroup.centralizer: the centralizer of a subset of an additive semigroup

We provide Monoid.centralizer, AddMonoid.centralizer, Subgroup.centralizer, and AddSubgroup.centralizer in other files.

structure IsAddCentral {M : Type u_1} [Add M] (z : M) :

Conditions for an element to be additively central

• comm : ∀ (a : M), z + a = a + z

• left_assoc : ∀ (b c : M), z + (b + c) = z + b + c

• mid_assoc : ∀ (a c : M), a + z + c = a + (z + c)

• right_assoc : ∀ (a b : M), a + b + z = a + (b + z)

Instances For
theorem IsAddCentral.comm {M : Type u_1} [Add M] {z : M} (self : ) (a : M) :
z + a = a + z

theorem IsAddCentral.left_assoc {M : Type u_1} [Add M] {z : M} (self : ) (b : M) (c : M) :
z + (b + c) = z + b + c

theorem IsAddCentral.mid_assoc {M : Type u_1} [Add M] {z : M} (self : ) (a : M) (c : M) :
a + z + c = a + (z + c)

theorem IsAddCentral.right_assoc {M : Type u_1} [Add M] {z : M} (self : ) (a : M) (b : M) :
a + b + z = a + (b + z)

structure IsMulCentral {M : Type u_1} [Mul M] (z : M) :

Conditions for an element to be multiplicatively central

• comm : ∀ (a : M), z * a = a * z

multiplication commutes

• left_assoc : ∀ (b c : M), z * (b * c) = z * b * c

associative property for left multiplication

• mid_assoc : ∀ (a c : M), a * z * c = a * (z * c)

middle associative multiplication property

• right_assoc : ∀ (a b : M), a * b * z = a * (b * z)

associative property for right multiplication

Instances For
theorem IsMulCentral.comm {M : Type u_1} [Mul M] {z : M} (self : ) (a : M) :
z * a = a * z

multiplication commutes

theorem IsMulCentral.left_assoc {M : Type u_1} [Mul M] {z : M} (self : ) (b : M) (c : M) :
z * (b * c) = z * b * c

associative property for left multiplication

theorem IsMulCentral.mid_assoc {M : Type u_1} [Mul M] {z : M} (self : ) (a : M) (c : M) :
a * z * c = a * (z * c)

middle associative multiplication property

theorem IsMulCentral.right_assoc {M : Type u_1} [Mul M] {z : M} (self : ) (a : M) (b : M) :
a * b * z = a * (b * z)

associative property for right multiplication

theorem isMulCentral_iff {M : Type u_1} [Mul M] (z : M) :
(∀ (a : M), z * a = a * z) (∀ (b c : M), z * (b * c) = z * b * c) (∀ (a c : M), a * z * c = a * (z * c)) ∀ (a b : M), a * b * z = a * (b * z)
theorem isAddCentral_iff {M : Type u_1} [Add M] (z : M) :
(∀ (a : M), z + a = a + z) (∀ (b c : M), z + (b + c) = z + b + c) (∀ (a c : M), a + z + c = a + (z + c)) ∀ (a b : M), a + b + z = a + (b + z)
theorem IsAddCentral.left_comm {M : Type u_1} {a : M} [Add M] (h : ) (b : M) (c : M) :
a + (b + c) = b + (a + c)
theorem IsMulCentral.left_comm {M : Type u_1} {a : M} [Mul M] (h : ) (b : M) (c : M) :
a * (b * c) = b * (a * c)
theorem IsAddCentral.right_comm {M : Type u_1} {c : M} [Add M] (h : ) (a : M) (b : M) :
a + b + c = a + c + b
theorem IsMulCentral.right_comm {M : Type u_1} {c : M} [Mul M] (h : ) (a : M) (b : M) :
a * b * c = a * c * b

### Center #

Set M

The center of an additive magma.

Equations
• = {z : M | }
Instances For
def Set.center (M : Type u_1) [Mul M] :
Set M

The center of a magma.

Equations
• = {z : M | }
Instances For
def Set.addCentralizer {M : Type u_1} (S : Set M) [Add M] :
Set M

The centralizer of a subset of an additive magma.

Equations
• S.addCentralizer = {c : M | mS, m + c = c + m}
Instances For
def Set.centralizer {M : Type u_1} (S : Set M) [Mul M] :
Set M

The centralizer of a subset of a magma.

Equations
• S.centralizer = {c : M | mS, m * c = c * m}
Instances For
theorem Set.mem_addCenter_iff {M : Type u_1} [Add M] {z : M} :
theorem Set.mem_center_iff {M : Type u_1} [Mul M] {z : M} :
z
theorem Set.mem_addCentralizer {M : Type u_1} {S : Set M} [Add M] {c : M} :
c S.addCentralizer mS, m + c = c + m
theorem Set.mem_centralizer_iff {M : Type u_1} {S : Set M} [Mul M] {c : M} :
c S.centralizer mS, m * c = c * m
@[simp]
theorem Set.add_mem_addCenter {M : Type u_1} [Add M] {z₁ : M} {z₂ : M} (hz₁ : z₁ ) (hz₂ : z₂ ) :
z₁ + z₂
@[simp]
theorem Set.mul_mem_center {M : Type u_1} [Mul M] {z₁ : M} {z₂ : M} (hz₁ : z₁ ) (hz₂ : z₂ ) :
z₁ * z₂
theorem Set.center_subset_centralizer {M : Type u_1} [Mul M] (S : Set M) :
S.centralizer
theorem Set.addCentralizer_subset {M : Type u_1} {S : Set M} {T : Set M} [Add M] (h : S T) :
theorem Set.centralizer_subset {M : Type u_1} {S : Set M} {T : Set M} [Mul M] (h : S T) :
T.centralizer S.centralizer
theorem Set.subset_centralizer_centralizer {M : Type u_1} {S : Set M} [Mul M] :
S S.centralizer.centralizer
@[simp]
@[simp]
theorem Set.centralizer_centralizer_centralizer {M : Type u_1} [Mul M] (S : Set M) :
S.centralizer.centralizer.centralizer = S.centralizer
instance Set.decidableMemAddCentralizer {M : Type u_1} {S : Set M} [Add M] [(a : M) → Decidable (∀ bS, b + a = a + b)] :
DecidablePred fun (x : M) => x S.addCentralizer
Equations
instance Set.decidableMemCentralizer {M : Type u_1} {S : Set M} [Mul M] [(a : M) → Decidable (∀ bS, b * a = a * b)] :
DecidablePred fun (x : M) => x S.centralizer
Equations
theorem AddSemigroup.mem_center_iff {M : Type u_1} [] {z : M} :
∀ (g : M), g + z = z + g
theorem Semigroup.mem_center_iff {M : Type u_1} [] {z : M} :
z ∀ (g : M), g * z = z * g
@[simp]
theorem Set.add_mem_addCentralizer {M : Type u_1} {S : Set M} [] {a : M} {b : M} (ha : a S.addCentralizer) (hb : b S.addCentralizer) :
@[simp]
theorem Set.mul_mem_centralizer {M : Type u_1} {S : Set M} [] {a : M} {b : M} (ha : a S.centralizer) (hb : b S.centralizer) :
a * b S.centralizer
@[simp]
theorem Set.addCentralizer_eq_top_iff_subset {M : Type u_1} {S : Set M} [] :
@[simp]
theorem Set.centralizer_eq_top_iff_subset {M : Type u_1} {S : Set M} [] :
S.centralizer = Set.univ S
@[simp]
theorem Set.addCentralizer_univ (M : Type u_1) [] :
@[simp]
theorem Set.centralizer_univ (M : Type u_1) [] :
Set.univ.centralizer =
instance Set.decidableMemAddCenter {M : Type u_1} [] [(a : M) → Decidable (∀ (b : M), b + a = a + b)] :
DecidablePred fun (x : M) =>
Equations
instance Set.decidableMemCenter {M : Type u_1} [] [(a : M) → Decidable (∀ (b : M), b * a = a * b)] :
DecidablePred fun (x : M) => x
Equations
@[simp]
theorem Set.addCenter_eq_univ (M : Type u_1) [] :
= Set.univ
@[simp]
theorem Set.center_eq_univ (M : Type u_1) [] :
= Set.univ
@[simp]
theorem Set.addCentralizer_eq_univ (M : Type u_1) {S : Set M} [] :
@[simp]
theorem Set.centralizer_eq_univ (M : Type u_1) {S : Set M} [] :
S.centralizer = Set.univ
@[simp]
theorem Set.zero_mem_addCenter {M : Type u_1} [] :
@[simp]
theorem Set.one_mem_center {M : Type u_1} [] :
1
@[simp]
theorem Set.zero_mem_addCentralizer {M : Type u_1} {S : Set M} [] :
@[simp]
theorem Set.one_mem_centralizer {M : Type u_1} {S : Set M} [] :
1 S.centralizer
theorem Set.subset_center_units {M : Type u_1} [] :
Units.val ⁻¹'
@[simp]
theorem Set.addUnits_neg_mem_center {M : Type u_1} [] {a : } (ha : a ) :
(-a)
@[simp]
theorem Set.units_inv_mem_center {M : Type u_1} [] {a : Mˣ} (ha : a ) :
a⁻¹
@[simp]
theorem Set.invOf_mem_center {M : Type u_1} [] {a : M} [] (ha : a ) :
@[simp]
theorem Set.neg_mem_addCenter {M : Type u_1} {a : M} (ha : ) :
@[simp]
theorem Set.inv_mem_center {M : Type u_1} [] {a : M} (ha : a ) :
@[simp]
theorem Set.sub_mem_addCenter {M : Type u_1} {a : M} {b : M} (ha : ) (hb : ) :
a - b
@[simp]
theorem Set.div_mem_center {M : Type u_1} [] {a : M} {b : M} (ha : a ) (hb : b ) :
a / b
@[simp]
theorem Set.neg_mem_addCentralizer {M : Type u_1} {S : Set M} [] {a : M} (ha : a S.addCentralizer) :