Centers of monoids #
Main definitions #
submonoid.center
: the center of a monoidadd_submonoid.center
: the center of an additive monoid
We provide subgroup.center
, add_subgroup.center
, subsemiring.center
, and subring.center
in
other files.
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
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' := _}
@[simp]
@[protected, instance]
def
submonoid.decidable_mem_center
{M : Type u_1}
[monoid M]
[decidable_eq M]
[fintype M] :
decidable_pred (λ (_x : M), _x ∈ submonoid.center M)
Equations
- submonoid.decidable_mem_center = λ (_x : M), decidable_of_iff' (∀ (g : M), g * _x = _x * g) submonoid.mem_center_iff
@[protected, instance]
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 := _}
@[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.
@[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
@[simp]