Mathlib.Algebra.Group.Center

Module docstring

{"# Centers of magmas and semigroups

Main definitions

Set.center: the center of a magma
Set.addCenter: the center of an additive magma
Set.centralizer: the centralizer of a subset of a magma
Set.addCentralizer: the centralizer of a subset of an additive magma

/-- Conditions for an element to be additively central -/
structure IsAddCentral [Add M] (z : M) : Prop where
  /-- addition commutes -/
  comm (a : M) : z + a = a + z
  /-- associative property for left addition -/
  left_assoc (b c : M) : z + (b + c) = (z + b) + c
  /-- middle associative addition property -/
  mid_assoc (a c : M) : (a + z) + c = a + (z + c)
  /-- associative property for right addition -/
  right_assoc (a b : M) : (a + b) + z = a + (b + z)

Additively central element

Informal description

An element $ z $ of an additive magma $ M $ is called *additively central* if it commutes with all other elements under addition, i.e., for all $ x, y \in M $, we have $ z + (x + y) = x + (z + y) $.

IsMulCentral structure

[Mul M] (z : M)

Full source

/-- Conditions for an element to be multiplicatively central -/
@[to_additive]
structure IsMulCentral [Mul M] (z : M) : Prop where
  /-- multiplication commutes -/
  comm (a : M) : z * a = a * z
  /-- associative property for left multiplication -/
  left_assoc (b c : M) : z * (b * c) = (z * b) * c
  /-- middle associative multiplication property -/
  mid_assoc (a c : M) : (a * z) * c = a * (z * c)
  /-- associative property for right multiplication -/
  right_assoc (a b : M) : (a * b) * z = a * (b * z)

Multiplicatively Central Element in a Magma

Informal description

An element $ z $ in a multiplicative magma $ M $ is called *multiplicatively central* if it commutes with every other element in $ M $. That is, for all $ x, y \in M $, the following properties hold: 1. $ z \cdot (x \cdot y) = x \cdot (z \cdot y) $ (left commutativity) 2. $ (x \cdot y) \cdot z = (x \cdot z) \cdot y $ (right commutativity)

IsMulCentral.left_comm theorem

(h : IsMulCentral a) (b c) : a * (b * c) = b * (a * c)

Full source

@[to_additive]
protected theorem left_comm (h : IsMulCentral a) (b c) : a * (b * c) = b * (a * c) := by
  simp only [h.comm, h.right_assoc]

Left Commutativity Property of Central Elements in a Magma

Informal description

Let $M$ be a magma and let $a \in M$ be a multiplicatively central element. Then for any elements $b, c \in M$, the following left commutativity relation holds: $$a \cdot (b \cdot c) = b \cdot (a \cdot c)$$

IsMulCentral.right_comm theorem

(h : IsMulCentral c) (a b) : a * b * c = a * c * b

Full source

@[to_additive]
protected theorem right_comm (h : IsMulCentral c) (a b) : a * b * c = a * c * b := by
  simp only [h.right_assoc, h.mid_assoc, h.comm]

Right Commutativity Property of Central Elements in a Magma

Informal description

Let $M$ be a magma and let $c \in M$ be a multiplicatively central element. Then for any elements $a, b \in M$, the following right commutativity relation holds: $$(a \cdot b) \cdot c = (a \cdot c) \cdot b$$

Set.center definition

: Set M

Full source

/-- The center of a magma. -/
@[to_additive addCenter " The center of an additive magma. "]
def center : Set M :=
  { z | IsMulCentral z }

Center of a magma

Informal description

The center of a magma $ M $ is the set of all elements $ z \in M $ that are multiplicatively central, i.e., elements that commute with every other element in $ M $.

Set.centralizer definition

: Set M

Full source

/-- The centralizer of a subset of a magma. -/
@[to_additive addCentralizer " The centralizer of a subset of an additive magma. "]
def centralizer : Set M := {c | ∀ m ∈ S, m * c = c * m}

Centralizer of a subset in a magma

Informal description

The centralizer of a subset $ S $ of a magma $ M $ is the set of all elements $ c \in M $ that commute with every element of $ S $, i.e., $ m * c = c * m $ for all $ m \in S $.

Set.mem_center_iff theorem

{z : M} : z ∈ center M ↔ IsMulCentral z

Full source

@[to_additive mem_addCenter_iff]
theorem mem_center_iff {z : M} : z ∈ center Mz ∈ center M ↔ IsMulCentral z :=
  Iff.rfl

Characterization of Central Elements: $z \in \text{center}(M) \leftrightarrow \text{IsMulCentral}(z)$

Informal description

An element $z$ of a magma $M$ belongs to the center of $M$ if and only if $z$ is multiplicatively central, i.e., it commutes with every other element in $M$.

Set.mem_centralizer_iff theorem

{c : M} : c ∈ centralizer S ↔ ∀ m ∈ S, m * c = c * m

Full source

@[to_additive mem_addCentralizer]
lemma mem_centralizer_iff {c : M} : c ∈ centralizer Sc ∈ centralizer S ↔ ∀ m ∈ S, m * c = c * m := Iff.rfl

Characterization of Centralizer Elements: $c \in \text{centralizer}(S) \leftrightarrow \forall m \in S, m * c = c * m$

Informal description

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

Set.mul_mem_center theorem

{z₁ z₂ : M} (hz₁ : z₁ ∈ Set.center M) (hz₂ : z₂ ∈ Set.center M) : z₁ * z₂ ∈ Set.center M

Full source

@[to_additive (attr := simp) add_mem_addCenter]
theorem mul_mem_center {z₁ z₂ : M} (hz₁ : z₁ ∈ Set.center M) (hz₂ : z₂ ∈ Set.center M) :
    z₁ * z₂ ∈ Set.center M where
  comm a := calc
    z₁ * z₂ * a = z₂ * z₁ * a := by rw [hz₁.comm]
    _ = z₂ * (z₁ * a) := by rw [hz₁.mid_assoc z₂]
    _ = (a * z₁) * z₂ := by rw [hz₁.comm, hz₂.comm]
    _ = a * (z₁ * z₂) := by rw [hz₂.right_assoc a z₁]
  left_assoc (b c : M) := calc
    z₁ * z₂ * (b * c) = z₁ * (z₂ * (b * c)) := by rw [hz₂.mid_assoc]
    _ = z₁ * ((z₂ * b) * c) := by rw [hz₂.left_assoc]
    _ = (z₁ * (z₂ * b)) * c := by rw [hz₁.left_assoc]
    _ = z₁ * z₂ * b * c := by rw [hz₂.mid_assoc]
  mid_assoc (a c : M) := calc
    a * (z₁ * z₂) * c = ((a * z₁) * z₂) * c := by rw [hz₁.mid_assoc]
    _ = (a * z₁) * (z₂ * c) := by rw [hz₂.mid_assoc]
    _ = a * (z₁ * (z₂ * c)) := by rw [hz₁.mid_assoc]
    _ = a * (z₁ * z₂ * c) := by rw [hz₂.mid_assoc]
  right_assoc (a b : M) := calc
    a * b * (z₁ * z₂) = ((a * b) * z₁) * z₂ := by rw [hz₂.right_assoc]
    _ = (a * (b * z₁)) * z₂ := by rw [hz₁.right_assoc]
    _ =  a * ((b * z₁) * z₂) := by rw [hz₂.right_assoc]
    _ = a * (b * (z₁ * z₂)) := by rw [hz₁.mid_assoc]

Closure of Center under Multiplication in a Magma

Informal description

For any elements $z_1$ and $z_2$ in the center of a magma $M$, the product $z_1 * z_2$ also belongs to the center of $M$.

Set.center_subset_centralizer theorem

(S : Set M) : Set.center M ⊆ S.centralizer

Full source

@[to_additive addCenter_subset_addCentralizer]
lemma center_subset_centralizer (S : Set M) : Set.centerSet.center M ⊆ S.centralizer :=
  fun _ hx m _ ↦ (hx.comm m).symm

Center is Contained in Centralizer of Any Subset

Informal description

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

Set.centralizer_union theorem

: centralizer (S ∪ T) = centralizer S ∩ centralizer T

Full source

@[to_additive addCentralizer_union]
lemma centralizer_union : centralizer (S ∪ T) = centralizercentralizer S ∩ centralizer T := by
  simp [centralizer, or_imp, forall_and, setOf_and]

Centralizer of Union Equals Intersection of Centralizers

Informal description

For any subsets $S$ and $T$ of a magma $M$, the centralizer of the union $S \cup T$ is equal to the intersection of the centralizers of $S$ and $T$, i.e., \[ \text{centralizer}(S \cup T) = \text{centralizer}(S) \cap \text{centralizer}(T). \]

Set.centralizer_subset theorem

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

Full source

@[to_additive (attr := gcongr) addCentralizer_subset]
lemma centralizer_subset (h : S ⊆ T) : centralizercentralizer T ⊆ centralizer S := fun _ ht s hs ↦ ht s (h hs)

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

Informal description

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

Set.subset_centralizer_centralizer theorem

: S ⊆ S.centralizer.centralizer

Full source

@[to_additive subset_addCentralizer_addCentralizer]
lemma subset_centralizer_centralizer : S ⊆ S.centralizer.centralizer := by
  intro x hx
  simp only [Set.mem_centralizer_iff]
  exact fun y hy => (hy x hx).symm

Inclusion of a Set in its Double Centralizer

Informal description

For any subset $S$ of a magma $M$, the set $S$ is contained in the centralizer of its own centralizer, i.e., $S \subseteq \text{centralizer}(\text{centralizer}(S))$.

Set.centralizer_centralizer_centralizer theorem

(S : Set M) : S.centralizer.centralizer.centralizer = S.centralizer

Full source

@[to_additive (attr := simp) addCentralizer_addCentralizer_addCentralizer]
lemma centralizer_centralizer_centralizer (S : Set M) :
    S.centralizer.centralizer.centralizer = S.centralizer := by
  refine Set.Subset.antisymm ?_ Set.subset_centralizer_centralizer
  intro x hx
  rw [Set.mem_centralizer_iff]
  intro y hy
  rw [Set.mem_centralizer_iff] at hx
  exact hx y <| Set.subset_centralizer_centralizer hy

Triple Centralizer Identity: $\text{centralizer}^3(S) = \text{centralizer}(S)$

Informal description

For any subset $S$ of a magma $M$, the triple centralizer of $S$ equals the centralizer of $S$, i.e., $\text{centralizer}(\text{centralizer}(\text{centralizer}(S))) = \text{centralizer}(S)$.

Set.decidableMemCentralizer instance

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

Full source

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

Decidability of Centralizer Membership

Informal description

For any magma $ M $ and subset $ S \subseteq M $, if there exists a decision procedure to determine whether any element $ a \in M $ commutes with all elements of $ S $, then membership in the centralizer of $ S $ is decidable.

Set.centralizer_centralizer_comm_of_comm theorem

 (h_comm : ∀ x ∈ S, ∀ y ∈ S, x * y = y * x) :
  ∀ x ∈ S.centralizer.centralizer, ∀ y ∈ S.centralizer.centralizer, x * y = y * x

Full source

@[to_additive addCentralizer_addCentralizer_comm_of_comm]
lemma centralizer_centralizer_comm_of_comm (h_comm : ∀ x ∈ S, ∀ y ∈ S, x * y = y * x) :
    ∀ x ∈ S.centralizer.centralizer, ∀ y ∈ S.centralizer.centralizer, x * y = y * x :=
  fun _ h₁ _ h₂ ↦ h₂ _ fun _ h₃ ↦ h₁ _ fun _ h₄ ↦ h_comm _ h₄ _ h₃

Commutativity in the Double Centralizer of a Commutative Subset

Informal description

Let $S$ be a subset of a magma $M$ such that for all $x, y \in S$, $x * y = y * x$. Then for any $x, y$ in the double centralizer of $S$ (i.e., $x, y \in S^{\perp\perp}$), we have $x * y = y * x$.

Semigroup.mem_center_iff theorem

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

Full source

@[to_additive]
theorem _root_.Semigroup.mem_center_iff {z : M} :
    z ∈ Set.center Mz ∈ Set.center M ↔ ∀ g, g * z = z * g := ⟨fun a g ↦ by rw [IsMulCentral.comm a g],
  fun h ↦ ⟨fun _ ↦ (Commute.eq (h _)).symm, fun _ _ ↦ (mul_assoc z _ _).symm,
  fun _ _ ↦ mul_assoc _ z _, fun _ _ ↦ mul_assoc _ _ z⟩ ⟩

Characterization of Central Elements in a Magma

Informal description

An element $z$ in a magma $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$.

Set.mul_mem_centralizer theorem

(ha : a ∈ centralizer S) (hb : b ∈ centralizer S) : a * b ∈ centralizer S

Full source

@[to_additive (attr := simp) add_mem_addCentralizer]
lemma mul_mem_centralizer (ha : a ∈ centralizer S) (hb : b ∈ centralizer S) :
    a * b ∈ centralizer S := fun g hg ↦ by
  rw [mul_assoc, ← hb g hg, ← mul_assoc, ha g hg, mul_assoc]

Product of Centralizer Elements is in Centralizer

Informal description

For any elements $a$ and $b$ in the centralizer of a subset $S$ of a magma $M$, the product $a * b$ also belongs to the centralizer of $S$.

Set.centralizer_eq_top_iff_subset theorem

: centralizer S = Set.univ ↔ S ⊆ center M

Full source

@[to_additive (attr := simp) addCentralizer_eq_top_iff_subset]
theorem centralizer_eq_top_iff_subset : centralizercentralizer S = Set.univ ↔ S ⊆ center M :=
  eq_top_iff.trans <| ⟨
    fun h _ hx ↦ Semigroup.mem_center_iff.mpr fun _ ↦ by rw [h trivial _ hx],
    fun h _ _ _ hm ↦ (h hm).comm _⟩

Centralizer Equals Entire Magma iff Subset is Central

Informal description

The centralizer of a subset $S$ of a magma $M$ is equal to the entire magma (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)$).

Set.centralizer_univ theorem

: centralizer univ = center M

Full source

@[to_additive (attr := simp) addCentralizer_univ]
lemma centralizer_univ : centralizer univ = center M :=
  Subset.antisymm (fun _ ha ↦ Semigroup.mem_center_iff.mpr fun b ↦ ha b (Set.mem_univ b))
  fun _ ha b _ ↦ (ha.comm b).symm

Centralizer of Entire Magma Equals Its Center

Informal description

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

Set.decidableMemCenter instance

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

Full source

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

Decidability of Membership in the Center of a Magma

Informal description

For any magma $ M $ with a decidable equality on the condition $ \forall b \in M, b * a = a * b $ for each $ a \in M $, the predicate $ \cdot \in \text{center}(M) $ is decidable. In other words, given that for every element $ a $ in $ M $, it is decidable whether $ a $ commutes with all other elements in $ M $, we can decide whether any given element belongs to the center of $ M $.

Set.center_eq_univ theorem

: center M = univ

Full source

@[to_additive (attr := simp) addCenter_eq_univ]
theorem center_eq_univ : center M = univ :=
  (Subset.antisymm (subset_univ _)) fun _ _ => Semigroup.mem_center_iff.mpr (fun _ => mul_comm _ _)

Commutative Magma Characterization via Center

Informal description

The center of a magma $M$ is equal to the entire set $M$ if and only if $M$ is commutative, i.e., $z * g = g * z$ for all $z, g \in M$.

Set.centralizer_eq_univ theorem

: centralizer S = univ

Full source

@[to_additive (attr := simp) addCentralizer_eq_univ]
lemma centralizer_eq_univ : centralizer S = univ :=
  eq_univ_of_forall fun _ _ _ ↦ mul_comm _ _

Centralizer Equals Universe in Magma

Informal description

The centralizer of a subset $S$ in a magma $M$ is equal to the entire set $M$ if and only if every element of $M$ commutes with every element of $S$, i.e., $m * c = c * m$ for all $m \in S$ and $c \in M$.

Set.one_mem_center theorem

: (1 : M) ∈ Set.center M

Full source

@[to_additive (attr := simp) zero_mem_addCenter]
theorem one_mem_center : (1 : M) ∈ Set.center M where
  comm _  := by rw [one_mul, mul_one]
  left_assoc _ _ := by rw [one_mul, one_mul]
  mid_assoc _ _ := by rw [mul_one, one_mul]
  right_assoc _ _ := by rw [mul_one, mul_one]

Identity Element is Central in a Magma

Informal description

The multiplicative identity element $1$ of a magma $M$ belongs to its center, i.e., $1 \in \text{center}(M)$.

Set.one_mem_centralizer theorem

: (1 : M) ∈ centralizer S

Full source

@[to_additive (attr := simp) zero_mem_addCentralizer]
lemma one_mem_centralizer : (1 : M) ∈ centralizer S := by simp [mem_centralizer_iff]

Identity Element Belongs to Centralizer of Any Subset

Informal description

For any subset $S$ of a magma $M$ with a multiplicative identity element $1$, the identity element $1$ belongs to the centralizer of $S$, i.e., $1 \in \text{centralizer}(S)$.

Set.subset_center_units theorem

: ((↑) : Mˣ → M) ⁻¹' center M ⊆ Set.center Mˣ

Full source

@[to_additive subset_addCenter_add_units]
theorem subset_center_units : ((↑) : Mˣ → M) ⁻¹' center M((↑) : Mˣ → M) ⁻¹' center M ⊆ Set.center Mˣ :=
  fun _ ha => by
  rw [_root_.Semigroup.mem_center_iff]
  intro _
  rw [← Units.eq_iff, Units.val_mul, Units.val_mul, ha.comm]

Inclusion of Central Units into Center of Units

Informal description

The preimage of the center of a magma $M$ under the canonical inclusion map from the units $M^\times$ to $M$ is contained in the center of the units $M^\times$. In other words, if a unit $u \in M^\times$ is central in $M$, then $u$ is also central in $M^\times$.

Set.units_inv_mem_center theorem

{a : Mˣ} (ha : ↑a ∈ Set.center M) : ↑a⁻¹ ∈ Set.center M

Full source

@[to_additive (attr := simp)]
theorem units_inv_mem_center {a : Mˣ} (ha : ↑a ∈ Set.center M) : ↑a⁻¹ ∈ Set.center M := by
  rw [Semigroup.mem_center_iff] at *
  exact (Commute.units_inv_right <| ha ·)

Inverse of Central Unit is Central

Informal description

For any unit $a$ in a magma $M$ such that the underlying element $a$ belongs to the center of $M$, the inverse $a^{-1}$ also belongs to the center of $M$.

Set.invOf_mem_center theorem

{a : M} [Invertible a] (ha : a ∈ Set.center M) : ⅟ a ∈ Set.center M

Full source

@[simp]
theorem invOf_mem_center {a : M} [Invertible a] (ha : a ∈ Set.center M) : ⅟a⅟a ∈ Set.center M := by
  rw [Semigroup.mem_center_iff] at *
  exact (Commute.invOf_right <| ha ·)

Inverse of Central Invertible Element is Central

Informal description

For any element $a$ in the center of a magma $M$ that has a two-sided inverse $\inv{a}$, the inverse $\inv{a}$ also belongs to the center of $M$.

Set.inv_mem_center theorem

(ha : a ∈ Set.center M) : a⁻¹ ∈ Set.center M

Full source

@[to_additive (attr := simp) neg_mem_addCenter]
theorem inv_mem_center (ha : a ∈ Set.center M) : a⁻¹a⁻¹ ∈ Set.center M := by
  rw [_root_.Semigroup.mem_center_iff]
  intro _
  rw [← inv_inj, mul_inv_rev, inv_inv, ha.comm, mul_inv_rev, inv_inv]

Inverse of Central Element is Central

Informal description

For any element $a$ in the center of a magma $M$, the inverse $a^{-1}$ is also in the center of $M$.

Set.div_mem_center theorem

(ha : a ∈ Set.center M) (hb : b ∈ Set.center M) : a / b ∈ Set.center M

Full source

@[to_additive (attr := simp) sub_mem_addCenter]
theorem div_mem_center (ha : a ∈ Set.center M) (hb : b ∈ Set.center M) : a / b ∈ Set.center M := by
  rw [div_eq_mul_inv]
  exact mul_mem_center ha (inv_mem_center hb)

Closure of Center under Division in a Magma

Informal description

For any elements $a$ and $b$ in the center of a magma $M$, the quotient $a / b$ also belongs to the center of $M$.

Set.inv_mem_centralizer theorem

(ha : a ∈ centralizer S) : a⁻¹ ∈ centralizer S

Full source

@[to_additive (attr := simp) neg_mem_addCentralizer]
lemma inv_mem_centralizer (ha : a ∈ centralizer S) : a⁻¹a⁻¹ ∈ centralizer S :=
  fun g hg ↦ by rw [mul_inv_eq_iff_eq_mul, mul_assoc, eq_inv_mul_iff_mul_eq, ha g hg]

Inverse of Centralizer Element is in Centralizer

Informal description

For any element $a$ in the centralizer of a subset $S$ of a magma $M$, the inverse $a^{-1}$ is also in the centralizer of $S$.

Set.div_mem_centralizer theorem

(ha : a ∈ centralizer S) (hb : b ∈ centralizer S) : a / b ∈ centralizer S

Full source

@[to_additive (attr := simp) sub_mem_addCentralizer]
lemma div_mem_centralizer (ha : a ∈ centralizer S) (hb : b ∈ centralizer S) :
    a / b ∈ centralizer S := by
  simpa only [div_eq_mul_inv] using mul_mem_centralizer ha (inv_mem_centralizer hb)

Quotient of Centralizer Elements is in Centralizer

Informal description

For any elements $a$ and $b$ in the centralizer of a subset $S$ of a magma $M$, the quotient $a / b$ also belongs to the centralizer of $S$.

Main definitions

See also