Centers of magmas and semigroups #

Main definitions #

Set.center: the center of a magma
Subsemigroup.center: the center of a semigroup
Set.addCenter: the center of an additive magma
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.

source

ink

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

Set M

The center of an additive magma.

Equations

Set.addCenter M = { z | ∀ (m : M), m + z = z + m }

source

ink

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

Set M

The center of a magma.

Equations

Set.center M = { z | ∀ (m : M), m * z = z * m }

source

ink

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

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

source

ink

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

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

source

ink

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

DecidablePred fun x => x ∈ Set.center M

Equations

Set.decidableMemCenter M x = decidable_of_iff' (∀ (g : M), g * x = x * g) (_ : x ∈ Set.center M ↔ ∀ (g : M), g * x = x * g)

source

ink

@[simp]

theorem Set.zero_mem_addCenter (M : Type u_1) [inst : AddZeroClass M] :

0 ∈ Set.addCenter M

source

ink

@[simp]

theorem Set.one_mem_center (M : Type u_1) [inst : MulOneClass M] :

1 ∈ Set.center M

source

ink

@[simp]

theorem Set.zero_mem_center (M : Type u_1) [inst : MulZeroClass M] :

0 ∈ Set.center M

source

ink

@[simp]

theorem Set.add_mem_addCenter {M : Type u_1} [inst : AddSemigroup M] {a : M} {b : M} (ha : a ∈ Set.addCenter M) (hb : b ∈ Set.addCenter M) :

a + b ∈ Set.addCenter M

source

ink

@[simp]

theorem Set.mul_mem_center {M : Type u_1} [inst : Semigroup M] {a : M} {b : M} (ha : a ∈ Set.center M) (hb : b ∈ Set.center M) :

a * b ∈ Set.center M

source

ink

@[simp]

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

-a ∈ Set.addCenter M

source

ink

@[simp]

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

a⁻¹ ∈ Set.center M

source

ink

@[simp]

theorem Set.add_mem_center {M : Type u_1} [inst : Distrib M] {a : M} {b : M} (ha : a ∈ Set.center M) (hb : b ∈ Set.center M) :

a + b ∈ Set.center M

source

ink

@[simp]

theorem Set.neg_mem_center {M : Type u_1} [inst : Ring M] {a : M} (ha : a ∈ Set.center M) :

-a ∈ Set.center M

source

ink

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

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

source

ink

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

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

source

ink

theorem Set.center_units_subset {M : Type u_1} [inst : GroupWithZero M] :

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

source

ink

theorem Set.center_units_eq {M : Type u_1} [inst : GroupWithZero M] :

Set.center Mˣ = Units.val ⁻¹' Set.center M

In a group with zero, the center of the units is the preimage of the center.

source

ink

@[simp]

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

a⁻¹ ∈ Set.center M

source

ink

@[simp]

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

a - b ∈ Set.addCenter M

source

ink

@[simp]

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

a / b ∈ Set.center M

source

ink

@[simp]

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

a / b ∈ Set.center M

source

ink

@[simp]

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

Set.addCenter M = Set.univ

source

ink

@[simp]

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

Set.center M = Set.univ

source

ink

def AddSubsemigroup.center.proof_1 (M : Type u_1) [inst : AddSemigroup M] :

∀ {a b : M}, a ∈ Set.addCenter M → b ∈ Set.addCenter M → a + b ∈ Set.addCenter M

Equations

(_ : a ∈ Set.addCenter M → b ∈ Set.addCenter M → a + b ∈ Set.addCenter M) = (_ : a ∈ Set.addCenter M → b ∈ Set.addCenter M → a + b ∈ Set.addCenter M)

source

ink

def AddSubsemigroup.center (M : Type u_1) [inst : AddSemigroup M] :

AddSubsemigroup M

The center of a semigroup M is the set of elements that commute with everything in M

Equations

AddSubsemigroup.center M = { carrier := Set.addCenter M, add_mem' := (_ : ∀ {a b : M}, a ∈ Set.addCenter M → b ∈ Set.addCenter M → a + b ∈ Set.addCenter M) }

source

ink

def Subsemigroup.center (M : Type u_1) [inst : Semigroup M] :

Subsemigroup M

The center of a semigroup M is the set of elements that commute with everything in M

Equations

Subsemigroup.center M = { carrier := Set.center M, mul_mem' := (_ : ∀ {a b : M}, a ∈ Set.center M → b ∈ Set.center M → a * b ∈ Set.center M) }

source

ink

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

z ∈ AddSubsemigroup.center M ↔ ∀ (g : M), g + z = z + g

source

ink

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

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

source

ink

instance AddSubsemigroup.decidableMemCenter {M : Type u_1} [inst : AddSemigroup M] (a : M) [inst : Decidable (∀ (b : M), b + a = a + b)] :

Decidable (a ∈ AddSubsemigroup.center M)

Equations

AddSubsemigroup.decidableMemCenter a = decidable_of_iff' (∀ (g : M), g + a = a + g) (_ : a ∈ AddSubsemigroup.center M ↔ ∀ (g : M), g + a = a + g)

source

ink

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

Decidable (a ∈ Subsemigroup.center M)

Equations

Subsemigroup.decidableMemCenter a = decidable_of_iff' (∀ (g : M), g * a = a * g) (_ : a ∈ Subsemigroup.center M ↔ ∀ (g : M), g * a = a * g)

source

ink

def AddSubsemigroup.instAddCommSemigroupSubtypeMemSubsemigroupToAddInstMembershipInstSetLikeSubsemigroupCenter.proof_2 {M : Type u_1} [inst : AddSemigroup M] (a : { x // x ∈ AddSubsemigroup.center M }) (b : { x // x ∈ AddSubsemigroup.center M }) (c : { x // x ∈ AddSubsemigroup.center M }) :

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

Equations

(_ : ∀ (a b c : { x // x ∈ AddSubsemigroup.center M }), a + b + c = a + (b + c)) = (_ : ∀ (a b c : { x // x ∈ AddSubsemigroup.center M }), a + b + c = a + (b + c))