Documentation

Mathlib.Algebra.Group.Centralizer

Centralizers of magmas and semigroups #

Main definitions #

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

See Mathlib.GroupTheory.Subsemigroup.Centralizer for the definition of the centralizer as a subsemigroup:

Subsemigroup.centralizer: the centralizer of a subset of a semigroup
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.

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

The centralizer of a subset of an additive magma.

Equations

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

Instances For

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

The centralizer of a subset of a magma.

Equations

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

Instances For

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

c ∈ Set.addCentralizer S ↔ ∀ m ∈ S, m + c = c + m

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

c ∈ Set.centralizer S ↔ ∀ m ∈ S, m * c = c * m

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

DecidablePred fun (x : M) => x ∈ Set.addCentralizer S

Equations

Set.decidableMemAddCentralizer x = decidable_of_iff' (∀ m ∈ S, m + x = x + m) ⋯

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

DecidablePred fun (x : M) => x ∈ Set.centralizer S

Equations

Set.decidableMemCentralizer x = decidable_of_iff' (∀ m ∈ S, m * x = x * m) ⋯

@[simp]

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

0 ∈ Set.addCentralizer S

@[simp]

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

1 ∈ Set.centralizer S

@[simp]

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

0 ∈ Set.centralizer S

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

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

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

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

Set.addCenter M ⊆ Set.addCentralizer S

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

Set.center M ⊆ Set.centralizer S

@[simp]

theorem Set.addCentralizer_eq_top_iff_subset {M : Type u_1} {s : Set M} [AddSemigroup 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} [Semigroup M] :

Set.centralizer s = Set.univ ↔ s ⊆ Set.center M

@[simp]

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

Set.addCentralizer Set.univ = Set.addCenter M

@[simp]

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

Set.centralizer Set.univ = Set.center M

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