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

ink

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

AddSubmonoid M

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

Equations

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

source

ink

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

0 ∈ Set.addCenter M

Equations

(_ : 0 ∈ Set.addCenter M) = (_ : 0 ∈ Set.addCenter M)

source

ink

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

∀ {a b : M}, a ∈ Set.addCenter M → b ∈ Set.addCenter M → a + b ∈ Set.addCenter M

Equations

(_ : a ∈ Set.addCenter M → b ∈ Set.addCenter M → a + b ∈ Set.addCenter M) = (_ : a ∈ Set.addCenter M → b ∈ Set.addCenter M → a + b ∈ Set.addCenter M)

source

ink

def Submonoid.center (M : Type u_1) [inst : Monoid M] :

Submonoid M

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

Equations

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

source

ink

theorem AddSubmonoid.coe_center (M : Type u_1) [inst : AddMonoid M] :

↑(AddSubmonoid.center M) = Set.addCenter M

source

ink

theorem Submonoid.coe_center (M : Type u_1) [inst : Monoid M] :

↑(Submonoid.center M) = Set.center M

source

ink

@[simp]

theorem AddSubmonoid.center_toAddSubsemigroup (M : Type u_1) [inst : AddMonoid M] :

(AddSubmonoid.center M).toAddSubsemigroup = AddSubsemigroup.center M

source

ink

@[simp]

theorem Submonoid.center_toSubsemigroup (M : Type u_1) [inst : Monoid M] :

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

source

ink

theorem AddSubmonoid.mem_center_iff {M : Type u_1} [inst : AddMonoid M] {z : M} :

z ∈ AddSubmonoid.center M ↔ ∀ (g : M), g + z = z + g

source

ink

theorem Submonoid.mem_center_iff {M : Type u_1} [inst : Monoid M] {z : M} :

z ∈ Submonoid.center M ↔ ∀ (g : M), g * z = z * g

source

ink

instance AddSubmonoid.decidableMemCenter {M : Type u_1} [inst : AddMonoid M] (a : M) [inst : 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) (_ : a ∈ AddSubmonoid.center M ↔ ∀ (g : M), g + a = a + g)

source

ink

instance Submonoid.decidableMemCenter {M : Type u_1} [inst : Monoid M] (a : M) [inst : 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) (_ : a ∈ Submonoid.center M ↔ ∀ (g : M), g * a = a * g)

source

ink

instance Submonoid.center.commMonoid {M : Type u_1} [inst : Monoid M] :

CommMonoid { x // x ∈ Submonoid.center M }

The center of a monoid is commutative.

Equations

Submonoid.center.commMonoid = let src := Submonoid.toMonoid (Submonoid.center M); CommMonoid.mk (_ : ∀ (x b : { x // x ∈ Submonoid.center M }), x * b = b * x)

source

ink

instance Submonoid.center.smulCommClass_left {M : Type u_1} [inst : Monoid M] :

SMulCommClass { x // x ∈ Submonoid.center M } M M

The center of a monoid acts commutatively on that monoid.

Equations

@Submonoid.center.smulCommClass_left = @Submonoid.center.smulCommClass_left.proof_1

source

ink

instance Submonoid.center.smulCommClass_right {M : Type u_1} [inst : Monoid M] :

SMulCommClass M { x // x ∈ Submonoid.center M } M

The center of a monoid acts commutatively on that monoid.

Equations

@Submonoid.center.smulCommClass_right = @Submonoid.center.smulCommClass_right.proof_1

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

source

ink

@[simp]

theorem Submonoid.center_eq_top (M : Type u_1) [inst : CommMonoid M] :

Submonoid.center M = ⊤