Documentation

Mathlib.GroupTheory.Submonoid.Center

Centers of monoids #

Main definitions #

We provide Subgroup.center, AddSubgroup.center, Subsemiring.center, and Subring.center in other files.

The center of an addition with zero M is the set of elements that commute with everything in M

Equations

The center of a multiplication with unit M is the set of elements that commute with everything in M

Equations
@[reducible, inline]

The center of an addition with zero is commutative and associative.

Equations
@[reducible, inline]

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.

Equations
Equations

The center of a monoid is commutative.

Equations
theorem AddSubmonoid.mem_center_iff {M : Type u_1} [AddMonoid M] {z : M} :
z AddSubmonoid.center M ∀ (g : M), g + z = z + g
theorem Submonoid.mem_center_iff {M : Type u_1} [Monoid M] {z : M} :
z Submonoid.center M ∀ (g : M), g * z = z * g
instance AddSubmonoid.decidableMemCenter {M : Type u_1} [AddMonoid M] (a : M) [Decidable (∀ (b : M), b + a = a + b)] :
Equations
instance Submonoid.decidableMemCenter {M : Type u_1} [Monoid M] (a : M) [Decidable (∀ (b : M), b * a = a * b)] :
Equations

The center of a monoid acts commutatively on that monoid.

Equations
  • =

The center of a monoid acts commutatively on that monoid.

Equations
  • =

Note that smulCommClass (center M) (center M) M is already implied by Submonoid.smulCommClass_right

For an additive monoid, the units of the center inject into the center of the units.

Equations
@[simp]
theorem val_unitsCenterToCenterUnits_apply_coe (M : Type u_1) [Monoid M] (n : (↥(Submonoid.center M))ˣ) :
((unitsCenterToCenterUnits M) n) = n

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.

Equations