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

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

Set M

The center of an additive magma.

Instances For

source

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

Set M

The center of a magma.

Instances For

source

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

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

source

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

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

source

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

DecidablePred fun x => x ∈ Set.center M

source

@[simp]

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

0 ∈ Set.addCenter M

source

@[simp]

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

1 ∈ Set.center M

source

@[simp]

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

0 ∈ Set.center M

source

@[simp]

theorem Set.natCast_mem_center (M : Type u_1) [NonAssocSemiring M] (n : ℕ) :

↑n ∈ Set.center M

source

@[simp]

theorem Set.ofNat_mem_center (M : Type u_1) [NonAssocSemiring M] (n : ℕ) [Nat.AtLeastTwo n] :

OfNat.ofNat n ∈ Set.center M

source

@[simp]

theorem Set.intCast_mem_center (M : Type u_1) [NonAssocRing M] (n : ℤ) :

↑n ∈ Set.center M

source

@[simp]

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

a + b ∈ Set.addCenter M

source

@[simp]

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

a * b ∈ Set.center M

source

@[simp]

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

-a ∈ Set.addCenter M

source

@[simp]

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

a⁻¹ ∈ Set.center M

source

@[simp]

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

a + b ∈ Set.center M

source

@[simp]

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

-a ∈ Set.center M

source

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

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

source

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

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

source

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

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

source

theorem Set.center_units_eq {M : Type u_1} [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

@[simp]

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

↑a⁻¹ ∈ Set.center M

source

@[simp]

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

⅟a ∈ Set.center M

source

@[simp]

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

a⁻¹ ∈ Set.center M

source

@[simp]

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

a - b ∈ Set.addCenter M

source

@[simp]

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

a / b ∈ Set.center M

source

@[simp]

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

a / b ∈ Set.center M

source

@[simp]

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

Set.addCenter M = Set.univ

source

@[simp]

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

Set.center M = Set.univ

source

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

AddSubsemigroup M

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

Instances For

source

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

Subsemigroup M

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

Instances For

source

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

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

source

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

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

source

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

Decidable (a ∈ AddSubsemigroup.center M)

source

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

Decidable (a ∈ Subsemigroup.center M)

source

theorem AddSubsemigroup.center.addCommSemigroup.proof_3 {M : Type u_1} [AddSemigroup M] :

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

source

theorem AddSubsemigroup.center.addCommSemigroup.proof_1 {M : Type u_1} [AddSemigroup M] :

AddMemClass (AddSubsemigroup M) M

source

theorem AddSubsemigroup.center.addCommSemigroup.proof_2 {M : Type u_1} [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)

source

instance AddSubsemigroup.center.addCommSemigroup {M : Type u_1} [AddSemigroup M] :

AddCommSemigroup { x // x ∈ AddSubsemigroup.center M }

The center of an additive semigroup is commutative.

source

instance Subsemigroup.center.commSemigroup {M : Type u_1} [Semigroup M] :

CommSemigroup { x // x ∈ Subsemigroup.center M }

The center of a semigroup is commutative.

source

@[simp]

theorem AddSubsemigroup.center_eq_top (M : Type u_1) [AddCommSemigroup M] :

AddSubsemigroup.center M = ⊤

source

@[simp]

theorem Subsemigroup.center_eq_top (M : Type u_1) [CommSemigroup M] :

Subsemigroup.center M = ⊤