Centers of semigroups, as subsemigroups.

Main definitions

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

References

• [Cabrera García and Rodríguez Palacios, Non-associative normed algebras. Volume 1] [CGRP14]

Set.center as a Subsemigroup.

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

The center of a semigroup M is the set of elements that commute with everything in M

Equations

• Eq (Subsemigroup.center M) { carrier := Set.center M, mul_mem' := ⋯ }

def AddSubsemigroup.center (M : Type u_1) [Add M] : AddSubsemigroup M

The center of a semigroup M is the set of elements that commute with everything in M

Equations

• Eq (AddSubsemigroup.center M) { carrier := Set.addCenter M, add_mem' := ⋯ }

def Subsemigroup.center.commSemigroup {M : Type u_1} [Mul M] : CommSemigroup (Subtype fun (x : M) => Membership.mem (center M) x)

The center of a magma is commutative and associative.

Equations

• Eq Subsemigroup.center.commSemigroup { toMul := MulMemClass.mul (Subsemigroup.center M), mul_assoc := ⋯, mul_comm := ⋯ }

def AddSubsemigroup.center.addCommSemigroup {M : Type u_1} [Add M] : AddCommSemigroup (Subtype fun (x : M) => Membership.mem (center M) x)

The center of an additive magma is commutative and associative.

Equations

• Eq AddSubsemigroup.center.addCommSemigroup { toAdd := AddMemClass.add (AddSubsemigroup.center M), add_assoc := ⋯, add_comm := ⋯ }

theorem Subsemigroup.mem_center_iff {M : Type u_1} [Semigroup M] {z : M} : Iff (Membership.mem (center M) z) (∀ (g : M), Eq (HMul.hMul g z) (HMul.hMul z g))

theorem AddSubsemigroup.mem_center_iff {M : Type u_1} [AddSemigroup M] {z : M} : Iff (Membership.mem (center M) z) (∀ (g : M), Eq (HAdd.hAdd g z) (HAdd.hAdd z g))

def Subsemigroup.decidableMemCenter {M : Type u_1} [Semigroup M] (a : M) [Decidable (∀ (b : M), Eq (HMul.hMul b a) (HMul.hMul a b))] : Decidable (Membership.mem (center M) a)

Equations

• Eq (Subsemigroup.decidableMemCenter a) (decidable_of_iff' (∀ (g : M), Eq (HMul.hMul g a) (HMul.hMul a g)) ⋯)

def AddSubsemigroup.decidableMemCenter {M : Type u_1} [AddSemigroup M] (a : M) [Decidable (∀ (b : M), Eq (HAdd.hAdd b a) (HAdd.hAdd a b))] : Decidable (Membership.mem (center M) a)

Equations

• Eq (AddSubsemigroup.decidableMemCenter a) (decidable_of_iff' (∀ (g : M), Eq (HAdd.hAdd g a) (HAdd.hAdd a g)) ⋯)

theorem Subsemigroup.center_eq_top (M : Type u_1) [CommSemigroup M] : Eq (center M) Top.top

theorem AddSubsemigroup.center_eq_top (M : Type u_1) [AddCommSemigroup M] : Eq (center M) Top.top