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] [cabreragarciarodriguezpalacios2014]

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

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

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

instance Subsemigroup.center.commSemigroup {M : Type u_1} [Mul M] : CommSemigroup ↥(center M)

The center of a magma is commutative and associative.

instance AddSubsemigroup.center.addCommSemigroup {M : Type u_1} [Add M] : AddCommSemigroup ↥(center M)

The center of an additive magma is commutative and associative.

theorem Subsemigroup.mem_center_iff {M : Type u_1} [Semigroup M] {z : M} : z ∈ center M ↔ ∀ (g : M), g * z = z * g

theorem AddSubsemigroup.mem_center_iff {M : Type u_1} [AddSemigroup M] {z : M} : z ∈ center M ↔ ∀ (g : M), g + z = z + g

instance Subsemigroup.decidableMemCenter {M : Type u_1} [Semigroup M] (a : M) [Decidable (∀ (b : M), b * a = a * b)] : Decidable (a ∈ center M)

instance AddSubsemigroup.decidableMemCenter {M : Type u_1} [AddSemigroup M] (a : M) [Decidable (∀ (b : M), b + a = a + b)] : Decidable (a ∈ center M)

@[simp]

theorem Subsemigroup.center_eq_top (M : Type u_1) [CommSemigroup M] : center M = ⊤

@[simp]

theorem AddSubsemigroup.center_eq_top (M : Type u_1) [AddCommSemigroup M] : center M = ⊤