Centers of magmas and semigroups #
Main definitions #
Set.center
: the center of a magmaSubsemigroup.center
: the center of a semigroupSet.addCenter
: the center of an additive magmaAddSubsemigroup.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.
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
@[simp]
@[simp]
theorem
Set.ofNat_mem_center
(M : Type u_1)
[NonAssocSemiring M]
(n : ℕ)
[Nat.AtLeastTwo n]
:
OfNat.ofNat n ∈ Set.center M
@[simp]
@[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
@[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
@[simp]
theorem
Set.neg_mem_addCenter
{M : Type u_1}
[AddGroup M]
{a : M}
(ha : a ∈ Set.addCenter M)
:
-a ∈ Set.addCenter M
@[simp]
theorem
Set.inv_mem_center
{M : Type u_1}
[Group M]
{a : M}
(ha : a ∈ Set.center M)
:
a⁻¹ ∈ Set.center M
@[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
@[simp]
theorem
Set.neg_mem_center
{M : Type u_1}
[NonUnitalNonAssocRing M]
{a : M}
(ha : a ∈ Set.center M)
:
-a ∈ Set.center M
theorem
Set.subset_addCenter_add_units
{M : Type u_1}
[AddMonoid M]
:
AddUnits.val ⁻¹' Set.addCenter M ⊆ Set.addCenter (AddUnits M)
theorem
Set.subset_center_units
{M : Type u_1}
[Monoid M]
:
Units.val ⁻¹' Set.center M ⊆ Set.center Mˣ
theorem
Set.center_units_subset
{M : Type u_1}
[GroupWithZero M]
:
Set.center Mˣ ⊆ Units.val ⁻¹' Set.center M
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.
@[simp]
theorem
Set.units_inv_mem_center
{M : Type u_1}
[Monoid M]
{a : Mˣ}
(ha : ↑a ∈ Set.center M)
:
↑a⁻¹ ∈ Set.center M
@[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
@[simp]
theorem
Set.inv_mem_center₀
{M : Type u_1}
[GroupWithZero M]
{a : M}
(ha : a ∈ Set.center M)
:
a⁻¹ ∈ Set.center M
@[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
@[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
@[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
@[simp]
The center of a semigroup M
is the set of elements that commute with everything in M
Instances For
The center of a semigroup M
is the set of elements that commute with everything in M
Instances For
instance
AddSubsemigroup.decidableMemCenter
{M : Type u_1}
[AddSemigroup M]
(a : M)
[Decidable (∀ (b : M), b + a = a + b)]
:
Decidable (a ∈ AddSubsemigroup.center M)
theorem
AddSubsemigroup.center.addCommSemigroup.proof_3
{M : Type u_1}
[AddSemigroup M]
:
∀ (x b : { x // x ∈ AddSubsemigroup.center M }), x + b = b + x
theorem
AddSubsemigroup.center.addCommSemigroup.proof_1
{M : Type u_1}
[AddSemigroup M]
:
AddMemClass (AddSubsemigroup M) M
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 })
:
instance
AddSubsemigroup.center.addCommSemigroup
{M : Type u_1}
[AddSemigroup M]
:
AddCommSemigroup { x // x ∈ AddSubsemigroup.center M }
The center of an additive semigroup is commutative.
instance
Subsemigroup.center.commSemigroup
{M : Type u_1}
[Semigroup M]
:
CommSemigroup { x // x ∈ Subsemigroup.center M }
The center of a semigroup is commutative.
@[simp]
@[simp]