Centralizers of magmas and semigroups #
Main definitions #
Set.centralizer
: the centralizer of a subset of a magmaSubsemigroup.centralizer
: the centralizer of a subset of a semigroupSet.addCentralizer
: the centralizer of a subset of an additive magmaAddSubsemigroup.centralizer
: the centralizer of a subset of an additive semigroup
We provide Monoid.centralizer
, AddMonoid.centralizer
, Subgroup.centralizer
, and
AddSubgroup.centralizer
in other files.
instance
Set.decidableMemAddCentralizer
{M : Type u_1}
{S : Set M}
[Add M]
[(a : M) → Decidable (∀ (b : M), b ∈ S → b + a = a + b)]
:
DecidablePred fun x => x ∈ Set.addCentralizer S
instance
Set.decidableMemCentralizer
{M : Type u_1}
{S : Set M}
[Mul M]
[(a : M) → Decidable (∀ (b : M), b ∈ S → b * a = a * b)]
:
DecidablePred fun x => x ∈ Set.centralizer S
@[simp]
theorem
Set.zero_mem_addCentralizer
{M : Type u_1}
(S : Set M)
[AddZeroClass M]
:
0 ∈ Set.addCentralizer S
@[simp]
@[simp]
@[simp]
theorem
Set.add_mem_addCentralizer
{M : Type u_1}
{S : Set M}
{a : M}
{b : M}
[AddSemigroup M]
(ha : a ∈ Set.addCentralizer S)
(hb : b ∈ Set.addCentralizer S)
:
a + b ∈ Set.addCentralizer S
@[simp]
theorem
Set.mul_mem_centralizer
{M : Type u_1}
{S : Set M}
{a : M}
{b : M}
[Semigroup M]
(ha : a ∈ Set.centralizer S)
(hb : b ∈ Set.centralizer S)
:
a * b ∈ Set.centralizer S
@[simp]
theorem
Set.neg_mem_addCentralizer
{M : Type u_1}
{S : Set M}
{a : M}
[AddGroup M]
(ha : a ∈ Set.addCentralizer S)
:
-a ∈ Set.addCentralizer S
@[simp]
theorem
Set.inv_mem_centralizer
{M : Type u_1}
{S : Set M}
{a : M}
[Group M]
(ha : a ∈ Set.centralizer S)
:
a⁻¹ ∈ Set.centralizer S
@[simp]
theorem
Set.add_mem_centralizer
{M : Type u_1}
{S : Set M}
{a : M}
{b : M}
[Distrib M]
(ha : a ∈ Set.centralizer S)
(hb : b ∈ Set.centralizer S)
:
a + b ∈ Set.centralizer S
@[simp]
theorem
Set.neg_mem_centralizer
{M : Type u_1}
{S : Set M}
{a : M}
[Mul M]
[HasDistribNeg M]
(ha : a ∈ Set.centralizer S)
:
-a ∈ Set.centralizer S
@[simp]
theorem
Set.inv_mem_centralizer₀
{M : Type u_1}
{S : Set M}
{a : M}
[GroupWithZero M]
(ha : a ∈ Set.centralizer S)
:
a⁻¹ ∈ Set.centralizer S
@[simp]
theorem
Set.sub_mem_addCentralizer
{M : Type u_1}
{S : Set M}
{a : M}
{b : M}
[AddGroup M]
(ha : a ∈ Set.addCentralizer S)
(hb : b ∈ Set.addCentralizer S)
:
a - b ∈ Set.addCentralizer S
@[simp]
theorem
Set.div_mem_centralizer
{M : Type u_1}
{S : Set M}
{a : M}
{b : M}
[Group M]
(ha : a ∈ Set.centralizer S)
(hb : b ∈ Set.centralizer S)
:
a / b ∈ Set.centralizer S
@[simp]
theorem
Set.div_mem_centralizer₀
{M : Type u_1}
{S : Set M}
{a : M}
{b : M}
[GroupWithZero M]
(ha : a ∈ Set.centralizer S)
(hb : b ∈ Set.centralizer S)
:
a / b ∈ Set.centralizer S
@[simp]
theorem
Set.addCentralizer_eq_top_iff_subset
{M : Type u_1}
{s : Set M}
[Add M]
:
Set.addCentralizer s = Set.univ ↔ s ⊆ Set.addCenter M
@[simp]
theorem
Set.centralizer_eq_top_iff_subset
{M : Type u_1}
{s : Set M}
[Mul M]
:
Set.centralizer s = Set.univ ↔ s ⊆ Set.center M
@[simp]
theorem
Set.addCentralizer_univ
(M : Type u_1)
[Add M]
:
Set.addCentralizer Set.univ = Set.addCenter M
@[simp]
@[simp]
theorem
Set.addCentralizer_eq_univ
{M : Type u_1}
(S : Set M)
[AddCommSemigroup M]
:
Set.addCentralizer S = Set.univ
@[simp]
theorem
Set.centralizer_eq_univ
{M : Type u_1}
(S : Set M)
[CommSemigroup M]
:
Set.centralizer S = Set.univ
The centralizer of a subset of an additive semigroup.
Instances For
The centralizer of a subset of a semigroup M
.
Instances For
@[simp]
@[simp]
instance
AddSubsemigroup.decidableMemCentralizer
{M : Type u_1}
{S : Set M}
[AddSemigroup M]
(a : M)
[Decidable (∀ (b : M), b ∈ S → b + a = a + b)]
:
theorem
AddSubsemigroup.centralizer_le
{M : Type u_1}
{S : Set M}
{T : Set M}
[AddSemigroup M]
(h : S ⊆ T)
:
@[simp]
theorem
AddSubsemigroup.centralizer_eq_top_iff_subset
{M : Type u_1}
[AddSemigroup M]
{s : Set M}
:
AddSubsemigroup.centralizer s = ⊤ ↔ s ⊆ ↑(AddSubsemigroup.center M)
@[simp]
theorem
Subsemigroup.centralizer_eq_top_iff_subset
{M : Type u_1}
[Semigroup M]
{s : Set M}
:
Subsemigroup.centralizer s = ⊤ ↔ s ⊆ ↑(Subsemigroup.center M)
@[simp]
theorem
AddSubsemigroup.centralizer_univ
(M : Type u_1)
[AddSemigroup M]
:
AddSubsemigroup.centralizer Set.univ = AddSubsemigroup.center M
@[simp]
theorem
Subsemigroup.centralizer_univ
(M : Type u_1)
[Semigroup M]
:
Subsemigroup.centralizer Set.univ = Subsemigroup.center M