Mathlib.GroupTheory.Submonoid.Center

Submonoid.center definition

: Submonoid M

Full source

/-- The center of a multiplication with unit `M` is the set of elements that commute with everything
in `M` -/
@[to_additive
      "The center of an addition with zero `M` is the set of elements that commute with everything
      in `M`"]
def center : Submonoid M where
  carrier := Set.center M
  one_mem' := Set.one_mem_center
  mul_mem' := Set.mul_mem_center

Center of a monoid

Informal description

The center of a monoid $ M $ is the submonoid consisting of all elements $ z \in M $ that commute with every element of $ M $, i.e., $ z \cdot m = m \cdot z $ for all $ m \in M $.

Submonoid.coe_center theorem

: ↑(center M) = Set.center M

Full source

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

Center Submonoid as Set of Central Elements

Informal description

The underlying set of the center of a monoid $M$ is equal to the set of central elements of $M$, i.e., $\{z \in M \mid \forall m \in M, z \cdot m = m \cdot z\}$.

Submonoid.center_toSubsemigroup theorem

: (center M).toSubsemigroup = Subsemigroup.center M

Full source

@[to_additive (attr := simp) AddSubmonoid.center_toAddSubsemigroup]
theorem center_toSubsemigroup : (center M).toSubsemigroup = Subsemigroup.center M :=
  rfl

Equality of Monoid Center and Semigroup Center Structures

Informal description

The subsemigroup obtained from the center of a monoid $M$ is equal to the center of $M$ viewed as a subsemigroup. That is, $(Z(M)).\text{toSubsemigroup} = Z_{\text{semigroup}}(M)$, where $Z(M)$ denotes the center of $M$ as a monoid and $Z_{\text{semigroup}}(M)$ denotes the center of $M$ as a semigroup.

Submonoid.center.commMonoid' abbrev

: CommMonoid (center M)

Full source

/-- The center of a multiplication with unit is commutative and associative.

This is not an instance as it forms an non-defeq diamond with `Submonoid.toMonoid` in the `npow`
field. -/
@[to_additive "The center of an addition with zero is commutative and associative."]
abbrev center.commMonoid' : CommMonoid (center M) :=
  { (center M).toMulOneClass, Subsemigroup.center.commSemigroup with }

Commutative Monoid Structure on the Center of a Monoid

Informal description

The center of a monoid $M$ forms a commutative monoid under the same multiplication operation as $M$.

Submonoid.center.commMonoid instance

: CommMonoid (center M)

Full source

/-- The center of a monoid is commutative. -/
@[to_additive]
instance center.commMonoid : CommMonoid (center M) :=
  { (center M).toMonoid, Subsemigroup.center.commSemigroup with }

Commutative Monoid Structure on the Center of a Monoid

Informal description

The center of a monoid $M$ forms a commutative monoid under the same operation as $M$.

Submonoid.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 Elements in the Center of a Monoid

Informal description

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

Submonoid.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' _ mem_center_iff

Decidability of Membership in the Center of a Monoid

Informal description

For any monoid $M$ and element $a \in M$, if there is a decision procedure to determine whether $a$ commutes with every element of $M$ (i.e., whether $b * a = a * b$ for all $b \in M$), then there is a decision procedure to determine whether $a$ belongs to the center of $M$.

Submonoid.center.smulCommClass_left instance

: SMulCommClass (center M) M M

Full source

/-- The center of a monoid acts commutatively on that monoid. -/
instance center.smulCommClass_left : SMulCommClass (center M) M M where
  smul_comm m x y := Commute.left_comm (m.prop.comm x) y

Commutative Action of the Center on a Monoid

Informal description

For any monoid $M$, the center of $M$ acts commutatively on $M$. That is, for any $z$ in the center of $M$ and any $m \in M$, we have $z \cdot m = m \cdot z$.

Submonoid.center.smulCommClass_right instance

: SMulCommClass M (center M) M

Full source

/-- The center of a monoid acts commutatively on that monoid. -/
instance center.smulCommClass_right : SMulCommClass M (center M) M :=
  SMulCommClass.symm _ _ _

Commutative Action of a Monoid via its Center

Informal description

For any monoid $M$, the monoid $M$ acts commutatively on itself via its center. That is, for any $m \in M$ and any $z$ in the center of $M$, we have $m \cdot z = z \cdot m$.

Submonoid.center_eq_top theorem

: center M = ⊤

Full source

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

Characterization of Commutative Monoids via Center: $Z(M) = M$

Informal description

The center of a monoid $M$ is equal to the entire monoid (i.e., $Z(M) = M$) if and only if $M$ is commutative.

unitsCenterToCenterUnits definition

[Monoid M] : (Submonoid.center M)ˣ →* Submonoid.center (Mˣ)

Full source

/-- For a monoid, the units of the center inject into the center of the units. This is not an
equivalence in general; one case when it is is for groups with zero, which is covered in
`centerUnitsEquivUnitsCenter`. -/
@[to_additive (attr := simps! apply_coe_val)
  "For an additive monoid, the units of the center inject into the center of the units."]
def unitsCenterToCenterUnits [Monoid M] : (Submonoid.center M)ˣ(Submonoid.center M)ˣ →* Submonoid.center (Mˣ) :=
  (Units.map (Submonoid.center M).subtype).codRestrict _ <|
      fun u ↦ Submonoid.mem_center_iff.mpr <|
        fun r ↦ Units.ext <| by
        rw [Units.val_mul, Units.coe_map, Submonoid.coe_subtype, Units.val_mul, Units.coe_map,
          Submonoid.coe_subtype, u.1.prop.comm r]

Inclusion of units of the center into the center of units

Informal description

For a monoid $ M $, the function maps units of the center of $ M $ to the center of the units of $ M $. Specifically, it takes a unit $ u $ in the center of $ M $ and returns the corresponding unit in $ M $ that lies in the center of the units of $ M $. This is achieved by restricting the canonical map from units of the center to units of $ M $ to those units that commute with all other units in $ M $.

unitsCenterToCenterUnits_injective theorem

[Monoid M] : Function.Injective (unitsCenterToCenterUnits M)

Full source

@[to_additive]
theorem unitsCenterToCenterUnits_injective [Monoid M] :
    Function.Injective (unitsCenterToCenterUnits M) :=
  fun _a _b h => Units.ext <| Subtype.ext <| congr_arg (Units.valUnits.val ∘ Subtype.val) h

Injectivity of the Unit Center Map: $Z(M)^\times \hookrightarrow Z(M^\times)$

Informal description

For any monoid $M$, the canonical map from the units of the center of $M$ to the center of the units of $M$ is injective. In other words, if two units in the center of $M$ have the same image in the center of the units of $M$, then they must be equal.

MulEquivClass.apply_mem_center theorem

 {F} [EquivLike F M N] [Mul M] [Mul N] [MulEquivClass F M N] (e : F) {x : M} (hx : x ∈ Set.center M) :
  e x ∈ Set.center N

Full source

@[to_additive] theorem _root_.MulEquivClass.apply_mem_center {F} [EquivLike F M N] [Mul M] [Mul N]
    [MulEquivClass F M N] (e : F) {x : M} (hx : x ∈ Set.center M) : e x ∈ Set.center N := by
  let e := MulEquivClass.toMulEquiv e
  show e x ∈ Set.center N
  constructor <;>
  (intros; apply e.symm.injective;
    simp only [map_mul, e.symm_apply_apply, (isMulCentral_iff _).mp hx])

Multiplicative Equivalence Preserves Center Elements

Informal description

Let $M$ and $N$ be multiplicative structures with multiplication operations, and let $F$ be a type equipped with an equivalence relation and a multiplicative equivalence structure between $M$ and $N$. For any multiplicative equivalence $e : F$ and any element $x \in M$ that belongs to the center of $M$, the image $e(x)$ belongs to the center of $N$.

MulEquivClass.apply_mem_center_iff theorem

 {F} [EquivLike F M N] [Mul M] [Mul N] [MulEquivClass F M N] (e : F) {x : M} : e x ∈ Set.center N ↔ x ∈ Set.center M

Full source

@[to_additive] theorem _root_.MulEquivClass.apply_mem_center_iff {F} [EquivLike F M N]
    [Mul M] [Mul N] [MulEquivClass F M N] (e : F) {x : M} :
    e x ∈ Set.center Ne x ∈ Set.center N ↔ x ∈ Set.center M :=
  ⟨(by simpa using MulEquivClass.apply_mem_center (MulEquivClass.toMulEquiv e).symm ·),
    MulEquivClass.apply_mem_center e⟩

Multiplicative Equivalence Preserves Center Membership if and only if

Informal description

Let $M$ and $N$ be multiplicative structures with multiplication operations, and let $F$ be a type equipped with an equivalence relation and a multiplicative equivalence structure between $M$ and $N$. For any multiplicative equivalence $e : F$ and any element $x \in M$, the image $e(x)$ belongs to the center of $N$ if and only if $x$ belongs to the center of $M$.

Subsemigroup.centerCongr definition

[Mul M] [Mul N] (e : M ≃* N) : center M ≃* center N

Full source

/-- The center of isomorphic magmas are isomorphic. -/
@[to_additive (attr := simps) "The center of isomorphic additive magmas are isomorphic."]
def Subsemigroup.centerCongr [Mul M] [Mul N] (e : M ≃* N) : centercenter M ≃* center N where
  toFun r := ⟨e r, MulEquivClass.apply_mem_center e r.2⟩
  invFun s := ⟨e.symm s, MulEquivClass.apply_mem_center e.symm s.2⟩
  left_inv _ := Subtype.ext (e.left_inv _)
  right_inv _ := Subtype.ext (e.right_inv _)
  map_mul' _ _ := Subtype.ext (map_mul ..)

Isomorphism of centers of magmas under multiplicative isomorphism

Informal description

Given two magmas $M$ and $N$ with multiplication operations, and a multiplicative isomorphism $e : M \simeq N$, the centers of $M$ and $N$ are isomorphic as magmas. Specifically, the isomorphism $e$ restricts to an isomorphism between $\text{center}(M)$ and $\text{center}(N)$, where $\text{center}(M)$ denotes the subset of $M$ consisting of elements that commute with all elements of $M$.

Submonoid.centerCongr definition

[MulOneClass M] [MulOneClass N] (e : M ≃* N) : center M ≃* center N

Full source

/-- The center of isomorphic monoids are isomorphic. -/
@[to_additive (attr := simps!) "The center of isomorphic additive monoids are isomorphic."]
def Submonoid.centerCongr [MulOneClass M] [MulOneClass N] (e : M ≃* N) : centercenter M ≃* center N :=
  Subsemigroup.centerCongr e

Isomorphism of centers of monoids under multiplicative isomorphism

Informal description

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

MulOpposite.op_mem_center_iff theorem

[Mul M] {x : M} : op x ∈ Set.center Mᵐᵒᵖ ↔ x ∈ Set.center M

Full source

@[to_additive] theorem MulOpposite.op_mem_center_iff [Mul M] {x : M} :
    opop x ∈ Set.center Mᵐᵒᵖop x ∈ Set.center Mᵐᵒᵖ ↔ x ∈ Set.center M := by
  simp_rw [Set.mem_center_iff, isMulCentral_iff, MulOpposite.forall, ← op_mul, op_inj]; aesop

Characterization of Opposite Elements in the Center of Opposite Monoid

Informal description

Let $M$ be a multiplicative structure. For any element $x \in M$, the opposite element $\mathrm{op}(x)$ belongs to the center of the opposite monoid $M^\mathrm{op}$ if and only if $x$ belongs to the center of $M$.

MulOpposite.unop_mem_center_iff theorem

[Mul M] {x : Mᵐᵒᵖ} : unop x ∈ Set.center M ↔ x ∈ Set.center Mᵐᵒᵖ

Full source

@[to_additive] theorem MulOpposite.unop_mem_center_iff [Mul M] {x : Mᵐᵒᵖ} :
    unopunop x ∈ Set.center Munop x ∈ Set.center M ↔ x ∈ Set.center Mᵐᵒᵖ :=
  op_mem_center_iff.symm

Characterization of Unopposite Elements in the Center of a Monoid

Informal description

Let $M$ be a multiplicative structure. For any element $x$ in the opposite monoid $M^\mathrm{op}$, the element $\mathrm{unop}(x)$ belongs to the center of $M$ if and only if $x$ belongs to the center of $M^\mathrm{op}$.

Subsemigroup.centerToMulOpposite definition

[Mul M] : center M ≃* center Mᵐᵒᵖ

Full source

/-- The center of a magma is isomorphic to the center of its opposite. -/
@[to_additive (attr := simps)
"The center of an additive magma is isomorphic to the center of its opposite."]
def Subsemigroup.centerToMulOpposite [Mul M] : centercenter M ≃* center Mᵐᵒᵖ where
  toFun r := ⟨_, MulOpposite.op_mem_center_iff.mpr r.2⟩
  invFun r := ⟨_, MulOpposite.unop_mem_center_iff.mpr r.2⟩
  left_inv _ := rfl
  right_inv _ := rfl
  map_mul' r _ := Subtype.ext (congr_arg MulOpposite.op <| r.2.1 _)

Isomorphism between the center of a magma and its opposite

Informal description

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

Submonoid.centerToMulOpposite definition

[MulOneClass M] : center M ≃* center Mᵐᵒᵖ

Full source

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

Isomorphism between the center of a monoid and its opposite

Informal description

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

Main definitions