Documentation

Mathlib.GroupTheory.Submonoid.Centralizer

Centralizers of magmas and monoids #

Main definitions #

Submonoid.centralizer: the centralizer of a subset of a monoid
AddSubmonoid.centralizer: the centralizer of a subset of an additive monoid

We provide Subgroup.centralizer, AddSubgroup.centralizer in other files.

def AddSubmonoid.centralizer.proof_2 {M : Type u_1} (S : Set M) [inst : AddMonoid M] :

0 ∈ Set.addCentralizer S

Equations

(_ : 0 ∈ Set.addCentralizer S) = (_ : 0 ∈ Set.addCentralizer S)

def AddSubmonoid.centralizer {M : Type u_1} (S : Set M) [inst : AddMonoid M] :

The centralizer of a subset of an additive monoid.

Equations

One or more equations did not get rendered due to their size.

def AddSubmonoid.centralizer.proof_1 {M : Type u_1} (S : Set M) [inst : AddMonoid 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)

def Submonoid.centralizer {M : Type u_1} (S : Set M) [inst : Monoid M] :

The centralizer of a subset of a monoid M.

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem AddSubmonoid.coe_centralizer {M : Type u_1} (S : Set M) [inst : AddMonoid M] :

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

@[simp]

theorem Submonoid.coe_centralizer {M : Type u_1} (S : Set M) [inst : Monoid M] :

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

theorem Submonoid.centralizer_toSubsemigroup {M : Type u_1} (S : Set M) [inst : Monoid M] :

(Submonoid.centralizer S).toSubsemigroup = Subsemigroup.centralizer S

theorem AddSubmonoid.centralizer_toAddSubsemigroup {M : Type u_1} [inst : AddMonoid M] (S : Set M) :

(AddSubmonoid.centralizer S).toAddSubsemigroup = AddSubsemigroup.centralizer S

theorem AddSubmonoid.mem_centralizer_iff {M : Type u_1} {S : Set M} [inst : AddMonoid M] {z : M} :

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

theorem Submonoid.mem_centralizer_iff {M : Type u_1} {S : Set M} [inst : Monoid M] {z : M} :

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

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

Decidable (a ∈ AddSubmonoid.centralizer S)

Equations

AddSubmonoid.decidableMemCentralizer a = decidable_of_iff' (∀ (g : M), g ∈ S → g + a = a + g) (_ : a ∈ AddSubmonoid.centralizer S ↔ ∀ (g : M), g ∈ S → g + a = a + g)

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

Decidable (a ∈ Submonoid.centralizer S)

Equations

Submonoid.decidableMemCentralizer a = decidable_of_iff' (∀ (g : M), g ∈ S → g * a = a * g) (_ : a ∈ Submonoid.centralizer S ↔ ∀ (g : M), g ∈ S → g * a = a * g)

theorem AddSubmonoid.centralizer_le {M : Type u_1} {S : Set M} {T : Set M} [inst : AddMonoid M] (h : S ⊆ T) :

AddSubmonoid.centralizer T ≤ AddSubmonoid.centralizer S

theorem Submonoid.centralizer_le {M : Type u_1} {S : Set M} {T : Set M} [inst : Monoid M] (h : S ⊆ T) :

Submonoid.centralizer T ≤ Submonoid.centralizer S

@[simp]

theorem AddSubmonoid.centralizer_univ (M : Type u_1) [inst : AddMonoid M] :

AddSubmonoid.centralizer Set.univ = AddSubmonoid.center M

@[simp]

theorem Submonoid.centralizer_univ (M : Type u_1) [inst : Monoid M] :

Submonoid.centralizer Set.univ = Submonoid.center M