Centers of semigroups, as subsemigroups. #
Main definitions #
Subsemigroup.center
: the center of a semigroupAddSubsemigroup.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.
References #
- [Cabrera García and Rodríguez Palacios, Non-associative normed algebras. Volume 1] [CGRP14]
Set.center
as a Subsemigroup
. #
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' := ⋯ }
Instances For
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' := ⋯ }
Instances For
theorem
AddSubsemigroup.center.addCommSemigroup.proof_2
{M : Type u_1}
[Add M]
(a : ↥(AddSubsemigroup.center M))
:
∀ (x : ↥(AddSubsemigroup.center M)), a + x = x + a
The center of an additive magma is commutative and associative.
Equations
- AddSubsemigroup.center.addCommSemigroup = AddCommSemigroup.mk ⋯
The center of a magma is commutative and associative.
Equations
- Subsemigroup.center.commSemigroup = CommSemigroup.mk ⋯
instance
AddSubsemigroup.decidableMemCenter
{M : Type u_1}
[AddSemigroup M]
(a : M)
[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) ⋯
instance
Subsemigroup.decidableMemCenter
{M : Type u_1}
[Semigroup M]
(a : M)
[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) ⋯
@[simp]
@[simp]