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.

theorem AddSubmonoid.centralizer.proof_1 {M : Type u_1} (S : Set M) [AddMonoid M] : ∀ {a b : M}, a ∈ Set.addCentralizer S → b ∈ Set.addCentralizer S → a + b ∈ Set.addCentralizer S

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 = { toAddSubsemigroup := { carrier := Set.addCentralizer S, add_mem' := ⋯ }, zero_mem' := ⋯ }

theorem AddSubmonoid.centralizer.proof_2 {M : Type u_1} (S : Set M) [AddMonoid M] : 0 ∈ Set.addCentralizer S

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 = { toSubsemigroup := { carrier := Set.centralizer S, mul_mem' := ⋯ }, one_mem' := ⋯ }

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

Equations

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

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

Equations

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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