Centralizers of magmas and monoids #
Main definitions #
set.centralizer: the center of a magmasubmonoid.centralizer: the center of a monoidset.add_centralizer: the center of an additive magmaadd_submonoid.centralizer: the center of an additive monoid
We provide subgroup.centralizer, add_subgroup.centralizer in other files.
@[protected, instance]
def
set.decidable_mem_add_centralizer
{M : Type u_1}
{S : set M}
[has_add M]
[decidable_eq M]
[fintype M]
[decidable_pred (λ (_x : M), _x ∈ S)] :
decidable_pred (λ (_x : M), _x ∈ S.add_centralizer)
Equations
- set.decidable_mem_add_centralizer = λ (_x : M), decidable_of_iff' (∀ (m : M), m ∈ S → m + _x = _x + m) set.mem_add_centralizer
@[protected, instance]
def
set.decidable_mem_centralizer
{M : Type u_1}
{S : set M}
[has_mul M]
[decidable_eq M]
[fintype M]
[decidable_pred (λ (_x : M), _x ∈ S)] :
decidable_pred (λ (_x : M), _x ∈ S.centralizer)
Equations
- set.decidable_mem_centralizer = λ (_x : M), decidable_of_iff' (∀ (m : M), m ∈ S → m * _x = _x * m) set.mem_centralizer_iff
@[simp]
theorem
set.zero_mem_add_centralizer
{M : Type u_1}
(S : set M)
[add_zero_class M] :
0 ∈ S.add_centralizer
@[simp]
@[simp]
@[simp]
theorem
set.mul_mem_centralizer
{M : Type u_1}
{S : set M}
{a b : M}
[semigroup M]
(ha : a ∈ S.centralizer)
(hb : b ∈ S.centralizer) :
a * b ∈ S.centralizer
@[simp]
theorem
set.add_mem_add_centralizer
{M : Type u_1}
{S : set M}
{a b : M}
[add_semigroup M]
(ha : a ∈ S.add_centralizer)
(hb : b ∈ S.add_centralizer) :
a + b ∈ S.add_centralizer
@[simp]
theorem
set.inv_mem_centralizer
{M : Type u_1}
{S : set M}
{a : M}
[group M]
(ha : a ∈ S.centralizer) :
a⁻¹ ∈ S.centralizer
@[simp]
theorem
set.neg_mem_add_centralizer
{M : Type u_1}
{S : set M}
{a : M}
[add_group M]
(ha : a ∈ S.add_centralizer) :
-a ∈ S.add_centralizer
@[simp]
theorem
set.add_mem_centralizer
{M : Type u_1}
{S : set M}
{a b : M}
[distrib M]
(ha : a ∈ S.centralizer)
(hb : b ∈ S.centralizer) :
a + b ∈ S.centralizer
@[simp]
theorem
set.neg_mem_centralizer
{M : Type u_1}
{S : set M}
{a : M}
[has_mul M]
[has_distrib_neg M]
(ha : a ∈ S.centralizer) :
-a ∈ S.centralizer
@[simp]
theorem
set.inv_mem_centralizer₀
{M : Type u_1}
{S : set M}
{a : M}
[group_with_zero M]
(ha : a ∈ S.centralizer) :
a⁻¹ ∈ S.centralizer
@[simp]
theorem
set.div_mem_centralizer
{M : Type u_1}
{S : set M}
{a b : M}
[group M]
(ha : a ∈ S.centralizer)
(hb : b ∈ S.centralizer) :
a / b ∈ S.centralizer
@[simp]
theorem
set.sub_mem_add_centralizer
{M : Type u_1}
{S : set M}
{a b : M}
[add_group M]
(ha : a ∈ S.add_centralizer)
(hb : b ∈ S.add_centralizer) :
a - b ∈ S.add_centralizer
@[simp]
theorem
set.div_mem_centralizer₀
{M : Type u_1}
{S : set M}
{a b : M}
[group_with_zero M]
(ha : a ∈ S.centralizer)
(hb : b ∈ S.centralizer) :
a / b ∈ S.centralizer
theorem
set.centralizer_subset
{M : Type u_1}
{S T : set M}
[has_mul M]
(h : S ⊆ T) :
T.centralizer ⊆ S.centralizer
@[simp]
@[simp]
@[simp]
@[simp]
The centralizer of a subset of a monoid M.
Equations
- submonoid.centralizer S = {carrier := S.centralizer (mul_one_class.to_has_mul M), mul_mem' := _, one_mem' := _}
The centralizer of a subset of an additive monoid.
Equations
- add_submonoid.centralizer S = {carrier := S.add_centralizer (add_zero_class.to_has_add M), add_mem' := _, zero_mem' := _}
@[simp, norm_cast]
@[simp, norm_cast]
@[protected, instance]
def
submonoid.decidable_mem_centralizer
{M : Type u_1}
{S : set M}
[monoid M]
[decidable_eq M]
[fintype M]
[decidable_pred (λ (_x : M), _x ∈ S)] :
decidable_pred (λ (_x : M), _x ∈ submonoid.centralizer S)
Equations
- submonoid.decidable_mem_centralizer = λ (_x : M), decidable_of_iff' (∀ (g : M), g ∈ S → g * _x = _x * g) submonoid.mem_centralizer_iff
@[protected, instance]
def
add_submonoid.decidable_mem_centralizer
{M : Type u_1}
{S : set M}
[add_monoid M]
[decidable_eq M]
[fintype M]
[decidable_pred (λ (_x : M), _x ∈ S)] :
decidable_pred (λ (_x : M), _x ∈ add_submonoid.centralizer S)
Equations
- add_submonoid.decidable_mem_centralizer = λ (_x : M), decidable_of_iff' (∀ (g : M), g ∈ S → g + _x = _x + g) add_submonoid.mem_centralizer_iff
@[simp]
@[simp]