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 AddSubsemigroup.center (M : Type u_1) [Add M] :

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

Equations
• = { carrier := , add_mem' := }
Instances For
def Subsemigroup.center (M : Type u_1) [Mul M] :

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

Equations
• = { carrier := , mul_mem' := }
Instances For

The center of an additive magma is commutative and associative.

Equations
theorem AddSubsemigroup.center.addCommSemigroup.proof_2 {M : Type u_1} [Add M] (a : ) :
∀ (x : ), a + x = x + a
∀ (x b x_1 : ), x + b + x_1 = x + (b + x_1)
instance Subsemigroup.center.commSemigroup {M : Type u_1} [Mul M] :

The center of a magma is commutative and associative.

Equations
• Subsemigroup.center.commSemigroup =
theorem AddSubsemigroup.mem_center_iff {M : Type u_1} [] {z : M} :
∀ (g : M), g + z = z + g
theorem Subsemigroup.mem_center_iff {M : Type u_1} [] {z : M} :
∀ (g : M), g * z = z * g
instance AddSubsemigroup.decidableMemCenter {M : Type u_1} [] (a : M) [Decidable (∀ (b : M), b + a = a + b)] :
Equations
instance Subsemigroup.decidableMemCenter {M : Type u_1} [] (a : M) [Decidable (∀ (b : M), b * a = a * b)] :
Equations
@[simp]
theorem AddSubsemigroup.center_eq_top (M : Type u_1) [] :
@[simp]
theorem Subsemigroup.center_eq_top (M : Type u_1) [] :