Mathlib.GroupTheory.Subsemigroup.Centralizer

Module docstring

{"# Centralizers in semigroups, as subsemigroups.

Main definitions

Subsemigroup.centralizer: the centralizer of a subset of a semigroup
AddSubsemigroup.centralizer: the centralizer of a subset of an additive semigroup

We provide Monoid.centralizer, AddMonoid.centralizer, Subgroup.centralizer, and AddSubgroup.centralizer in other files. "}

Subsemigroup.centralizer definition

: Subsemigroup M

Full source

/-- The centralizer of a subset of a semigroup `M`. -/
@[to_additive "The centralizer of a subset of an additive semigroup."]
def centralizer : Subsemigroup M where
  carrier := S.centralizer
  mul_mem' := Set.mul_mem_centralizer

Centralizer subsemigroup

Informal description

The centralizer of a subset $ S $ of a semigroup $ M $ is the subsemigroup consisting of all elements $ c \in M $ that commute with every element of $ S $, i.e., $ m \cdot c = c \cdot m $ for all $ m \in S $.

Subsemigroup.coe_centralizer theorem

: ↑(centralizer S) = S.centralizer

Full source

@[to_additive (attr := simp, norm_cast)]
theorem coe_centralizer : ↑(centralizer S) = S.centralizer :=
  rfl

Underlying Set of Centralizer Subsemigroup Equals Centralizer

Informal description

The underlying set of the centralizer subsemigroup of a subset $S$ in a semigroup $M$ is equal to the centralizer of $S$ in $M$, i.e., $\{c \in M \mid \forall m \in S, m \cdot c = c \cdot m\}$.

Subsemigroup.mem_centralizer_iff theorem

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

Full source

@[to_additive]
theorem mem_centralizer_iff {z : M} : z ∈ centralizer Sz ∈ centralizer S ↔ ∀ g ∈ S, g * z = z * g :=
  Iff.rfl

Characterization of Centralizer Elements in a Semigroup

Informal description

An element $z$ in a semigroup $M$ belongs to the centralizer of a subset $S \subseteq M$ if and only if $z$ commutes with every element of $S$, i.e., for all $g \in S$, we have $g \cdot z = z \cdot g$.

Subsemigroup.decidableMemCentralizer instance

(a) [Decidable <| ∀ b ∈ S, b * a = a * b] : Decidable (a ∈ centralizer S)

Full source

@[to_additive]
instance decidableMemCentralizer (a) [Decidable <| ∀ b ∈ S, b * a = a * b] :
    Decidable (a ∈ centralizer S) :=
  decidable_of_iff' _ mem_centralizer_iff

Decidability of Membership in Centralizer Subsemigroup

Informal description

For any element $a$ in a semigroup $M$ and subset $S \subseteq M$, if there is a decision procedure to determine whether $a$ commutes with every element of $S$ (i.e., $\forall b \in S, b * a = a * b$), then there is a decision procedure to determine whether $a$ belongs to the centralizer subsemigroup of $S$.

Subsemigroup.center_le_centralizer theorem

(S) : center M ≤ centralizer S

Full source

@[to_additive]
theorem center_le_centralizer (S) : center M ≤ centralizer S :=
  S.center_subset_centralizer

Center is Contained in Centralizer of Any Subset

Informal description

For any subset $S$ of a semigroup $M$, the center of $M$ is contained in the centralizer of $S$, i.e., $\text{center}(M) \leq \text{centralizer}(S)$.

Subsemigroup.centralizer_le theorem

(h : S ⊆ T) : centralizer T ≤ centralizer S

Full source

@[to_additive]
theorem centralizer_le (h : S ⊆ T) : centralizer T ≤ centralizer S :=
  Set.centralizer_subset h

Centralizer Antimonotonicity: $S \subseteq T$ implies $\text{centralizer}(T) \leq \text{centralizer}(S)$

Informal description

For any subsets $S$ and $T$ of a semigroup $M$, if $S \subseteq T$, then the centralizer of $T$ is contained in the centralizer of $S$, i.e., $\text{centralizer}(T) \leq \text{centralizer}(S)$.

Subsemigroup.centralizer_eq_top_iff_subset theorem

{s : Set M} : centralizer s = ⊤ ↔ s ⊆ center M

Full source

@[to_additive (attr := simp)]
theorem centralizer_eq_top_iff_subset {s : Set M} : centralizercentralizer s = ⊤ ↔ s ⊆ center M :=
  SetLike.ext'_iff.trans Set.centralizer_eq_top_iff_subset

Centralizer Equals Entire Semigroup iff Subset is Central

Informal description

For any subset $s$ of a semigroup $M$, the centralizer of $s$ is equal to the entire semigroup (i.e., $\text{centralizer}(s) = M$) if and only if $s$ is contained in the center of $M$ (i.e., $s \subseteq \text{center}(M)$).

Subsemigroup.centralizer_univ theorem

: centralizer Set.univ = center M

Full source

@[to_additive (attr := simp)]
theorem centralizer_univ : centralizer Set.univ = center M :=
  SetLike.ext' (Set.centralizer_univ M)

Centralizer of Entire Semigroup Equals Its Center

Informal description

For any semigroup $M$, the centralizer of the universal set (all elements of $M$) is equal to the center of $M$, i.e., $\text{centralizer}(M) = \text{center}(M)$.

Subsemigroup.closure_le_centralizer_centralizer theorem

(s : Set M) : closure s ≤ centralizer (centralizer s)

Full source

@[to_additive]
lemma closure_le_centralizer_centralizer (s : Set M) :
    closure s ≤ centralizer (centralizer s) :=
  closure_le.mpr Set.subset_centralizer_centralizer

Subsemigroup Generated by a Set is Contained in its Double Centralizer

Informal description

For any subset $S$ of a semigroup $M$, the subsemigroup generated by $S$ is contained in the centralizer of the centralizer of $S$, i.e., $\langle S \rangle \leq \text{centralizer}(\text{centralizer}(S))$.

Subsemigroup.closureCommSemigroupOfComm abbrev

{s : Set M} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) : CommSemigroup (closure s)

Full source

/-- If all the elements of a set `s` commute, then `closure s` is a commutative semigroup. -/
@[to_additive
      "If all the elements of a set `s` commute, then `closure s` forms an additive
      commutative semigroup."]
abbrev closureCommSemigroupOfComm {s : Set M} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) :
    CommSemigroup (closure s) :=
  { MulMemClass.toSemigroup (closure s) with
    mul_comm := fun ⟨_, h₁⟩ ⟨_, h₂⟩ ↦
      have := closure_le_centralizer_centralizer s
      Subtype.ext <| Set.centralizer_centralizer_comm_of_comm hcomm _ (this h₁) _ (this h₂) }

Commutative Semigroup Generated by Commuting Elements

Informal description

Let $M$ be a semigroup and $s$ a subset of $M$ such that all elements of $s$ commute pairwise (i.e., $a * b = b * a$ for all $a, b \in s$). Then the subsemigroup generated by $s$ is a commutative semigroup.