Mathlib.GroupTheory.Submonoid.Centralizer

Submonoid.centralizer definition

: Submonoid M

Full source

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

Centralizer of a subset in a monoid

Informal description

The centralizer of a subset $S$ of a monoid $M$ is the submonoid consisting of all elements $m \in M$ that commute with every element of $S$, i.e., $m * s = s * m$ for all $s \in S$.

Submonoid.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 Submonoid Equals Centralizer Set

Informal description

The underlying set of the centralizer submonoid of a subset $S$ in a monoid $M$ is equal to the centralizer of $S$ in $M$, i.e., $\overline{\text{centralizer}(S)} = \{m \in M \mid \forall s \in S, m * s = s * m\}$.

Submonoid.centralizer_toSubsemigroup theorem

: (centralizer S).toSubsemigroup = Subsemigroup.centralizer S

Full source

theorem centralizer_toSubsemigroup : (centralizer S).toSubsemigroup = Subsemigroup.centralizer S :=
  rfl

Submonoid Centralizer as Subsemigroup

Informal description

The subsemigroup obtained from the centralizer submonoid of a subset $S$ in a monoid $M$ is equal to the centralizer of $S$ in the underlying semigroup of $M$.

AddSubmonoid.centralizer_toAddSubsemigroup theorem

{M} [AddMonoid M] (S : Set M) : (AddSubmonoid.centralizer S).toAddSubsemigroup = AddSubsemigroup.centralizer S

Full source

theorem _root_.AddSubmonoid.centralizer_toAddSubsemigroup {M} [AddMonoid M] (S : Set M) :
    (AddSubmonoid.centralizer S).toAddSubsemigroup = AddSubsemigroup.centralizer S :=
  rfl

Centralizer as Additive Subsemigroup in Additive Monoid

Informal description

For any additive monoid $M$ and subset $S \subseteq M$, the underlying additive subsemigroup of the centralizer of $S$ in $M$ is equal to the centralizer of $S$ in the additive subsemigroup structure of $M$.

Submonoid.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 Membership in a Monoid

Informal description

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

Submonoid.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 monoid $M$, the center of $M$ is contained in the centralizer of $s$. In other words, every element of the center commutes with every element of $s$.

Submonoid.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 Centralizer Membership

Informal description

For any element $a$ in a monoid $M$ and subset $S \subseteq M$, if we can decide whether $a$ commutes with every element of $S$ (i.e., $\forall b \in S, b * a = a * b$), then we can decide whether $a$ belongs to the centralizer of $S$.

Submonoid.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

Monotonicity of Centralizer: $\text{centralizer}(T) \leq \text{centralizer}(S)$ when $S \subseteq T$

Informal description

For any subsets $S$ and $T$ of a monoid $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)$.

Submonoid.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 Monoid if and only if Subset is Central

Informal description

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

Submonoid.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 Monoid Equals Center

Informal description

The centralizer of the entire set of a monoid $M$ is equal to the center of $M$, i.e., $\text{centralizer}(M) = \text{center}(M)$.

Submonoid.le_centralizer_centralizer theorem

{s : Submonoid M} : s ≤ centralizer (centralizer (s : Set M))

Full source

@[to_additive]
lemma le_centralizer_centralizer {s : Submonoid M} : s ≤ centralizer (centralizer (s : Set M)) :=
  Set.subset_centralizer_centralizer

Submonoid containment in double centralizer

Informal description

For any submonoid $s$ of a monoid $M$, $s$ is contained in the centralizer of the centralizer of $s$ (viewed as a subset of $M$). In other words, every element of $s$ commutes with every element that commutes with all elements of $s$.

Submonoid.centralizer_centralizer_centralizer theorem

{s : Set M} : centralizer s.centralizer.centralizer = centralizer s

Full source

@[to_additive (attr := simp)]
lemma centralizer_centralizer_centralizer {s : Set M} :
    centralizer s.centralizer.centralizer = centralizer s := by
  apply SetLike.coe_injective
  simp only [coe_centralizer, Set.centralizer_centralizer_centralizer]

Triple Centralizer Identity in Monoids

Informal description

For any subset $s$ of a monoid $M$, the centralizer of the centralizer of the centralizer of $s$ is equal to the centralizer of $s$, i.e., $\text{centralizer}(\text{centralizer}(\text{centralizer}(s))) = \text{centralizer}(s)$.

Submonoid.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

Submonoid closure is contained in the double centralizer

Informal description

For any subset $s$ of a monoid $M$, the submonoid generated by $s$ is contained in the centralizer of the centralizer of $s$, i.e., $\text{closure}(s) \leq \text{centralizer}(\text{centralizer}(s))$.

Submonoid.closureCommMonoidOfComm abbrev

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

Full source

/-- If all the elements of a set `s` commute, then `closure s` is a commutative monoid. -/
@[to_additive
      "If all the elements of a set `s` commute, then `closure s` forms an additive
      commutative monoid."]
abbrev closureCommMonoidOfComm {s : Set M} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) :
    CommMonoid (closure s) :=
  { (closure s).toMonoid 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₂) }

Commutativity of Submonoid Closure for Commuting Elements

Informal description

Let $M$ be a monoid and $s$ a subset of $M$ such that every pair of elements in $s$ commutes (i.e., $a \cdot b = b \cdot a$ for all $a, b \in s$). Then the submonoid generated by $s$ (denoted $\text{closure}(s)$) is a commutative monoid.

Main definitions