Documentation

Mathlib.Algebra.Group.Center

Centers of magmas and semigroups #

Main definitions #

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

See also #

See Mathlib/GroupTheory/Subsemigroup/Center.lean for the definition of the center as a subsemigroup:

Subsemigroup.center: the center of a semigroup
AddSubsemigroup.center: the center of an additive semigroup

We provide Submonoid.center, AddSubmonoid.center, Subgroup.center, AddSubgroup.center, Subsemiring.center, and Subring.center in other files.

See Mathlib/GroupTheory/Subsemigroup/Centralizer.lean 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.

source

structure IsAddCentral {M : Type u_1} [Add M] (z : M) :

Prop

Conditions for an element to be additively central

comm (a : M) : AddCommute z a
addition commutes
left_assoc (b c : M) : z + (b + c) = z + b + c
associative property for left addition
right_assoc (a b : M) : a + b + z = a + (b + z)
associative property for right addition

Instances For

source

structure IsMulCentral {M : Type u_1} [Mul M] (z : M) :

Prop

Conditions for an element to be multiplicatively central

comm (a : M) : Commute z a
multiplication commutes
left_assoc (b c : M) : z * (b * c) = z * b * c
associative property for left multiplication
right_assoc (a b : M) : a * b * z = a * (b * z)
associative property for right multiplication

Instances For

source

theorem isMulCentral_iff {M : Type u_1} [Mul M] (z : M) :

IsMulCentral z ↔ (∀ (a : M), Commute z a) ∧ (∀ (b c : M), z * (b * c) = z * b * c) ∧ ∀ (a b : M), a * b * z = a * (b * z)

source

theorem isAddCentral_iff {M : Type u_1} [Add M] (z : M) :

IsAddCentral z ↔ (∀ (a : M), AddCommute z a) ∧ (∀ (b c : M), z + (b + c) = z + b + c) ∧ ∀ (a b : M), a + b + z = a + (b + z)

source

theorem IsMulCentral.mid_assoc {M : Type u_1} [Mul M] {z : M} (h : IsMulCentral z) (a c : M) :

a * z * c = a * (z * c)

source

theorem IsAddCentral.mid_assoc {M : Type u_1} [Add M] {z : M} (h : IsAddCentral z) (a c : M) :

a + z + c = a + (z + c)

source

theorem IsMulCentral.left_comm {M : Type u_1} {a : M} [Mul M] (h : IsMulCentral a) (b c : M) :

a * (b * c) = b * (a * c)

source

theorem IsAddCentral.left_comm {M : Type u_1} {a : M} [Add M] (h : IsAddCentral a) (b c : M) :

a + (b + c) = b + (a + c)

source

theorem IsMulCentral.right_comm {M : Type u_1} {c : M} [Mul M] (h : IsMulCentral c) (a b : M) :

a * b * c = a * c * b

source

theorem IsAddCentral.right_comm {M : Type u_1} {c : M} [Add M] (h : IsAddCentral c) (a b : M) :

a + b + c = a + c + b

Center #

source

def Set.center (M : Type u_1) [Mul M] :

Set M

The center of a magma.

Equations

Set.center M = {z : M | IsMulCentral z}

Instances For

source

def Set.addCenter (M : Type u_1) [Add M] :

Set M

The center of an additive magma.

Equations

Set.addCenter M = {z : M | IsAddCentral z}

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

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

Instances For

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

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

Instances For

source

theorem Set.mem_center_iff {M : Type u_1} [Mul M] {z : M} :

z ∈ center M ↔ IsMulCentral z

source

theorem Set.mem_addCenter_iff {M : Type u_1} [Add M] {z : M} :

z ∈ addCenter M ↔ IsAddCentral z

source

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

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

source

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

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

source

@[simp]

theorem Set.mul_mem_center {M : Type u_1} [Mul M] {z₁ z₂ : M} (hz₁ : z₁ ∈ center M) (hz₂ : z₂ ∈ center M) :

z₁ * z₂ ∈ center M

source

@[simp]

theorem Set.add_mem_addCenter {M : Type u_1} [Add M] {z₁ z₂ : M} (hz₁ : z₁ ∈ addCenter M) (hz₂ : z₂ ∈ addCenter M) :

z₁ + z₂ ∈ addCenter M

source

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

center M ⊆ S.centralizer

source

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

addCenter M ⊆ S.addCentralizer

source

theorem Set.centralizer_union {M : Type u_1} {S T : Set M} [Mul M] :

(S ∪ T).centralizer = S.centralizer ∩ T.centralizer

source

theorem Set.addCentralizer_union {M : Type u_1} {S T : Set M} [Add M] :

(S ∪ T).addCentralizer = S.addCentralizer ∩ T.addCentralizer

source

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

T.centralizer ⊆ S.centralizer

source

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

T.addCentralizer ⊆ S.addCentralizer

source

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

S ⊆ S.centralizer.centralizer

source

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

S ⊆ S.addCentralizer.addCentralizer

source

@[simp]

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

S.centralizer.centralizer.centralizer = S.centralizer

source

@[simp]

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

S.addCentralizer.addCentralizer.addCentralizer = S.addCentralizer

source

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 ∈ S.centralizer

Equations

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

source

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 ∈ S.addCentralizer

Equations

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

source

theorem Set.centralizer_centralizer_comm_of_comm {M : Type u_1} {S : Set M} [Mul M] (h_comm : ∀ x ∈ S, ∀ y ∈ S, x * y = y * x) (x : M) :

x ∈ S.centralizer.centralizer → ∀ y ∈ S.centralizer.centralizer, x * y = y * x

source

theorem Set.addCentralizer_addCentralizer_comm_of_comm {M : Type u_1} {S : Set M} [Add M] (h_comm : ∀ x ∈ S, ∀ y ∈ S, x + y = y + x) (x : M) :

x ∈ S.addCentralizer.addCentralizer → ∀ y ∈ S.addCentralizer.addCentralizer, x + y = y + x

source

theorem Set.centralizer_empty {M : Type u_1} [Mul M] :

∅.centralizer = ⊤

source

theorem Set.addCentralizer_empty {M : Type u_1} [Add M] :

∅.addCentralizer = ⊤

source

theorem Set.centralizer_prod {M : Type u_1} [Mul M] {N : Type u_2} [Mul N] {S : Set M} {T : Set N} (hS : S.Nonempty) (hT : T.Nonempty) :

(S ×ˢ T).centralizer = S.centralizer ×ˢ T.centralizer

The centralizer of the product of non-empty sets is equal to the product of the centralizers.

source

theorem Set.addCentralizer_prod {M : Type u_1} [Add M] {N : Type u_2} [Add N] {S : Set M} {T : Set N} (hS : S.Nonempty) (hT : T.Nonempty) :

(S ×ˢ T).addCentralizer = S.addCentralizer ×ˢ T.addCentralizer

source

theorem Set.prod_centralizer_subset_centralizer_prod {M : Type u_1} [Mul M] {N : Type u_2} [Mul N] (S : Set M) (T : Set N) :

S.centralizer ×ˢ T.centralizer ⊆ (S ×ˢ T).centralizer

source

theorem Set.prod_addCentralizer_subset_addCentralizer_prod {M : Type u_1} [Add M] {N : Type u_2} [Add N] (S : Set M) (T : Set N) :

S.addCentralizer ×ˢ T.addCentralizer ⊆ (S ×ˢ T).addCentralizer

source

theorem Set.center_prod {M : Type u_1} [Mul M] {N : Type u_2} [Mul N] :

center (M × N) = center M ×ˢ center N

source

theorem Set.addCenter_prod {M : Type u_1} [Add M] {N : Type u_2} [Add N] :

addCenter (M × N) = addCenter M ×ˢ addCenter N

source

theorem Set.center_pi {ι : Type u_2} {A : ι → Type u_3} [(i : ι) → Mul (A i)] :

center ((i : ι) → A i) = univ.pi fun (i : ι) => center (A i)

source

theorem Set.addCenter_pi {ι : Type u_2} {A : ι → Type u_3} [(i : ι) → Add (A i)] :

addCenter ((i : ι) → A i) = univ.pi fun (i : ι) => addCenter (A i)

source

theorem Semigroup.mem_center_iff {M : Type u_1} [Semigroup M] {z : M} :

z ∈ Set.center M ↔ ∀ (g : M), g * z = z * g

source

theorem AddSemigroup.mem_center_iff {M : Type u_1} [AddSemigroup M] {z : M} :

z ∈ Set.addCenter M ↔ ∀ (g : M), g + z = z + g

source

@[simp]

theorem Set.mul_mem_centralizer {M : Type u_1} {S : Set M} [Semigroup M] {a b : M} (ha : a ∈ S.centralizer) (hb : b ∈ S.centralizer) :

a * b ∈ S.centralizer

source

@[simp]

theorem Set.add_mem_addCentralizer {M : Type u_1} {S : Set M} [AddSemigroup M] {a b : M} (ha : a ∈ S.addCentralizer) (hb : b ∈ S.addCentralizer) :

a + b ∈ S.addCentralizer

source

@[simp]

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

S.centralizer = univ ↔ S ⊆ center M

source

@[simp]

theorem Set.addCentralizer_eq_top_iff_subset {M : Type u_1} {S : Set M} [AddSemigroup M] :

S.addCentralizer = univ ↔ S ⊆ addCenter M

source

@[simp]

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

univ.centralizer = center M

source

@[simp]

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

univ.addCentralizer = addCenter M

source

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

DecidablePred fun (x : M) => x ∈ center M

Equations

Set.decidableMemCenter x✝ = decidable_of_iff' (∀ (g : M), g * x✝ = x✝ * g) ⋯

source

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

DecidablePred fun (x : M) => x ∈ addCenter M

Equations

Set.decidableMemAddCenter x✝ = decidable_of_iff' (∀ (g : M), g + x✝ = x✝ + g) ⋯

source

@[simp]

theorem Set.center_eq_univ (M : Type u_1) [CommSemigroup M] :

center M = univ

source

@[simp]

theorem Set.addCenter_eq_univ (M : Type u_1) [AddCommSemigroup M] :

addCenter M = univ

source

@[simp]

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

S.centralizer = univ

source

@[simp]

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

S.addCentralizer = univ

source

@[simp]

theorem Set.one_mem_center {M : Type u_1} [MulOneClass M] :

1 ∈ center M

source

@[simp]

theorem Set.zero_mem_addCenter {M : Type u_1} [AddZeroClass M] :

0 ∈ addCenter M

source

@[simp]

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

1 ∈ S.centralizer

source

@[simp]

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

0 ∈ S.addCentralizer

source

theorem Set.subset_center_units {M : Type u_1} [Monoid M] :

Units.val ⁻¹' center M ⊆ center Mˣ

source

theorem Set.subset_addCenter_add_units {M : Type u_1} [AddMonoid M] :

AddUnits.val ⁻¹' addCenter M ⊆ addCenter (AddUnits M)

source

@[simp]

theorem Set.units_inv_mem_center {M : Type u_1} [Monoid M] {a : Mˣ} (ha : ↑a ∈ center M) :

↑a⁻¹ ∈ center M

source

@[simp]

theorem Set.addUnits_neg_mem_center {M : Type u_1} [AddMonoid M] {a : AddUnits M} (ha : ↑a ∈ addCenter M) :

↑(-a) ∈ addCenter M

source

@[simp]

theorem Set.invOf_mem_center {M : Type u_1} [Monoid M] {a : M} [Invertible a] (ha : a ∈ center M) :

⅟a ∈ center M

source

@[simp]

theorem Set.inv_mem_center {M : Type u_1} [DivisionMonoid M] {a : M} (ha : a ∈ center M) :

a⁻¹ ∈ center M

source

@[simp]

theorem Set.neg_mem_addCenter {M : Type u_1} [SubtractionMonoid M] {a : M} (ha : a ∈ addCenter M) :

-a ∈ addCenter M

source

@[simp]

theorem Set.div_mem_center {M : Type u_1} [DivisionMonoid M] {a b : M} (ha : a ∈ center M) (hb : b ∈ center M) :

a / b ∈ center M

source

@[simp]

theorem Set.sub_mem_addCenter {M : Type u_1} [SubtractionMonoid M] {a b : M} (ha : a ∈ addCenter M) (hb : b ∈ addCenter M) :

a - b ∈ addCenter M

source

@[simp]

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

a⁻¹ ∈ S.centralizer

source

@[simp]

theorem Set.neg_mem_addCentralizer {M : Type u_1} {S : Set M} [AddGroup M] {a : M} (ha : a ∈ S.addCentralizer) :

-a ∈ S.addCentralizer

source

@[simp]

theorem Set.div_mem_centralizer {M : Type u_1} {S : Set M} [Group M] {a b : M} (ha : a ∈ S.centralizer) (hb : b ∈ S.centralizer) :

a / b ∈ S.centralizer

source

@[simp]

theorem Set.sub_mem_addCentralizer {M : Type u_1} {S : Set M} [AddGroup M] {a b : M} (ha : a ∈ S.addCentralizer) (hb : b ∈ S.addCentralizer) :

a - b ∈ S.addCentralizer