Centralizers of magmas and semigroups #

Main definitions #

Set.centralizer: the centralizer of a subset of a magma
Subsemigroup.centralizer: the centralizer of a subset of a semigroup
Set.addCentralizer: the centralizer of a subset of an additive magma
AddSubsemigroup.centralizer: the centralizer of a subset of an additive semigroup

We provide Monoid.centralizer, AddMonoid.centralizer, Subgroup.centralizer, and AddSubgroup.centralizer in other files.

source

def Set.addCentralizer {M : Type u_1} (S : Set M) [Add M] :

Set M

The centralizer of a subset of an additive magma.

Equations

Set.addCentralizer S = {c | ∀ (m : M), m ∈ S → m + c = c + m}

Instances For

source

def Set.centralizer {M : Type u_1} (S : Set M) [Mul M] :

Set M

The centralizer of a subset of a magma.

Equations

Set.centralizer S = {c | ∀ (m : M), m ∈ S → m * c = c * m}

Instances For

source

theorem Set.mem_addCentralizer {M : Type u_1} {S : Set M} [Add M] {c : M} :

c ∈ Set.addCentralizer S ↔ ∀ (m : M), m ∈ S → m + c = c + m

source

theorem Set.mem_centralizer_iff {M : Type u_1} {S : Set M} [Mul M] {c : M} :

c ∈ Set.centralizer S ↔ ∀ (m : M), m ∈ S → m * c = c * m

source

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

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)

source

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

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)

source

@[simp]

theorem Set.zero_mem_addCentralizer {M : Type u_1} (S : Set M) [AddZeroClass M] :

0 ∈ Set.addCentralizer S

source

@[simp]

theorem Set.one_mem_centralizer {M : Type u_1} (S : Set M) [MulOneClass M] :

1 ∈ Set.centralizer S

source

@[simp]

theorem Set.zero_mem_centralizer {M : Type u_1} (S : Set M) [MulZeroClass M] :

0 ∈ Set.centralizer S

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

theorem Set.addCentralizer_subset {M : Type u_1} {S : Set M} {T : Set M} [Add M] (h : S ⊆ T) :

Set.addCentralizer T ⊆ Set.addCentralizer S

source

theorem Set.centralizer_subset {M : Type u_1} {S : Set M} {T : Set M} [Mul M] (h : S ⊆ T) :

Set.centralizer T ⊆ Set.centralizer S

source

theorem Set.addCenter_subset_addCentralizer {M : Type u_1} [Add M] (S : Set M) :

Set.addCenter M ⊆ Set.addCentralizer S

source

theorem Set.center_subset_centralizer {M : Type u_1} [Mul M] (S : Set M) :

Set.center M ⊆ Set.centralizer S

source

@[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

source

@[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

source

@[simp]

theorem Set.addCentralizer_univ (M : Type u_1) [Add M] :

Set.addCentralizer Set.univ = Set.addCenter M

source

@[simp]

theorem Set.centralizer_univ (M : Type u_1) [Mul M] :

Set.centralizer Set.univ = Set.center M

source

@[simp]

theorem Set.addCentralizer_eq_univ {M : Type u_1} (S : Set M) [AddCommSemigroup M] :

Set.addCentralizer S = Set.univ

source

@[simp]

theorem Set.centralizer_eq_univ {M : Type u_1} (S : Set M) [CommSemigroup M] :

Set.centralizer S = Set.univ

source

def AddSubsemigroup.centralizer {M : Type u_1} (S : Set M) [AddSemigroup M] :

AddSubsemigroup M

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) }

Instances For

source

def Subsemigroup.centralizer {M : Type u_1} (S : Set M) [Semigroup M] :

Subsemigroup M

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) }

Instances For

source

@[simp]

theorem AddSubsemigroup.coe_centralizer {M : Type u_1} (S : Set M) [AddSemigroup M] :

↑(AddSubsemigroup.centralizer S) = Set.addCentralizer S

source

@[simp]

theorem Subsemigroup.coe_centralizer {M : Type u_1} (S : Set M) [Semigroup M] :

↑(Subsemigroup.centralizer S) = Set.centralizer S

source

theorem AddSubsemigroup.mem_centralizer_iff {M : Type u_1} {S : Set M} [AddSemigroup M] {z : M} :

z ∈ AddSubsemigroup.centralizer S ↔ ∀ (g : M), g ∈ S → g + z = z + g

source

theorem Subsemigroup.mem_centralizer_iff {M : Type u_1} {S : Set M} [Semigroup M] {z : M} :

z ∈ Subsemigroup.centralizer S ↔ ∀ (g : M), g ∈ S → g * z = z * g

source

instance AddSubsemigroup.decidableMemCentralizer {M : Type u_1} {S : Set M} [AddSemigroup M] (a : M) [Decidable (∀ (b : M), b ∈ S → b + a = a + b)] :

Decidable (a ∈ AddSubsemigroup.centralizer S)

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)

source

instance Subsemigroup.decidableMemCentralizer {M : Type u_1} {S : Set M} [Semigroup M] (a : M) [Decidable (∀ (b : M), b ∈ S → b * a = a * b)] :

Decidable (a ∈ Subsemigroup.centralizer S)

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)

source

theorem AddSubsemigroup.center_le_centralizer {M : Type u_1} [AddSemigroup M] (S : Set M) :

AddSubsemigroup.center M ≤ AddSubsemigroup.centralizer S

source

theorem Subsemigroup.center_le_centralizer {M : Type u_1} [Semigroup M] (S : Set M) :

Subsemigroup.center M ≤ Subsemigroup.centralizer S

source

theorem AddSubsemigroup.centralizer_le {M : Type u_1} {S : Set M} {T : Set M} [AddSemigroup M] (h : S ⊆ T) :

AddSubsemigroup.centralizer T ≤ AddSubsemigroup.centralizer S

source

theorem Subsemigroup.centralizer_le {M : Type u_1} {S : Set M} {T : Set M} [Semigroup M] (h : S ⊆ T) :

Subsemigroup.centralizer T ≤ Subsemigroup.centralizer S

source

@[simp]

theorem AddSubsemigroup.centralizer_eq_top_iff_subset {M : Type u_1} [AddSemigroup M] {s : Set M} :

AddSubsemigroup.centralizer s = ⊤ ↔ s ⊆ ↑(AddSubsemigroup.center M)

source

@[simp]

theorem Subsemigroup.centralizer_eq_top_iff_subset {M : Type u_1} [Semigroup M] {s : Set M} :

Subsemigroup.centralizer s = ⊤ ↔ s ⊆ ↑(Subsemigroup.center M)

source

@[simp]

theorem AddSubsemigroup.centralizer_univ (M : Type u_1) [AddSemigroup M] :

AddSubsemigroup.centralizer Set.univ = AddSubsemigroup.center M

source

@[simp]

theorem Subsemigroup.centralizer_univ (M : Type u_1) [Semigroup M] :

Subsemigroup.centralizer Set.univ = Subsemigroup.center M