Centralizers in semigroups, as subsemigroups.

Main definitions

• 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.

def AddSubsemigroup.centralizer {M : Type u_1} (S : Set M) [AddSemigroup M] : AddSubsemigroup M

The centralizer of a subset of an additive semigroup.

Equations

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

def Subsemigroup.centralizer {M : Type u_1} (S : Set M) [Semigroup M] : Subsemigroup M

The centralizer of a subset of a semigroup M.

Equations

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

@[simp]

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

@[simp]

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

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

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

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

Equations

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

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

Equations

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

theorem AddSubsemigroup.center_le_centralizer {M : Type u_1} [AddSemigroup M] (S : Set M) : AddSubsemigroup.center M ≤ AddSubsemigroup.centralizer S

theorem Subsemigroup.center_le_centralizer {M : Type u_1} [Semigroup M] (S : Set M) : Subsemigroup.center M ≤ Subsemigroup.centralizer S

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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