Centers of magmas and monoids #
Main definitions #
set.center: the center of a magmasubmonoid.center: the center of a monoidset.add_center: the center of an additive magmaadd_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 magma.
Equations
- set.center M = {z : M | ∀ (m : M), m * z = z * m}
The center of an additive magma.
Equations
- set.add_center M = {z : M | ∀ (m : M), m + z = z + m}
@[protected, instance]
def
set.decidable_mem_center
(M : Type u_1)
[has_mul M]
[decidable_eq M]
[fintype M] :
decidable_pred (λ (_x : M), _x ∈ set.center M)
Equations
- set.decidable_mem_center M = λ (_x : M), decidable_of_iff' (∀ (g : M), g * _x = _x * g) _
@[simp]
@[simp]
theorem
set.mul_mem_center
{M : Type u_1}
[semigroup M]
{a b : M}
(ha : a ∈ set.center M)
(hb : b ∈ set.center M) :
a * b ∈ set.center M
@[simp]
theorem
set.add_mem_add_center
{M : Type u_1}
[add_semigroup M]
{a b : M}
(ha : a ∈ set.add_center M)
(hb : b ∈ set.add_center M) :
a + b ∈ set.add_center M
@[simp]
theorem
set.inv_mem_center
{M : Type u_1}
[group M]
{a : M}
(ha : a ∈ set.center M) :
a⁻¹ ∈ set.center M
@[simp]
theorem
set.neg_mem_add_center
{M : Type u_1}
[add_group M]
{a : M}
(ha : a ∈ set.add_center M) :
-a ∈ set.add_center M
@[simp]
theorem
set.add_mem_center
{M : Type u_1}
[distrib M]
{a b : M}
(ha : a ∈ set.center M)
(hb : b ∈ set.center M) :
a + b ∈ set.center M
@[simp]
theorem
set.neg_mem_center
{M : Type u_1}
[ring M]
{a : M}
(ha : a ∈ set.center M) :
-a ∈ set.center M
theorem
set.subset_center_units
{M : Type u_1}
[monoid M] :
coe ⁻¹' set.center M ⊆ set.center (units M)
theorem
set.subset_add_center_add_units
{M : Type u_1}
[add_monoid M] :
coe ⁻¹' set.add_center M ⊆ set.add_center (add_units M)
theorem
set.center_units_subset
{M : Type u_1}
[group_with_zero M] :
set.center (units M) ⊆ coe ⁻¹' set.center M
theorem
set.center_units_eq
{M : Type u_1}
[group_with_zero M] :
set.center (units M) = coe ⁻¹' set.center M
In a group with zero, the center of the units is the preimage of the center.
@[simp]
theorem
set.inv_mem_center₀
{M : Type u_1}
[group_with_zero M]
{a : M}
(ha : a ∈ set.center M) :
a⁻¹ ∈ set.center M
@[simp]
theorem
set.div_mem_center
{M : Type u_1}
[group M]
{a b : M}
(ha : a ∈ set.center M)
(hb : b ∈ set.center M) :
a / b ∈ set.center M
@[simp]
theorem
set.sub_mem_add_center
{M : Type u_1}
[add_group M]
{a b : M}
(ha : a ∈ set.add_center M)
(hb : b ∈ set.add_center M) :
a - b ∈ set.add_center M
@[simp]
theorem
set.div_mem_center₀
{M : Type u_1}
[group_with_zero M]
{a b : M}
(ha : a ∈ set.center M)
(hb : b ∈ set.center M) :
a / b ∈ set.center M
@[simp]
@[simp]
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), one_mem' := _, mul_mem' := _}
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), zero_mem' := _, add_mem' := _}
@[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 := _}
@[simp]