Centers of monoids #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main definitions #

submonoid.center: the center of a monoid
add_submonoid.center: the center of an additive monoid

We provide subgroup.center, add_subgroup.center, subsemiring.center, and subring.center in other files.

source

def submonoid.center (M : Type u_1) [monoid M] :

submonoid M

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

Equations

submonoid.center M = {carrier := set.center M (mul_one_class.to_has_mul M), mul_mem' := _, one_mem' := _}

Instances for ↥submonoid.center

source

def add_submonoid.center (M : Type u_1) [add_monoid M] :

add_submonoid M

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

Equations

add_submonoid.center M = {carrier := set.add_center M (add_zero_class.to_has_add M), add_mem' := _, zero_mem' := _}

source

theorem add_submonoid.coe_center (M : Type u_1) [add_monoid M] :

↑(add_submonoid.center M) = set.add_center M

source

theorem submonoid.coe_center (M : Type u_1) [monoid M] :

↑(submonoid.center M) = set.center M

source

@[simp]

theorem submonoid.center_to_subsemigroup (M : Type u_1) [monoid M] :

(submonoid.center M).to_subsemigroup = subsemigroup.center M

source

theorem add_submonoid.center_to_add_subsemigroup (M : Type u_1) [add_monoid M] :

(add_submonoid.center M).to_add_subsemigroup = add_subsemigroup.center M

source

theorem add_submonoid.mem_center_iff {M : Type u_1} [add_monoid M] {z : M} :

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

source

theorem submonoid.mem_center_iff {M : Type u_1} [monoid M] {z : M} :

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

source

@[protected, instance]

def add_submonoid.decidable_mem_center {M : Type u_1} [add_monoid M] (a : M) [decidable (∀ (b : M), b + a = a + b)] :

decidable (a ∈ add_submonoid.center M)

Equations

add_submonoid.decidable_mem_center a = decidable_of_iff' (∀ (g : M), g + a = a + g) add_submonoid.mem_center_iff

source

@[protected, instance]

def submonoid.decidable_mem_center {M : Type u_1} [monoid M] (a : M) [decidable (∀ (b : M), b * a = a * b)] :

decidable (a ∈ submonoid.center M)

Equations

submonoid.decidable_mem_center a = decidable_of_iff' (∀ (g : M), g * a = a * g) submonoid.mem_center_iff

source

@[protected, instance]

def submonoid.center.comm_monoid {M : Type u_1} [monoid M] :

comm_monoid ↥(submonoid.center M)

The center of a monoid is commutative.

Equations

submonoid.center.comm_monoid = {mul := monoid.mul (submonoid.center M).to_monoid, mul_assoc := _, one := monoid.one (submonoid.center M).to_monoid, one_mul := _, mul_one := _, npow := monoid.npow (submonoid.center M).to_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _}

source

@[protected, instance]

def submonoid.center.smul_comm_class_left {M : Type u_1} [monoid M] :

smul_comm_class ↥(submonoid.center M) M M

The center of a monoid acts commutatively on that monoid.

source

@[protected, instance]

def submonoid.center.smul_comm_class_right {M : Type u_1} [monoid M] :

smul_comm_class M ↥(submonoid.center M) M

The center of a monoid acts commutatively on that monoid.

Note that smul_comm_class (center M) (center M) M is already implied by submonoid.smul_comm_class_right

source

@[simp]

theorem submonoid.center_eq_top (M : Type u_1) [comm_monoid M] :

submonoid.center M = ⊤