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}
[inst : Add M]
[inst : (a : M) → Decidable (∀ (b : M), b ∈ S → b + a = a + b)]
:
DecidablePred fun x => x ∈ Set.addCentralizer S
Equations
- Set.decidableMemAddCentralizer x = decidable_of_iff' (∀ (m : M), m ∈ S → m + x = x + m) (_ : x ∈ Set.addCentralizer S ↔ ∀ (m : M), m ∈ S → m + x = x + m)
instance
Set.decidableMemCentralizer
{M : Type u_1}
{S : Set M}
[inst : Mul M]
[inst : (a : M) → Decidable (∀ (b : M), b ∈ S → b * a = a * b)]
:
DecidablePred fun x => x ∈ Set.centralizer S
Equations
- Set.decidableMemCentralizer x = decidable_of_iff' (∀ (m : M), m ∈ S → m * x = x * m) (_ : x ∈ Set.centralizer S ↔ ∀ (m : M), m ∈ S → m * x = x * m)
@[simp]
theorem
Set.zero_mem_add_centralizer
{M : Type u_1}
(S : Set M)
[inst : AddZeroClass M]
:
0 ∈ Set.addCentralizer S
@[simp]
theorem
Set.one_mem_centralizer
{M : Type u_1}
(S : Set M)
[inst : MulOneClass M]
:
1 ∈ Set.centralizer S
@[simp]
theorem
Set.zero_mem_centralizer
{M : Type u_1}
(S : Set M)
[inst : MulZeroClass M]
:
0 ∈ Set.centralizer S
@[simp]
theorem
Set.add_mem_add_centralizer
{M : Type u_1}
{S : Set M}
{a : M}
{b : M}
[inst : 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}
[inst : Semigroup M]
(ha : a ∈ Set.centralizer S)
(hb : b ∈ Set.centralizer S)
:
a * b ∈ Set.centralizer S
@[simp]
theorem
Set.neg_mem_add_centralizer
{M : Type u_1}
{S : Set M}
{a : M}
[inst : 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}
[inst : 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}
[inst : 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}
[inst : Mul M]
[inst : 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}
[inst : GroupWithZero M]
(ha : a ∈ Set.centralizer S)
:
a⁻¹ ∈ Set.centralizer S
@[simp]
theorem
Set.sub_mem_add_centralizer
{M : Type u_1}
{S : Set M}
{a : M}
{b : M}
[inst : 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}
[inst : 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}
[inst : GroupWithZero M]
(ha : a ∈ Set.centralizer S)
(hb : b ∈ Set.centralizer S)
:
a / b ∈ Set.centralizer S
@[simp]
theorem
Set.add_centralizer_univ
(M : Type u_1)
[inst : Add M]
:
Set.addCentralizer Set.univ = Set.addCenter M
@[simp]
@[simp]
theorem
Set.add_centralizer_eq_univ
{M : Type u_1}
(S : Set M)
[inst : AddCommSemigroup M]
:
Set.addCentralizer S = Set.univ
@[simp]
theorem
Set.centralizer_eq_univ
{M : Type u_1}
(S : Set M)
[inst : CommSemigroup M]
:
Set.centralizer S = Set.univ
The centralizer of a subset of an additive semigroup.
Equations
- AddSubsemigroup.centralizer S = { carrier := Set.addCentralizer S, add_mem' := (_ : ∀ {a b : M}, a ∈ Set.addCentralizer S → b ∈ Set.addCentralizer S → a + b ∈ Set.addCentralizer S) }
def
AddSubsemigroup.centralizer.proof_1
{M : Type u_1}
(S : Set M)
[inst : AddSemigroup M]
:
∀ {a b : M}, a ∈ Set.addCentralizer S → b ∈ Set.addCentralizer S → a + b ∈ Set.addCentralizer S
Equations
- (_ : a ∈ Set.addCentralizer S → b ∈ Set.addCentralizer S → a + b ∈ Set.addCentralizer S) = (_ : a ∈ Set.addCentralizer S → b ∈ Set.addCentralizer S → a + b ∈ Set.addCentralizer S)
The centralizer of a subset of a semigroup M.
Equations
- Subsemigroup.centralizer S = { carrier := Set.centralizer S, mul_mem' := (_ : ∀ {a b : M}, a ∈ Set.centralizer S → b ∈ Set.centralizer S → a * b ∈ Set.centralizer S) }
@[simp]
@[simp]
theorem
AddSubsemigroup.mem_centralizer_iff
{M : Type u_1}
{S : Set M}
[inst : AddSemigroup M]
{z : M}
:
instance
AddSubsemigroup.decidableMemCentralizer
{M : Type u_1}
{S : Set M}
[inst : AddSemigroup M]
(a : M)
[inst : Decidable (∀ (b : M), b ∈ S → b + a = a + b)]
:
Equations
- AddSubsemigroup.decidableMemCentralizer a = decidable_of_iff' (∀ (g : M), g ∈ S → g + a = a + g) (_ : a ∈ AddSubsemigroup.centralizer S ↔ ∀ (g : M), g ∈ S → g + a = a + g)
instance
Subsemigroup.decidableMemCentralizer
{M : Type u_1}
{S : Set M}
[inst : Semigroup M]
(a : M)
[inst : Decidable (∀ (b : M), b ∈ S → b * a = a * b)]
:
Equations
- Subsemigroup.decidableMemCentralizer a = decidable_of_iff' (∀ (g : M), g ∈ S → g * a = a * g) (_ : a ∈ Subsemigroup.centralizer S ↔ ∀ (g : M), g ∈ S → g * a = a * g)
theorem
AddSubsemigroup.centralizer_le
{M : Type u_1}
{S : Set M}
{T : Set M}
[inst : AddSemigroup M]
(h : S ⊆ T)
:
@[simp]
theorem
AddSubsemigroup.centralizer_univ
(M : Type u_1)
[inst : AddSemigroup M]
:
AddSubsemigroup.centralizer Set.univ = AddSubsemigroup.center M
@[simp]
theorem
Subsemigroup.centralizer_univ
(M : Type u_1)
[inst : Semigroup M]
:
Subsemigroup.centralizer Set.univ = Subsemigroup.center M