Mathlib.GroupTheory.Subsemigroup.Center

Module docstring

{"# 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. "}

Subsemigroup.center definition

: Subsemigroup M

Full source

/-- The center of a semigroup `M` is the set of elements that commute with everything in `M` -/
@[to_additive
      "The center of a semigroup `M` is the set of elements that commute with everything in `M`"]
def center : Subsemigroup M where
  carrier := Set.center M
  mul_mem' := Set.mul_mem_center

Center of a semigroup as a subsemigroup

Informal description

The center of a semigroup $ M $ is the subsemigroup consisting of all elements $ z \in M $ that commute with every element in $ M $, i.e., $ z * g = g * z $ for all $ g \in M $.

Subsemigroup.center.commSemigroup instance

: CommSemigroup (center M)

Full source

/-- The center of a magma is commutative and associative. -/
@[to_additive "The center of an additive magma is commutative and associative."]
instance center.commSemigroup : CommSemigroup (center M) where
  mul_assoc _ b _ := Subtype.ext <| b.2.mid_assoc _ _
  mul_comm a _ := Subtype.ext <| a.2.comm _

Commutative Semigroup Structure on the Center of a Semigroup

Informal description

The center of a semigroup $M$, consisting of all elements that commute with every element of $M$, forms a commutative semigroup under the same operation as $M$.

Subsemigroup.mem_center_iff theorem

{z : M} : z ∈ center M ↔ ∀ g, g * z = z * g

Full source

@[to_additive]
theorem mem_center_iff {z : M} : z ∈ center Mz ∈ center M ↔ ∀ g, g * z = z * g := by
  rw [← Semigroup.mem_center_iff]
  exact Iff.rfl

Characterization of Central Elements in a Semigroup

Informal description

An element $z$ in a semigroup $M$ belongs to the center of $M$ if and only if it commutes with every element $g \in M$, i.e., $g * z = z * g$ for all $g \in M$.

Subsemigroup.decidableMemCenter instance

(a) [Decidable <| ∀ b : M, b * a = a * b] : Decidable (a ∈ center M)

Full source

@[to_additive]
instance decidableMemCenter (a) [Decidable <| ∀ b : M, b * a = a * b] :
    Decidable (a ∈ center M) :=
  decidable_of_iff' _ Semigroup.mem_center_iff

Decidability of Membership in the Center of a Semigroup

Informal description

For any semigroup $M$ and element $a \in M$, if it is decidable whether $a$ commutes with every element of $M$ (i.e., $b * a = a * b$ for all $b \in M$), then membership in the center of $M$ is decidable for $a$.

Subsemigroup.center_eq_top theorem

: center M = ⊤

Full source

@[to_additive (attr := simp)]
theorem center_eq_top : center M = ⊤ :=
  SetLike.coe_injective (Set.center_eq_univ M)

Characterization of Commutative Semigroups via Center

Informal description

The center of a semigroup $M$ is equal to the entire semigroup (denoted by $\top$) if and only if $M$ is commutative, i.e., $g * h = h * g$ for all $g, h \in M$.