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) [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 = { toAddSubsemigroup := { carrier := Set.addCenter M, add_mem' := ⋯ }, zero_mem' := ⋯ }

theorem AddSubmonoid.center.proof_1 (M : Type u_1) [AddZeroClass M] : ∀ {a b : M}, a ∈ Set.addCenter M → b ∈ Set.addCenter M → a + b ∈ Set.addCenter M

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 = { toSubsemigroup := { carrier := Set.center M, mul_mem' := ⋯ }, one_mem' := ⋯ }

theorem AddSubmonoid.coe_center (M : Type u_1) [AddZeroClass M] : ↑(AddSubmonoid.center M) = Set.addCenter M

theorem Submonoid.coe_center (M : Type u_1) [MulOneClass M] : ↑(Submonoid.center M) = Set.center M

@[simp]

theorem AddSubmonoid.center_toAddSubsemigroup (M : Type u_1) [AddZeroClass M] : (AddSubmonoid.center M).toAddSubsemigroup = AddSubsemigroup.center M

@[simp]

theorem Submonoid.center_toSubsemigroup (M : Type u_1) [MulOneClass M] : (Submonoid.center M).toSubsemigroup = Subsemigroup.center M

theorem AddSubmonoid.center.addCommMonoid'.proof_6 {M : Type u_1} [AddZeroClass M] (a : ↥(AddSubsemigroup.center M)) (b : ↥(AddSubsemigroup.center M)) : a + b = b + a

theorem AddSubmonoid.center.addCommMonoid'.proof_1 {M : Type u_1} [AddZeroClass M] (a : ↥(AddSubsemigroup.center M)) (b : ↥(AddSubsemigroup.center M)) (c : ↥(AddSubsemigroup.center M)) : a + b + c = a + (b + c)

theorem AddSubmonoid.center.addCommMonoid'.proof_4 {M : Type u_1} [AddZeroClass M] : ∀ (x : ↥(AddSubmonoid.center M)), nsmulRec 0 x = nsmulRec 0 x

abbrev AddSubmonoid.center.addCommMonoid' {M : Type u_1} [AddZeroClass M] : AddCommMonoid ↥(AddSubmonoid.center M)

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

Equations

• AddSubmonoid.center.addCommMonoid' = let __src := AddSubmonoid.toAddZeroClass (AddSubmonoid.center M); let __src_1 := AddSubsemigroup.center.addCommSemigroup; AddCommMonoid.mk ⋯

theorem AddSubmonoid.center.addCommMonoid'.proof_3 {M : Type u_1} [AddZeroClass M] (a : ↥(AddSubmonoid.center M)) : a + 0 = a

theorem AddSubmonoid.center.addCommMonoid'.proof_5 {M : Type u_1} [AddZeroClass M] : ∀ (n : ℕ) (x : ↥(AddSubmonoid.center M)), nsmulRec (n + 1) x = nsmulRec (n + 1) x

theorem AddSubmonoid.center.addCommMonoid'.proof_2 {M : Type u_1} [AddZeroClass M] (a : ↥(AddSubmonoid.center M)) : 0 + a = a

@[inline, reducible]

abbrev Submonoid.center.commMonoid' {M : Type u_1} [MulOneClass M] : CommMonoid ↥(Submonoid.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

• Submonoid.center.commMonoid' = let __src := Submonoid.toMulOneClass (Submonoid.center M); let __src_1 := Subsemigroup.center.commSemigroup; CommMonoid.mk ⋯

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

Equations

• AddSubmonoid.center.addCommMonoid = let __src := AddSubmonoid.toAddMonoid (AddSubmonoid.center M); let __src_1 := AddSubsemigroup.center.addCommSemigroup; AddCommMonoid.mk ⋯

theorem AddSubmonoid.center.addCommMonoid.proof_1 {M : Type u_1} [AddMonoid M] (a : ↥(AddSubsemigroup.center M)) (b : ↥(AddSubsemigroup.center M)) : a + b = b + a

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

The center of a monoid is commutative.

Equations

• Submonoid.center.commMonoid = let __src := Submonoid.toMonoid (Submonoid.center M); let __src_1 := Subsemigroup.center.commSemigroup; CommMonoid.mk ⋯

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)] : Decidable (a ∈ AddSubmonoid.center M)

Equations

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

instance Submonoid.decidableMemCenter {M : Type u_1} [Monoid M] (a : M) [Decidable (∀ (b : M), b * a = a * b)] : Decidable (a ∈ Submonoid.center M)

Equations

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

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

The center of a monoid acts commutatively on that monoid.

Equations

• ⋯ = ⋯

instance Submonoid.center.smulCommClass_right {M : Type u_1} [Monoid M] : SMulCommClass M (↥(Submonoid.center 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) [CommMonoid M] : Submonoid.center M = ⊤

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 = AddMonoidHom.codRestrict (AddUnits.map (AddSubmonoid.subtype (AddSubmonoid.center M))) (AddSubmonoid.center (AddUnits M)) ⋯

theorem addUnitsCenterToCenterAddUnits.proof_2 (M : Type u_1) [AddMonoid M] (u : AddUnits ↥(AddSubmonoid.center M)) : (AddUnits.map (AddSubmonoid.subtype (AddSubmonoid.center M))) u ∈ AddSubmonoid.center (AddUnits M)

theorem addUnitsCenterToCenterAddUnits.proof_1 (M : Type u_1) [AddMonoid M] : AddSubmonoidClass (AddSubmonoid (AddUnits M)) (AddUnits M)

@[simp]

theorem val_addUnitsCenterToCenterAddUnits_apply_coe (M : Type u_1) [AddMonoid M] (n : AddUnits ↥(AddSubmonoid.center M)) : ↑↑((addUnitsCenterToCenterAddUnits M) n) = ↑↑n

@[simp]

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

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 when it is is for groups with zero, which is covered in centerUnitsEquivUnitsCenter.

Equations

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

theorem addUnitsCenterToCenterAddUnits_injective (M : Type u_1) [AddMonoid M] : Function.Injective ⇑(addUnitsCenterToCenterAddUnits M)

theorem unitsCenterToCenterUnits_injective (M : Type u_1) [Monoid M] : Function.Injective ⇑(unitsCenterToCenterUnits M)