Mathlib.GroupTheory.Subgroup.Center

Subgroup.center definition

: Subgroup G

Full source

/-- The center of a group `G` is the set of elements that commute with everything in `G` -/
@[to_additive
      "The center of an additive group `G` is the set of elements that commute with
      everything in `G`"]
def center : Subgroup G :=
  { Submonoid.center G with
    carrier := Set.center G
    inv_mem' := Set.inv_mem_center }

Center of a group

Informal description

The center of a group $ G $ is the subgroup consisting of all elements $ z \in G $ that commute with every element of $ G $, i.e., $ z \cdot g = g \cdot z $ for all $ g \in G $. It is constructed as a submonoid of $ G $ with the additional property that it is closed under taking inverses.

Subgroup.coe_center theorem

: ↑(center G) = Set.center G

Full source

@[to_additive]
theorem coe_center : ↑(center G) = Set.center G :=
  rfl

Equality of Group Center and Set Center

Informal description

The underlying set of the center of a group $G$ is equal to the center of $G$ as a set, i.e., $\overline{\text{center}(G)} = \text{Set.center}(G)$, where $\overline{\text{center}(G)}$ denotes the underlying set of the subgroup $\text{center}(G)$.

Subgroup.center_toSubmonoid theorem

: (center G).toSubmonoid = Submonoid.center G

Full source

@[to_additive (attr := simp)]
theorem center_toSubmonoid : (center G).toSubmonoid = Submonoid.center G :=
  rfl

Equality of Group Center's Submonoid and Monoid Center

Informal description

For any group $G$, the underlying submonoid of its center is equal to the center of $G$ as a monoid. That is, $(Z(G)).\text{toSubmonoid} = Z_{\text{monoid}}(G)$, where $Z(G)$ denotes the center of $G$ as a group and $Z_{\text{monoid}}(G)$ denotes the center of $G$ as a monoid.

Subgroup.center.isMulCommutative instance

: IsMulCommutative (center G)

Full source

instance center.isMulCommutative : IsMulCommutative (center G) :=
  ⟨⟨fun a b => Subtype.ext (b.2.comm a).symm⟩⟩

Commutativity of the Center of a Group

Informal description

The center of a group $G$ is commutative under the group operation. That is, for any two elements $z_1, z_2$ in the center of $G$, we have $z_1 \cdot z_2 = z_2 \cdot z_1$.

Subgroup.centerCongr definition

{H} [Group H] (e : G ≃* H) : center G ≃* center H

Full source

/-- The center of isomorphic groups are isomorphic. -/
@[to_additive (attr := simps!) "The center of isomorphic additive groups are isomorphic."]
def centerCongr {H} [Group H] (e : G ≃* H) : centercenter G ≃* center H := Submonoid.centerCongr e

Isomorphism of centers of groups under multiplicative isomorphism

Informal description

Given two groups $ G $ and $ H $, and a multiplicative isomorphism $ e : G \simeq H $, the centers of $ G $ and $ H $ are isomorphic as groups. Specifically, the isomorphism $ e $ restricts to an isomorphism between $ \text{center}(G) $ and $ \text{center}(H) $, where $ \text{center}(G) $ denotes the subgroup of $ G $ consisting of elements that commute with every element of $ G $.

Subgroup.centerToMulOpposite definition

: center G ≃* center Gᵐᵒᵖ

Full source

/-- The center of a group is isomorphic to the center of its opposite. -/
@[to_additive (attr := simps!)
"The center of an additive group is isomorphic to the center of its opposite."]
def centerToMulOpposite : centercenter G ≃* center Gᵐᵒᵖ := Submonoid.centerToMulOpposite

Isomorphism between the center of a group and its opposite

Informal description

The center of a group $ G $ is isomorphic as a multiplicative structure to the center of its multiplicative opposite $ G^{\text{op}} $. The isomorphism maps an element $ z $ in the center of $ G $ to its opposite in $ G^{\text{op}} $, and vice versa, preserving the multiplicative structure.

Subgroup.mem_center_iff theorem

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

Full source

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

Characterization of Central Elements in a Group

Informal description

An element $z$ of a group $G$ belongs to the center of $G$ if and only if $z$ commutes with every element $g$ of $G$, i.e., $g \cdot z = z \cdot g$ for all $g \in G$.

Subgroup.decidableMemCenter instance

(z : G) [Decidable (∀ g, g * z = z * g)] : Decidable (z ∈ center G)

Full source

instance decidableMemCenter (z : G) [Decidable (∀ g, g * z = z * g)] : Decidable (z ∈ center G) :=
  decidable_of_iff' _ mem_center_iff

Decidability of Membership in the Center of a Group

Informal description

For any group $G$ and element $z \in G$, if there is a decision procedure to determine whether $z$ commutes with every element of $G$ (i.e., $g \cdot z = z \cdot g$ for all $g \in G$), then there is a decision procedure to determine whether $z$ belongs to the center of $G$.

Subgroup.centerCharacteristic instance

: (center G).Characteristic

Full source

@[to_additive]
instance centerCharacteristic : (center G).Characteristic := by
  refine characteristic_iff_comap_le.mpr fun ϕ g hg => ?_
  rw [mem_center_iff]
  intro h
  rw [← ϕ.injective.eq_iff, map_mul, map_mul]
  exact (hg.comm (ϕ h)).symm

The Center is a Characteristic Subgroup

Informal description

The center of a group $G$ is a characteristic subgroup, meaning it is preserved by all automorphisms of $G$.

CommGroup.center_eq_top theorem

{G : Type*} [CommGroup G] : center G = ⊤

Full source

theorem _root_.CommGroup.center_eq_top {G : Type*} [CommGroup G] : center G = ⊤ := by
  rw [eq_top_iff']
  intro x
  rw [Subgroup.mem_center_iff]
  intro y
  exact mul_comm y x

Center of a Commutative Group is the Whole Group

Informal description

For any commutative group $G$, the center of $G$ is equal to the entire group, i.e., $\text{center}(G) = G$.

Group.commGroupOfCenterEqTop definition

(h : center G = ⊤) : CommGroup G

Full source

/-- A group is commutative if the center is the whole group -/
def _root_.Group.commGroupOfCenterEqTop (h : center G = ⊤) : CommGroup G :=
  { ‹Group G› with
    mul_comm := by
      rw [eq_top_iff'] at h
      intro x y
      apply Subgroup.mem_center_iff.mp _ x
      exact h y
  }

Commutative group structure from center condition

Informal description

Given a group $ G $ whose center equals the entire group (i.e., $ \text{center}(G) = G $), then $ G $ is a commutative group. That is, the group operation is commutative: $ x \cdot y = y \cdot x $ for all $ x, y \in G $.

Subgroup.center_le_normalizer theorem

: center G ≤ H.normalizer

Full source

@[to_additive]
theorem center_le_normalizer : center G ≤ H.normalizer := fun x hx y => by
  simp [← mem_center_iff.mp hx y, mul_assoc]

Center is Contained in Normalizer of Any Subgroup

Informal description

For any subgroup $H$ of a group $G$, the center of $G$ is contained in the normalizer of $H$, i.e., $\text{center}(G) \leq \text{normalizer}(H)$.

ConjClasses.mk_bijOn theorem

(G : Type*) [Group G] : Set.BijOn ConjClasses.mk (↑(Subgroup.center G)) (noncenter G)ᶜ

Full source

theorem mk_bijOn (G : Type*) [Group G] :
    Set.BijOn ConjClasses.mk (↑(Subgroup.center G)) (noncenter G)ᶜ := by
  refine ⟨fun g hg ↦ ?_, fun x hx y _ H ↦ ?_, ?_⟩
  · simp only [mem_noncenter, Set.compl_def, Set.mem_setOf, Set.not_nontrivial_iff]
    intro x hx y hy
    simp only [mem_carrier_iff_mk_eq, mk_eq_mk_iff_isConj] at hx hy
    rw [hx.eq_of_right_mem_center hg, hy.eq_of_right_mem_center hg]
  · rw [mk_eq_mk_iff_isConj] at H
    exact H.eq_of_left_mem_center hx
  · rintro ⟨g⟩ hg
    refine ⟨g, ?_, rfl⟩
    simp only [mem_noncenter, Set.compl_def, Set.mem_setOf, Set.not_nontrivial_iff] at hg
    rw [SetLike.mem_coe, Subgroup.mem_center_iff]
    intro h
    rw [← mul_inv_eq_iff_eq_mul]
    refine hg ?_ mem_carrier_mk
    rw [mem_carrier_iff_mk_eq]
    apply mk_eq_mk_iff_isConj.mpr
    rw [isConj_comm, isConj_iff]
    exact ⟨h, rfl⟩

Bijection Between Group Center and Central Conjugacy Classes

Informal description

Let $G$ be a group. The function that maps each element to its conjugacy class is a bijection between: 1. The center of $G$ (viewed as a set), and 2. The complement of the set of non-central conjugacy classes of $G$. In other words, the map $\text{ConjClasses.mk}$ restricted to the center of $G$ is bijective onto the set of conjugacy classes that are central (i.e., singleton conjugacy classes).