Centralizers of magmas and monoids

Main definitions

• Submonoid.centralizer: the centralizer of a subset of a monoid
• AddSubmonoid.centralizer: the centralizer of a subset of an additive monoid

We provide Subgroup.centralizer, AddSubgroup.centralizer in other files.

def Submonoid.centralizer {M : Type u_1} (S : Set M) [Monoid M] : Submonoid M

The centralizer of a subset of a monoid M.

Equations

• Submonoid.centralizer S = { carrier := S.centralizer, mul_mem' := ⋯, one_mem' := ⋯ }

def AddSubmonoid.centralizer {M : Type u_1} (S : Set M) [AddMonoid M] : AddSubmonoid M

The centralizer of a subset of an additive monoid.

Equations

• AddSubmonoid.centralizer S = { carrier := S.addCentralizer, add_mem' := ⋯, zero_mem' := ⋯ }

@[simp]

theorem Submonoid.coe_centralizer {M : Type u_1} (S : Set M) [Monoid M] : ↑(centralizer S) = S.centralizer

@[simp]

theorem AddSubmonoid.coe_centralizer {M : Type u_1} (S : Set M) [AddMonoid M] : ↑(centralizer S) = S.addCentralizer

theorem Submonoid.centralizer_toSubsemigroup {M : Type u_1} (S : Set M) [Monoid M] : (centralizer S).toSubsemigroup = Subsemigroup.centralizer S

theorem AddSubmonoid.centralizer_toAddSubsemigroup {M : Type u_1} (S : Set M) [AddMonoid M] : (centralizer S).toAddSubsemigroup = AddSubsemigroup.centralizer S

theorem Submonoid.mem_centralizer_iff {M : Type u_1} {S : Set M} [Monoid M] {z : M} : z ∈ centralizer S ↔ ∀ g ∈ S, g * z = z * g

theorem AddSubmonoid.mem_centralizer_iff {M : Type u_1} {S : Set M} [AddMonoid M] {z : M} : z ∈ centralizer S ↔ ∀ g ∈ S, g + z = z + g

theorem Submonoid.center_le_centralizer {M : Type u_1} [Monoid M] (s : Set M) : center M ≤ centralizer s

theorem AddSubmonoid.center_le_centralizer {M : Type u_1} [AddMonoid M] (s : Set M) : center M ≤ centralizer s

@[implicit_reducible]

instance Submonoid.decidableMemCentralizer {M : Type u_1} {S : Set M} [Monoid M] (a : M) [Decidable (∀ b ∈ S, b * a = a * b)] : Decidable (a ∈ centralizer S)

Equations

• Submonoid.decidableMemCentralizer a = decidable_of_iff' (∀ g ∈ S, g * a = a * g) ⋯

@[implicit_reducible]

instance AddSubmonoid.decidableMemCentralizer {M : Type u_1} {S : Set M} [AddMonoid M] (a : M) [Decidable (∀ b ∈ S, b + a = a + b)] : Decidable (a ∈ centralizer S)

Equations

• AddSubmonoid.decidableMemCentralizer a = decidable_of_iff' (∀ g ∈ S, g + a = a + g) ⋯

theorem Submonoid.centralizer_le {M : Type u_1} {S T : Set M} [Monoid M] (h : S ⊆ T) : centralizer T ≤ centralizer S

theorem AddSubmonoid.centralizer_le {M : Type u_1} {S T : Set M} [AddMonoid M] (h : S ⊆ T) : centralizer T ≤ centralizer S

@[simp]

theorem Submonoid.centralizer_eq_top_iff_subset {M : Type u_1} [Monoid M] {s : Set M} : centralizer s = ⊤ ↔ s ⊆ ↑(center M)

@[simp]

theorem AddSubmonoid.centralizer_eq_top_iff_subset {M : Type u_1} [AddMonoid M] {s : Set M} : centralizer s = ⊤ ↔ s ⊆ ↑(center M)

@[simp]

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

@[simp]

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

theorem Submonoid.le_centralizer_centralizer (M : Type u_1) [Monoid M] {s : Submonoid M} : s ≤ centralizer ↑(centralizer ↑s)

theorem AddSubmonoid.le_centralizer_centralizer (M : Type u_1) [AddMonoid M] {s : AddSubmonoid M} : s ≤ centralizer ↑(centralizer ↑s)

@[simp]

theorem Submonoid.centralizer_centralizer_centralizer (M : Type u_1) [Monoid M] {s : Set M} : centralizer s.centralizer.centralizer = centralizer s

@[simp]

theorem AddSubmonoid.centralizer_centralizer_centralizer (M : Type u_1) [AddMonoid M] {s : Set M} : centralizer s.addCentralizer.addCentralizer = centralizer s

theorem Submonoid.closure_le_centralizer_centralizer {M : Type u_1} [Monoid M] (s : Set M) : closure s ≤ centralizer ↑(centralizer s)

theorem AddSubmonoid.closure_le_centralizer_centralizer {M : Type u_1} [AddMonoid M] (s : Set M) : closure s ≤ centralizer ↑(centralizer s)

theorem Submonoid.isMulCommutative_closure (M : Type u_1) [Monoid M] {s : Set M} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) : IsMulCommutative ↥(closure s)

If all the elements of a set s commute, then closure s is a commutative monoid.

theorem AddSubmonoid.isAddCommutative_closure (M : Type u_1) [AddMonoid M] {s : Set M} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a + b = b + a) : IsAddCommutative ↥(closure s)

If all the elements of a set s commute, then closure s forms an additive commutative monoid.

@[reducible, inline, deprecated Submonoid.isMulCommutative_closure (since := "2026-03-09")]

abbrev Submonoid.closureCommMonoidOfComm (M : Type u_1) [Monoid M] {s : Set M} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) : CommMonoid ↥(closure s)

If all the elements of a set s commute, then closure s is a commutative monoid.

Equations

• Submonoid.closureCommMonoidOfComm M hcomm = inferInstance

@[reducible, inline, deprecated Submonoid.isMulCommutative_closure (since := "2026-03-09")]

abbrev AddSubmonoid.closureAddCommMonoidOfComm (M : Type u_1) [AddMonoid M] {s : Set M} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a + b = b + a) : AddCommMonoid ↥(closure s)

If all the elements of a set s commute, then closure s forms an additive commutative monoid.

Equations

• AddSubmonoid.closureAddCommMonoidOfComm M hcomm = inferInstance

instance Submonoid.instIsMulCommutative_closure (M : Type u_1) [Monoid M] {S : Type u_2} [SetLike S M] [MulMemClass S M] (s : S) [IsMulCommutative ↥s] : IsMulCommutative ↥(closure ↑s)

instance AddSubmonoid.instIsAddCommutative_closure (M : Type u_1) [AddMonoid M] {S : Type u_2} [SetLike S M] [AddMemClass S M] (s : S) [IsAddCommutative ↥s] : IsAddCommutative ↥(closure ↑s)