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 also

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) : Prop

Conditions for an element to be additively central

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

  addition commutes

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

  associative property for left addition

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

  middle associative addition property

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

  associative property for right addition

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

addition commutes

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

associative property for left addition

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

middle associative addition property

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

associative property for right addition

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

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

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

multiplication commutes

theorem IsMulCentral.left_assoc {M : Type u_1} [Mul M] {z : M} (self : IsMulCentral z) (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 : IsMulCentral z) (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 : IsMulCentral z) (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) : IsMulCentral z ↔ (∀ (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) : IsAddCentral z ↔ (∀ (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 : IsAddCentral a) (b : M) (c : M) : a + (b + c) = b + (a + c)

theorem IsMulCentral.left_comm {M : Type u_1} {a : M} [Mul M] (h : IsMulCentral a) (b : M) (c : M) : a * (b * c) = b * (a * c)

theorem IsAddCentral.right_comm {M : Type u_1} {c : M} [Add M] (h : IsAddCentral c) (a : M) (b : M) : a + b + c = a + c + b

theorem IsMulCentral.right_comm {M : Type u_1} {c : M} [Mul M] (h : IsMulCentral c) (a : M) (b : M) : a * b * c = a * c * b

Center

def Set.addCenter (M : Type u_1) [Add M] : Set M

The center of an additive magma.

Equations

• Set.addCenter M = {z : M | IsAddCentral z}

def Set.center (M : Type u_1) [Mul M] : Set M

The center of a magma.

Equations

• Set.center M = {z : M | IsMulCentral z}

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 | ∀ m ∈ S, m + c = c + m}

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 | ∀ m ∈ S, m * c = c * m}

theorem Set.mem_addCenter_iff {M : Type u_1} [Add M] {z : M} : z ∈ Set.addCenter M ↔ IsAddCentral z

theorem Set.mem_center_iff {M : Type u_1} [Mul M] {z : M} : z ∈ Set.center M ↔ IsMulCentral z

theorem Set.mem_addCentralizer {M : Type u_1} {S : Set M} [Add M] {c : M} : c ∈ S.addCentralizer ↔ ∀ m ∈ S, m + c = c + m

theorem Set.mem_centralizer_iff {M : Type u_1} {S : Set M} [Mul M] {c : M} : c ∈ S.centralizer ↔ ∀ m ∈ S, m * c = c * m

@[simp]

theorem Set.add_mem_addCenter {M : Type u_1} [Add M] {z₁ : M} {z₂ : M} (hz₁ : z₁ ∈ Set.addCenter M) (hz₂ : z₂ ∈ Set.addCenter M) : z₁ + z₂ ∈ Set.addCenter M

@[simp]

theorem Set.mul_mem_center {M : Type u_1} [Mul M] {z₁ : M} {z₂ : M} (hz₁ : z₁ ∈ Set.center M) (hz₂ : z₂ ∈ Set.center M) : z₁ * z₂ ∈ Set.center M

theorem Set.addCenter_subset_addCentralizer {M : Type u_1} [Add M] (S : Set M) : Set.addCenter M ⊆ S.addCentralizer

theorem Set.center_subset_centralizer {M : Type u_1} [Mul M] (S : Set M) : Set.center M ⊆ S.centralizer

theorem Set.addCentralizer_subset {M : Type u_1} {S : Set M} {T : Set M} [Add M] (h : S ⊆ T) : T.addCentralizer ⊆ S.addCentralizer

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_addCentralizer_addCentralizer {M : Type u_1} {S : Set M} [Add M] : S ⊆ S.addCentralizer.addCentralizer

theorem Set.subset_centralizer_centralizer {M : Type u_1} {S : Set M} [Mul M] : S ⊆ S.centralizer.centralizer

@[simp]

theorem Set.addCentralizer_addCentralizer_addCentralizer {M : Type u_1} [Add M] (S : Set M) : S.addCentralizer.addCentralizer.addCentralizer = S.addCentralizer

@[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 (∀ b ∈ S, b + a = a + b)] : DecidablePred fun (x : M) => x ∈ S.addCentralizer

Equations

• Set.decidableMemAddCentralizer x = decidable_of_iff' (∀ m ∈ S, m + x = x + m) ⋯

instance Set.decidableMemCentralizer {M : Type u_1} {S : Set M} [Mul M] [(a : M) → Decidable (∀ b ∈ S, b * a = a * b)] : DecidablePred fun (x : M) => x ∈ S.centralizer

Equations

• Set.decidableMemCentralizer x = decidable_of_iff' (∀ m ∈ S, m * x = x * m) ⋯

theorem AddSemigroup.mem_center_iff {M : Type u_1} [AddSemigroup M] {z : M} : z ∈ Set.addCenter M ↔ ∀ (g : M), g + z = z + g

theorem Semigroup.mem_center_iff {M : Type u_1} [Semigroup M] {z : M} : z ∈ Set.center M ↔ ∀ (g : M), g * z = z * g

@[simp]

theorem Set.add_mem_addCentralizer {M : Type u_1} {S : Set M} [AddSemigroup M] {a : M} {b : M} (ha : a ∈ S.addCentralizer) (hb : b ∈ S.addCentralizer) : a + b ∈ S.addCentralizer

@[simp]

theorem Set.mul_mem_centralizer {M : Type u_1} {S : Set M} [Semigroup 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} [AddSemigroup M] : S.addCentralizer = Set.univ ↔ S ⊆ Set.addCenter M

@[simp]

theorem Set.centralizer_eq_top_iff_subset {M : Type u_1} {S : Set M} [Semigroup M] : S.centralizer = Set.univ ↔ S ⊆ Set.center M

@[simp]

theorem Set.addCentralizer_univ (M : Type u_1) [AddSemigroup M] : Set.univ.addCentralizer = Set.addCenter M

@[simp]

theorem Set.centralizer_univ (M : Type u_1) [Semigroup M] : Set.univ.centralizer = Set.center M

instance Set.decidableMemAddCenter {M : Type u_1} [AddSemigroup M] [(a : M) → Decidable (∀ (b : M), b + a = a + b)] : DecidablePred fun (x : M) => x ∈ Set.addCenter M

Equations

• Set.decidableMemAddCenter x = decidable_of_iff' (∀ (g : M), g + x = x + g) ⋯

instance Set.decidableMemCenter {M : Type u_1} [Semigroup M] [(a : M) → Decidable (∀ (b : M), b * a = a * b)] : DecidablePred fun (x : M) => x ∈ Set.center M

Equations

• Set.decidableMemCenter x = decidable_of_iff' (∀ (g : M), g * x = x * g) ⋯

@[simp]

theorem Set.addCenter_eq_univ (M : Type u_1) [AddCommSemigroup M] : Set.addCenter M = Set.univ

@[simp]

theorem Set.center_eq_univ (M : Type u_1) [CommSemigroup M] : Set.center M = Set.univ

@[simp]

theorem Set.addCentralizer_eq_univ (M : Type u_1) {S : Set M} [AddCommSemigroup M] : S.addCentralizer = Set.univ

@[simp]

theorem Set.centralizer_eq_univ (M : Type u_1) {S : Set M} [CommSemigroup M] : S.centralizer = Set.univ

@[simp]

theorem Set.zero_mem_addCenter {M : Type u_1} [AddZeroClass M] : 0 ∈ Set.addCenter M

@[simp]

theorem Set.one_mem_center {M : Type u_1} [MulOneClass M] : 1 ∈ Set.center M

@[simp]

theorem Set.zero_mem_addCentralizer {M : Type u_1} {S : Set M} [AddZeroClass M] : 0 ∈ S.addCentralizer

@[simp]

theorem Set.one_mem_centralizer {M : Type u_1} {S : Set M} [MulOneClass M] : 1 ∈ S.centralizer

theorem Set.subset_addCenter_add_units {M : Type u_1} [AddMonoid M] : AddUnits.val ⁻¹' Set.addCenter M ⊆ Set.addCenter (AddUnits M)

theorem Set.subset_center_units {M : Type u_1} [Monoid M] : Units.val ⁻¹' Set.center M ⊆ Set.center Mˣ

@[simp]

theorem Set.addUnits_neg_mem_center {M : Type u_1} [AddMonoid M] {a : AddUnits M} (ha : ↑a ∈ Set.addCenter M) : ↑(-a) ∈ Set.addCenter M

@[simp]

theorem Set.units_inv_mem_center {M : Type u_1} [Monoid M] {a : Mˣ} (ha : ↑a ∈ Set.center M) : ↑a⁻¹ ∈ Set.center M

@[simp]

theorem Set.invOf_mem_center {M : Type u_1} [Monoid M] {a : M} [Invertible a] (ha : a ∈ Set.center M) : ⅟a ∈ Set.center M

@[simp]

theorem Set.neg_mem_addCenter {M : Type u_1} [SubtractionMonoid M] {a : M} (ha : a ∈ Set.addCenter M) : -a ∈ Set.addCenter M

@[simp]

theorem Set.inv_mem_center {M : Type u_1} [DivisionMonoid M] {a : M} (ha : a ∈ Set.center M) : a⁻¹ ∈ Set.center M

@[simp]

theorem Set.sub_mem_addCenter {M : Type u_1} [SubtractionMonoid M] {a : M} {b : M} (ha : a ∈ Set.addCenter M) (hb : b ∈ Set.addCenter M) : a - b ∈ Set.addCenter M

@[simp]

theorem Set.div_mem_center {M : Type u_1} [DivisionMonoid M] {a : M} {b : M} (ha : a ∈ Set.center M) (hb : b ∈ Set.center M) : a / b ∈ Set.center M

@[simp]

theorem Set.neg_mem_addCentralizer {M : Type u_1} {S : Set M} [AddGroup M] {a : M} (ha : a ∈ S.addCentralizer) : -a ∈ S.addCentralizer

@[simp]

theorem Set.inv_mem_centralizer {M : Type u_1} {S : Set M} [Group M] {a : M} (ha : a ∈ S.centralizer) : a⁻¹ ∈ S.centralizer

@[simp]

theorem Set.sub_mem_addCentralizer {M : Type u_1} {S : Set M} [AddGroup M] {a : M} {b : M} (ha : a ∈ S.addCentralizer) (hb : b ∈ S.addCentralizer) : a - b ∈ S.addCentralizer

@[simp]

theorem Set.div_mem_centralizer {M : Type u_1} {S : Set M} [Group M] {a : M} {b : M} (ha : a ∈ S.centralizer) (hb : b ∈ S.centralizer) : a / b ∈ S.centralizer