Centralizers of magmas and monoids #

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

Main definitions #

submonoid.centralizer: the centralizer of a subset of a monoid
add_submonoid.centralizer: the centralizer of a subset of an additive monoid

We provide subgroup.centralizer, add_subgroup.centralizer in other files.

source

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

submonoid M

The centralizer of a subset of a monoid M.

Equations

submonoid.centralizer S = {carrier := S.centralizer (mul_one_class.to_has_mul M), mul_mem' := _, one_mem' := _}

source

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

add_submonoid M

The centralizer of a subset of an additive monoid.

Equations

add_submonoid.centralizer S = {carrier := S.add_centralizer (add_zero_class.to_has_add M), add_mem' := _, zero_mem' := _}

source

@[simp, norm_cast]

theorem add_submonoid.coe_centralizer {M : Type u_1} (S : set M) [add_monoid M] :

↑(add_submonoid.centralizer S) = S.add_centralizer

source

@[simp, norm_cast]

theorem submonoid.coe_centralizer {M : Type u_1} (S : set M) [monoid M] :

↑(submonoid.centralizer S) = S.centralizer

source

theorem submonoid.centralizer_to_subsemigroup {M : Type u_1} (S : set M) [monoid M] :

(submonoid.centralizer S).to_subsemigroup = subsemigroup.centralizer S

source

theorem add_submonoid.centralizer_to_add_subsemigroup {M : Type u_1} [add_monoid M] (S : set M) :

(add_submonoid.centralizer S).to_add_subsemigroup = add_subsemigroup.centralizer S

source

theorem submonoid.mem_centralizer_iff {M : Type u_1} {S : set M} [monoid M] {z : M} :

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

source

theorem add_submonoid.mem_centralizer_iff {M : Type u_1} {S : set M} [add_monoid M] {z : M} :

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

source

theorem submonoid.center_le_centralizer {M : Type u_1} [monoid M] (s : set M) :

submonoid.center M ≤ submonoid.centralizer s

source

theorem add_submonoid.center_le_centralizer {M : Type u_1} [add_monoid M] (s : set M) :

add_submonoid.center M ≤ add_submonoid.centralizer s

source

@[protected, instance]

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

decidable (a ∈ submonoid.centralizer S)

Equations

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

source

@[protected, instance]

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

decidable (a ∈ add_submonoid.centralizer S)

Equations

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

source

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

add_submonoid.centralizer T ≤ add_submonoid.centralizer S

source

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

submonoid.centralizer T ≤ submonoid.centralizer S

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

theorem submonoid.centralizer_univ (M : Type u_1) [monoid M] :

submonoid.centralizer set.univ = submonoid.center M

source

@[simp]

theorem add_submonoid.centralizer_univ (M : Type u_1) [add_monoid M] :

add_submonoid.centralizer set.univ = add_submonoid.center M