# 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.

source
def Submonoid.center (M : Type u_1) [MulOneClass M] :
Submonoid M

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

Equations

- Submonoid.center M = { carrier := Set.center M, mul_mem' := ⋯, one_mem' := ⋯ }

Instances For

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

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

Equations

- AddSubmonoid.center M = { carrier := Set.addCenter M, add_mem' := ⋯, zero_mem' := ⋯ }

Instances For

source
theorem Submonoid.coe_center (M : Type u_1) [MulOneClass M] :
↑(center M) = Set.center M
source
theorem AddSubmonoid.coe_center (M : Type u_1) [AddZeroClass M] :
↑(center M) = Set.addCenter M
source
@[simp]
theorem Submonoid.center_toSubsemigroup (M : Type u_1) [MulOneClass M] :
(center M).toSubsemigroup = Subsemigroup.center M
source
@[simp]
theorem AddSubmonoid.center_toAddSubsemigroup (M : Type u_1) [AddZeroClass M] :
(center M).toAddSubsemigroup = AddSubsemigroup.center M
source
@[reducible, inline]
abbrev Submonoid.center.commMonoid' {M : Type u_1} [MulOneClass M] :
CommMonoid ↥(center M)

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

- One or more equations did not get rendered due to their size.

Instances For

source
@[reducible, inline]
abbrev AddSubmonoid.center.addCommMonoid' {M : Type u_1} [AddZeroClass M] :
AddCommMonoid ↥(center M)

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance Submonoid.center.commMonoid {M : Type u_1} [Monoid M] :
CommMonoid ↥(center M)

The center of a monoid is commutative.

Equations

- Submonoid.center.commMonoid = { toMonoid := (Submonoid.center M).toMonoid, mul_comm := ⋯ }

source
instance AddSubmonoid.center.addCommMonoid {M : Type u_1} [AddMonoid M] :
AddCommMonoid ↥(center M)
Equations

- AddSubmonoid.center.addCommMonoid = { toAddMonoid := (AddSubmonoid.center M).toAddMonoid, add_comm := ⋯ }

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

- Submonoid.decidableMemCenter a = decidable_of_iff' (∀ (g : M), g * a = a * g) ⋯

source
instance AddSubmonoid.decidableMemCenter {M : Type u_1} [AddMonoid M] (a : M) [Decidable (∀ (b : M), b + a = a + b)] :
Decidable (a ∈ center M)
Equations

- AddSubmonoid.decidableMemCenter a = decidable_of_iff' (∀ (g : M), g + a = a + g) ⋯

source
instance Submonoid.center.smulCommClass_left {M : Type u_1} [Monoid M] :
SMulCommClass (↥(center M)) M M

The center of a monoid acts commutatively on that monoid.

source
instance Submonoid.center.smulCommClass_right {M : Type u_1} [Monoid M] :
SMulCommClass M (↥(center M)) M

The center of a monoid acts commutatively on that monoid.

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

source
@[simp]
theorem Submonoid.center_eq_top (M : Type u_1) [CommMonoid M] :
center M = ⊤
source
def unitsCenterToCenterUnits (M : Type u_1) [Monoid M] :
(↥(Submonoid.center M))ˣ →* ↥(Submonoid.center M ˣ)

For a monoid, the units of the center inject into the center of the units. This is not an equivalence in general; one case where this holds is for groups with zero, which is covered in `centerUnitsEquivUnitsCenter`.

Equations

- unitsCenterToCenterUnits M = (Units.map (Submonoid.center M).subtype).codRestrict (Submonoid.center M ˣ) ⋯

Instances For

source
def addUnitsCenterToCenterAddUnits (M : Type u_1) [AddMonoid M] :
AddUnits ↥(AddSubmonoid.center M) →+ ↥(AddSubmonoid.center (AddUnits M))

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

Equations

- addUnitsCenterToCenterAddUnits M = (AddUnits.map (AddSubmonoid.center M).subtype).codRestrict (AddSubmonoid.center (AddUnits M)) ⋯

Instances For

source
@[simp]
theorem val_unitsCenterToCenterUnits_apply_coe (M : Type u_1) [Monoid M] (n : (↥(Submonoid.center M))ˣ) :
↑↑((unitsCenterToCenterUnits M) n) = ↑↑n
source
@[simp]
theorem val_addUnitsCenterToCenterAddUnits_apply_coe (M : Type u_1) [AddMonoid M] (n : AddUnits ↥(AddSubmonoid.center M)) :
↑↑((addUnitsCenterToCenterAddUnits M) n) = ↑↑n
source
theorem unitsCenterToCenterUnits_injective (M : Type u_1) [Monoid M] :
Function.Injective ⇑(unitsCenterToCenterUnits M)
source
theorem addUnitsCenterToCenterAddUnits_injective (M : Type u_1) [AddMonoid M] :
Function.Injective ⇑(addUnitsCenterToCenterAddUnits M)
source
theorem MulEquivClass.apply_mem_center {M : Type u_3} {N : Type u_1} {F : Type u_2} [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
source
theorem AddEquivClass.apply_mem_center {M : Type u_3} {N : Type u_1} {F : Type u_2} [EquivLike F M N] [Add M] [Add N] [AddEquivClass F M N] (e : F) {x : M} (hx : x ∈ Set.addCenter M) :
e x ∈ Set.addCenter N
source
theorem MulEquivClass.apply_mem_center_iff {M : Type u_3} {N : Type u_1} {F : Type u_2} [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
source
theorem AddEquivClass.apply_mem_center_iff {M : Type u_3} {N : Type u_1} {F : Type u_2} [EquivLike F M N] [Add M] [Add N] [AddEquivClass F M N] (e : F) {x : M} :
e x ∈ Set.addCenter N ↔ x ∈ Set.addCenter M
source
def Subsemigroup.centerCongr {M : Type u_2} {N : Type u_1} [Mul M] [Mul N] (e : M ≃* N) :
↥(center M) ≃* ↥(center N)

The center of isomorphic magmas are isomorphic.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def AddSubsemigroup.centerCongr {M : Type u_2} {N : Type u_1} [Add M] [Add N] (e : M ≃+ N) :
↥(center M) ≃+ ↥(center N)

The center of isomorphic additive magmas are isomorphic.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem Subsemigroup.centerCongr_symm_apply_coe {M : Type u_2} {N : Type u_1} [Mul M] [Mul N] (e : M ≃* N) (s : ↥(center N)) :
↑((centerCongr e).symm s) = e.symm ↑s
source
@[simp]
theorem AddSubsemigroup.centerCongr_symm_apply_coe {M : Type u_2} {N : Type u_1} [Add M] [Add N] (e : M ≃+ N) (s : ↥(center N)) :
↑((centerCongr e).symm s) = e.symm ↑s
source
@[simp]
theorem AddSubsemigroup.centerCongr_apply_coe {M : Type u_2} {N : Type u_1} [Add M] [Add N] (e : M ≃+ N) (r : ↥(center M)) :
↑((centerCongr e) r) = e ↑r
source
@[simp]
theorem Subsemigroup.centerCongr_apply_coe {M : Type u_2} {N : Type u_1} [Mul M] [Mul N] (e : M ≃* N) (r : ↥(center M)) :
↑((centerCongr e) r) = e ↑r
source
def Submonoid.centerCongr {M : Type u_2} {N : Type u_1} [MulOneClass M] [MulOneClass N] (e : M ≃* N) :
↥(center M) ≃* ↥(center N)

The center of isomorphic monoids are isomorphic.

Equations

- Submonoid.centerCongr e = Subsemigroup.centerCongr e

Instances For

source
def AddSubmonoid.centerCongr {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) :
↥(center M) ≃+ ↥(center N)

The center of isomorphic additive monoids are isomorphic.

Equations

- AddSubmonoid.centerCongr e = AddSubsemigroup.centerCongr e

Instances For

source
@[simp]
theorem AddSubmonoid.centerCongr_apply_coe {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) (r : ↥(AddSubsemigroup.center M)) :
↑((centerCongr e) r) = e ↑r
source
@[simp]
theorem Submonoid.centerCongr_symm_apply_coe {M : Type u_2} {N : Type u_1} [MulOneClass M] [MulOneClass N] (e : M ≃* N) (s : ↥(Subsemigroup.center N)) :
↑((centerCongr e).symm s) = e.symm ↑s
source
@[simp]
theorem AddSubmonoid.centerCongr_symm_apply_coe {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) (s : ↥(AddSubsemigroup.center N)) :
↑((centerCongr e).symm s) = e.symm ↑s
source
@[simp]
theorem Submonoid.centerCongr_apply_coe {M : Type u_2} {N : Type u_1} [MulOneClass M] [MulOneClass N] (e : M ≃* N) (r : ↥(Subsemigroup.center M)) :
↑((centerCongr e) r) = e ↑r
source
theorem MulOpposite.op_mem_center_iff {M : Type u_2} [Mul M] {x : M} :
op x ∈ Set.center M ᵐᵒᵖ ↔ x ∈ Set.center M
source
theorem AddOpposite.op_mem_center_iff {M : Type u_2} [Add M] {x : M} :
op x ∈ Set.addCenter M ᵃᵒᵖ ↔ x ∈ Set.addCenter M
source
theorem MulOpposite.unop_mem_center_iff {M : Type u_2} [Mul M] {x : M ᵐᵒᵖ} :
unop x ∈ Set.center M ↔ x ∈ Set.center M ᵐᵒᵖ
source
theorem AddOpposite.unop_mem_center_iff {M : Type u_2} [Add M] {x : M ᵃᵒᵖ} :
unop x ∈ Set.addCenter M ↔ x ∈ Set.addCenter M ᵃᵒᵖ
source
def Subsemigroup.centerToMulOpposite {M : Type u_2} [Mul M] :
↥(center M) ≃* ↥(center M ᵐᵒᵖ)

The center of a magma is isomorphic to the center of its opposite.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def AddSubsemigroup.centerToAddOpposite {M : Type u_2} [Add M] :
↥(center M) ≃+ ↥(center M ᵃᵒᵖ)

The center of an additive magma is isomorphic to the center of its opposite.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem Subsemigroup.centerToMulOpposite_apply_coe {M : Type u_2} [Mul M] (r : ↥(center M)) :
↑(centerToMulOpposite r) = MulOpposite.op ↑r
source
@[simp]
theorem AddSubsemigroup.centerToAddOpposite_symm_apply_coe {M : Type u_2} [Add M] (r : ↥(center M ᵃᵒᵖ)) :
↑(centerToAddOpposite.symm r) = AddOpposite.unop ↑r
source
@[simp]
theorem AddSubsemigroup.centerToAddOpposite_apply_coe {M : Type u_2} [Add M] (r : ↥(center M)) :
↑(centerToAddOpposite r) = AddOpposite.op ↑r
source
@[simp]
theorem Subsemigroup.centerToMulOpposite_symm_apply_coe {M : Type u_2} [Mul M] (r : ↥(center M ᵐᵒᵖ)) :
↑(centerToMulOpposite.symm r) = MulOpposite.unop ↑r
source
def Submonoid.centerToMulOpposite {M : Type u_2} [MulOneClass M] :
↥(center M) ≃* ↥(center M ᵐᵒᵖ)

The center of a monoid is isomorphic to the center of its opposite.

Equations

- Submonoid.centerToMulOpposite = Subsemigroup.centerToMulOpposite

Instances For

source
def AddSubmonoid.centerToAddOpposite {M : Type u_2} [AddZeroClass M] :
↥(center M) ≃+ ↥(center M ᵃᵒᵖ)

The center of an additive monoid is isomorphic to the center of its opposite.

Equations

- AddSubmonoid.centerToAddOpposite = AddSubsemigroup.centerToAddOpposite

Instances For

source
@[simp]
theorem AddSubmonoid.centerToAddOpposite_symm_apply_coe {M : Type u_2} [AddZeroClass M] (r : ↥(AddSubsemigroup.center M ᵃᵒᵖ)) :
↑(centerToAddOpposite.symm r) = AddOpposite.unop ↑r
source
@[simp]
theorem Submonoid.centerToMulOpposite_apply_coe {M : Type u_2} [MulOneClass M] (r : ↥(Subsemigroup.center M)) :
↑(centerToMulOpposite r) = MulOpposite.op ↑r
source
@[simp]
theorem Submonoid.centerToMulOpposite_symm_apply_coe {M : Type u_2} [MulOneClass M] (r : ↥(Subsemigroup.center M ᵐᵒᵖ)) :
↑(centerToMulOpposite.symm r) = MulOpposite.unop ↑r
source
@[simp]
theorem AddSubmonoid.centerToAddOpposite_apply_coe {M : Type u_2} [AddZeroClass M] (r : ↥(AddSubsemigroup.center M)) :
↑(centerToAddOpposite r) = AddOpposite.op ↑r