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] : AddSubsemigroup M

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

Equations

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

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

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

theorem AddSubsemigroup.center.addCommSemigroup.proof_2 {M : Type u_1} [Add M] (a : { x : M // x ∈ AddSubsemigroup.center M }) : ∀ (x : { x : M // x ∈ AddSubsemigroup.center M }), a + x = x + a

theorem AddSubsemigroup.center.addCommSemigroup.proof_1 {M : Type u_1} [Add M] : ∀ (x b x_1 : { x : M // x ∈ AddSubsemigroup.center M }), x + b + x_1 = x + (b + x_1)

instance AddSubsemigroup.center.addCommSemigroup {M : Type u_1} [Add M] : AddCommSemigroup { x : M // x ∈ AddSubsemigroup.center M }

The center of an additive magma is commutative and associative.

Equations

• AddSubsemigroup.center.addCommSemigroup = AddCommSemigroup.mk ⋯

instance Subsemigroup.center.commSemigroup {M : Type u_1} [Mul M] : CommSemigroup { x : M // x ∈ Subsemigroup.center M }

The center of a magma is commutative and associative.

Equations

• Subsemigroup.center.commSemigroup = CommSemigroup.mk ⋯

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

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

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

Equations

• AddSubsemigroup.decidableMemCenter a = decidable_of_iff' (∀ (g : M), g + a = a + g) ⋯

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

Equations

• Subsemigroup.decidableMemCenter a = decidable_of_iff' (∀ (g : M), g * a = a * g) ⋯

@[simp]

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

@[simp]

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