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 Subsemigroup.centralizer {M : Type u_1} (S : Set M) [Semigroup M] : Subsemigroup M

The centralizer of a subset of a semigroup M.

Equations

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

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

The centralizer of a subset of an additive semigroup.

Equations

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

theorem Subsemigroup.coe_centralizer {M : Type u_1} (S : Set M) [Semigroup M] : Eq (SetLike.coe (centralizer S)) S.centralizer

theorem AddSubsemigroup.coe_centralizer {M : Type u_1} (S : Set M) [AddSemigroup M] : Eq (SetLike.coe (centralizer S)) S.addCentralizer

theorem Subsemigroup.mem_centralizer_iff {M : Type u_1} {S : Set M} [Semigroup M] {z : M} : Iff (Membership.mem (centralizer S) z) (∀ (g : M), Membership.mem S g → Eq (HMul.hMul g z) (HMul.hMul z g))

theorem AddSubsemigroup.mem_centralizer_iff {M : Type u_1} {S : Set M} [AddSemigroup M] {z : M} : Iff (Membership.mem (centralizer S) z) (∀ (g : M), Membership.mem S g → Eq (HAdd.hAdd g z) (HAdd.hAdd z g))

def Subsemigroup.decidableMemCentralizer {M : Type u_1} {S : Set M} [Semigroup M] (a : M) [Decidable (∀ (b : M), Membership.mem S b → Eq (HMul.hMul b a) (HMul.hMul a b))] : Decidable (Membership.mem (centralizer S) a)

Equations

• Eq (Subsemigroup.decidableMemCentralizer a) (decidable_of_iff' (∀ (g : M), Membership.mem S g → Eq (HMul.hMul g a) (HMul.hMul a g)) ⋯)

def AddSubsemigroup.decidableMemCentralizer {M : Type u_1} {S : Set M} [AddSemigroup M] (a : M) [Decidable (∀ (b : M), Membership.mem S b → Eq (HAdd.hAdd b a) (HAdd.hAdd a b))] : Decidable (Membership.mem (centralizer S) a)

Equations

• Eq (AddSubsemigroup.decidableMemCentralizer a) (decidable_of_iff' (∀ (g : M), Membership.mem S g → Eq (HAdd.hAdd g a) (HAdd.hAdd a g)) ⋯)

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

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

theorem Subsemigroup.centralizer_le {M : Type u_1} {S T : Set M} [Semigroup M] (h : HasSubset.Subset S T) : LE.le (centralizer T) (centralizer S)

theorem AddSubsemigroup.centralizer_le {M : Type u_1} {S T : Set M} [AddSemigroup M] (h : HasSubset.Subset S T) : LE.le (centralizer T) (centralizer S)

theorem Subsemigroup.centralizer_eq_top_iff_subset {M : Type u_1} [Semigroup M] {s : Set M} : Iff (Eq (centralizer s) Top.top) (HasSubset.Subset s (SetLike.coe (center M)))

theorem AddSubsemigroup.centralizer_eq_top_iff_subset {M : Type u_1} [AddSemigroup M] {s : Set M} : Iff (Eq (centralizer s) Top.top) (HasSubset.Subset s (SetLike.coe (center M)))

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

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

theorem Subsemigroup.closure_le_centralizer_centralizer {M : Type u_1} [Semigroup M] (s : Set M) : LE.le (closure s) (centralizer (SetLike.coe (centralizer s)))

theorem AddSubsemigroup.closure_le_centralizer_centralizer {M : Type u_1} [AddSemigroup M] (s : Set M) : LE.le (closure s) (centralizer (SetLike.coe (centralizer s)))

@[reducible, inline]

abbrev Subsemigroup.closureCommSemigroupOfComm (M : Type u_1) [Semigroup M] {s : Set M} (hcomm : ∀ (a : M), Membership.mem s a → ∀ (b : M), Membership.mem s b → Eq (HMul.hMul a b) (HMul.hMul b a)) : CommSemigroup (Subtype fun (x : M) => Membership.mem (closure s) x)

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

Equations

• Eq (Subsemigroup.closureCommSemigroupOfComm M hcomm) { toSemigroup := MulMemClass.toSemigroup (Subsemigroup.closure s), mul_comm := ⋯ }

@[reducible, inline]

abbrev AddSubsemigroup.closureAddCommSemigroupOfComm (M : Type u_1) [AddSemigroup M] {s : Set M} (hcomm : ∀ (a : M), Membership.mem s a → ∀ (b : M), Membership.mem s b → Eq (HAdd.hAdd a b) (HAdd.hAdd b a)) : AddCommSemigroup (Subtype fun (x : M) => Membership.mem (closure s) x)

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

Equations

• Eq (AddSubsemigroup.closureAddCommSemigroupOfComm M hcomm) { toAddSemigroup := AddMemClass.toAddSemigroup (AddSubsemigroup.closure s), add_comm := ⋯ }