Centers of magmas and semigroups #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Main definitions #
set.center: the center of a magmasubsemigroup.center: the center of a semigroupset.add_center: the center of an additive magmaadd_subsemigroup.center: the center of an additive semigroup
We provide submonoid.center, add_submonoid.center, subgroup.center, add_subgroup.center,
subsemiring.center, and subring.center in other files.
@[protected, instance]
def
set.decidable_mem_center
(M : Type u_1)
[has_mul M]
[Π (a : M), decidable (∀ (b : M), b * a = a * b)] :
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_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 Mˣ ⊆ coe ⁻¹' set.center M
theorem
set.center_units_eq
{M : Type u_1}
[group_with_zero M] :
set.center 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 semigroup M is the set of elements that commute with everything in M
Equations
- subsemigroup.center M = {carrier := set.center M (semigroup.to_has_mul M), mul_mem' := _}
Instances for ↥subsemigroup.center
The center of a semigroup M is the set of elements that commute with everything in
M
Equations
- add_subsemigroup.center M = {carrier := set.add_center M (add_semigroup.to_has_add M), add_mem' := _}
Instances for ↥add_subsemigroup.center
theorem
subsemigroup.coe_center
(M : Type u_1)
[semigroup M] :
↑(subsemigroup.center M) = set.center M
@[protected, instance]
def
subsemigroup.decidable_mem_center
{M : Type u_1}
[semigroup M]
(a : M)
[decidable (∀ (b : M), b * a = a * b)] :
decidable (a ∈ subsemigroup.center M)
Equations
- subsemigroup.decidable_mem_center a = decidable_of_iff' (∀ (g : M), g * a = a * g) subsemigroup.mem_center_iff
@[protected, instance]
def
add_subsemigroup.decidable_mem_center
{M : Type u_1}
[add_semigroup M]
(a : M)
[decidable (∀ (b : M), b + a = a + b)] :
Equations
- add_subsemigroup.decidable_mem_center a = decidable_of_iff' (∀ (g : M), g + a = a + g) add_subsemigroup.mem_center_iff
@[protected, instance]
The center of an additive semigroup is commutative.
Equations
@[protected, instance]
The center of a semigroup is commutative.
Equations
- subsemigroup.center.comm_semigroup = {mul := semigroup.mul (mul_mem_class.to_semigroup (subsemigroup.center M)), mul_assoc := _, mul_comm := _}
@[simp]
@[simp]