# Centers of monoids #

## Main definitions #

• Submonoid.center: the center of a monoid
• AddSubmonoid.center: the center of an additive monoid

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

def AddSubmonoid.center (M : Type u_1) [] :

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

Equations
• = { carrier := , add_mem' := , zero_mem' := }
Instances For
theorem AddSubmonoid.center.proof_1 (M : Type u_1) [] :
∀ {a b : M}, a + b
def Submonoid.center (M : Type u_1) [] :

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

Equations
• = { carrier := , mul_mem' := , one_mem' := }
Instances For
theorem AddSubmonoid.coe_center (M : Type u_1) [] :
theorem Submonoid.coe_center (M : Type u_1) [] :
() =
@[simp]
@[simp]
theorem Submonoid.center_toSubsemigroup (M : Type u_1) [] :
().toSubsemigroup =
theorem AddSubmonoid.center.addCommMonoid'.proof_6 {M : Type u_1} [] (a : ) (b : ) :
a + b = b + a
theorem AddSubmonoid.center.addCommMonoid'.proof_1 {M : Type u_1} [] (a : ) (b : ) (c : ) :
a + b + c = a + (b + c)
∀ (x : ), nsmulRec 0 x = nsmulRec 0 x

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

Equations
Instances For
a + 0 = a
∀ (n : ) (x : ), nsmulRec (n + 1) x = nsmulRec (n + 1) x
0 + a = a
@[reducible, inline]
abbrev Submonoid.center.commMonoid' {M : Type u_1} [] :

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
• Submonoid.center.commMonoid' = let __src := ().toMulOneClass; let __src_1 := Subsemigroup.center.commSemigroup;
Instances For
Equations
theorem AddSubmonoid.center.addCommMonoid.proof_1 {M : Type u_1} [] (a : ) (b : ) :
a + b = b + a
instance Submonoid.center.commMonoid {M : Type u_1} [] :

The center of a monoid is commutative.

Equations
• Submonoid.center.commMonoid = let __src := ().toMonoid; let __src_1 := Subsemigroup.center.commSemigroup;
theorem AddSubmonoid.mem_center_iff {M : Type u_1} [] {z : M} :
∀ (g : M), g + z = z + g
theorem Submonoid.mem_center_iff {M : Type u_1} [] {z : M} :
∀ (g : M), g * z = z * g
instance AddSubmonoid.decidableMemCenter {M : Type u_1} [] (a : M) [Decidable (∀ (b : M), b + a = a + b)] :
Equations
instance Submonoid.decidableMemCenter {M : Type u_1} [] (a : M) [Decidable (∀ (b : M), b * a = a * b)] :
Equations
instance Submonoid.center.smulCommClass_left {M : Type u_1} [] :
SMulCommClass (()) M M

The center of a monoid acts commutatively on that monoid.

Equations
• =
instance Submonoid.center.smulCommClass_right {M : Type u_1} [] :
SMulCommClass M (()) M

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

@[simp]
theorem Submonoid.center_eq_top (M : Type u_1) [] :
→+ ()

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

Equations
Instances For
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.