Centralizers of magmas and semigroups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main definitions #

set.centralizer: the centralizer of a subset of a magma
subsemigroup.centralizer: the centralizer of a subset of a semigroup
set.add_centralizer: the centralizer of a subset of an additive magma
add_subsemigroup.centralizer: the centralizer of a subset of an additive semigroup

We provide monoid.centralizer, add_monoid.centralizer, subgroup.centralizer, and add_subgroup.centralizer in other files.

source

def set.centralizer {M : Type u_1} (S : set M) [has_mul M] :

set M

The centralizer of a subset of a magma.

Equations

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

source

def set.add_centralizer {M : Type u_1} (S : set M) [has_add M] :

set M

The centralizer of a subset of an additive magma.

Equations

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

source

theorem set.mem_add_centralizer {M : Type u_1} {S : set M} [has_add M] {c : M} :

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

source

theorem set.mem_centralizer_iff {M : Type u_1} {S : set M} [has_mul M] {c : M} :

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

source

@[protected, instance]

def set.decidable_mem_add_centralizer {M : Type u_1} {S : set M} [has_add M] [Π (a : M), decidable (∀ (b : M), b ∈ S → b + a = a + b)] :

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

source

@[protected, instance]

def set.decidable_mem_centralizer {M : Type u_1} {S : set M} [has_mul M] [Π (a : M), decidable (∀ (b : M), b ∈ S → b * a = a * b)] :

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

source

@[simp]

theorem set.zero_mem_add_centralizer {M : Type u_1} (S : set M) [add_zero_class M] :

0 ∈ S.add_centralizer

source

@[simp]

theorem set.one_mem_centralizer {M : Type u_1} (S : set M) [mul_one_class M] :

1 ∈ S.centralizer

source

@[simp]

theorem set.zero_mem_centralizer {M : Type u_1} (S : set M) [mul_zero_class M] :

0 ∈ S.centralizer

source

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

source

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

source

@[simp]

theorem set.inv_mem_centralizer {M : Type u_1} {S : set M} {a : M} [group M] (ha : a ∈ S.centralizer) :

a⁻¹ ∈ S.centralizer

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

T.centralizer ⊆ S.centralizer

source

theorem set.add_centralizer_subset {M : Type u_1} {S T : set M} [has_add M] (h : S ⊆ T) :

T.add_centralizer ⊆ S.add_centralizer

source

theorem set.add_center_subset_add_centralizer {M : Type u_1} [has_add M] (S : set M) :

set.add_center M ⊆ S.add_centralizer

source

theorem set.center_subset_centralizer {M : Type u_1} [has_mul M] (S : set M) :

set.center M ⊆ S.centralizer

source

@[simp]

theorem set.add_centralizer_eq_top_iff_subset {M : Type u_1} {s : set M} [has_add M] :

s.add_centralizer = set.univ ↔ s ⊆ set.add_center M

source

@[simp]

theorem set.centralizer_eq_top_iff_subset {M : Type u_1} {s : set M} [has_mul M] :

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

source

@[simp]

theorem set.add_centralizer_univ (M : Type u_1) [has_add M] :

set.univ.add_centralizer = set.add_center M

source

@[simp]

theorem set.centralizer_univ (M : Type u_1) [has_mul M] :

set.univ.centralizer = set.center M

source

@[simp]

theorem set.add_centralizer_eq_univ {M : Type u_1} (S : set M) [add_comm_semigroup M] :

S.add_centralizer = set.univ

source

@[simp]

theorem set.centralizer_eq_univ {M : Type u_1} (S : set M) [comm_semigroup M] :

S.centralizer = set.univ

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 := S.centralizer (semigroup.to_has_mul M), mul_mem' := _}

source

def add_subsemigroup.centralizer {M : Type u_1} (S : set M) [add_semigroup M] :

add_subsemigroup M

The centralizer of a subset of an additive semigroup.

Equations

add_subsemigroup.centralizer S = {carrier := S.add_centralizer (add_semigroup.to_has_add M), add_mem' := _}

source

@[simp, norm_cast]

theorem subsemigroup.coe_centralizer {M : Type u_1} (S : set M) [semigroup M] :

↑(subsemigroup.centralizer S) = S.centralizer

source

@[simp, norm_cast]

theorem add_subsemigroup.coe_centralizer {M : Type u_1} (S : set M) [add_semigroup M] :

↑(add_subsemigroup.centralizer S) = S.add_centralizer

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

theorem add_subsemigroup.mem_centralizer_iff {M : Type u_1} {S : set M} [add_semigroup M] {z : M} :

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

source

@[protected, instance]

def subsemigroup.decidable_mem_centralizer {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.decidable_mem_centralizer a = decidable_of_iff' (∀ (g : M), g ∈ S → g * a = a * g) subsemigroup.mem_centralizer_iff

source

@[protected, instance]

def add_subsemigroup.decidable_mem_centralizer {M : Type u_1} {S : set M} [add_semigroup M] (a : M) [decidable (∀ (b : M), b ∈ S → b + a = a + b)] :

decidable (a ∈ add_subsemigroup.centralizer S)

Equations

add_subsemigroup.decidable_mem_centralizer a = decidable_of_iff' (∀ (g : M), g ∈ S → g + a = a + g) add_subsemigroup.mem_centralizer_iff

source

theorem add_subsemigroup.center_le_centralizer {M : Type u_1} [add_semigroup M] (S : set M) :

add_subsemigroup.center M ≤ add_subsemigroup.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 subsemigroup.centralizer_le {M : Type u_1} {S T : set M} [semigroup M] (h : S ⊆ T) :

subsemigroup.centralizer T ≤ subsemigroup.centralizer S

source

theorem add_subsemigroup.centralizer_le {M : Type u_1} {S T : set M} [add_semigroup M] (h : S ⊆ T) :

add_subsemigroup.centralizer T ≤ add_subsemigroup.centralizer S

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 add_subsemigroup.centralizer_eq_top_iff_subset {M : Type u_1} [add_semigroup M] {s : set M} :

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

source

@[simp]

theorem add_subsemigroup.centralizer_univ (M : Type u_1) [add_semigroup M] :

add_subsemigroup.centralizer set.univ = add_subsemigroup.center M

source

@[simp]

theorem subsemigroup.centralizer_univ (M : Type u_1) [semigroup M] :

subsemigroup.centralizer set.univ = subsemigroup.center M