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)
[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)
@[simp]
@[simp]
@[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
@[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
@[simp]
theorem
Set.neg_mem_addCenter
{M : Type u_1}
[inst : AddGroup M]
{a : M}
(ha : a ∈ Set.addCenter M)
:
-a ∈ Set.addCenter M
@[simp]
theorem
Set.inv_mem_center
{M : Type u_1}
[inst : Group M]
{a : M}
(ha : a ∈ Set.center M)
:
a⁻¹ ∈ Set.center M
@[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
@[simp]
theorem
Set.neg_mem_center
{M : Type u_1}
[inst : Ring M]
{a : M}
(ha : a ∈ Set.center M)
:
-a ∈ Set.center M
theorem
Set.subset_addCenter_add_units
{M : Type u_1}
[inst : AddMonoid M]
:
AddUnits.val ⁻¹' Set.addCenter M ⊆ Set.addCenter (AddUnits M)
theorem
Set.subset_center_units
{M : Type u_1}
[inst : Monoid M]
:
Units.val ⁻¹' Set.center M ⊆ Set.center Mˣ
theorem
Set.center_units_subset
{M : Type u_1}
[inst : GroupWithZero M]
:
Set.center Mˣ ⊆ Units.val ⁻¹' Set.center M
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.
@[simp]
theorem
Set.inv_mem_center₀
{M : Type u_1}
[inst : GroupWithZero M]
{a : M}
(ha : a ∈ Set.center M)
:
a⁻¹ ∈ Set.center M
@[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
@[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
@[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
@[simp]
theorem
Set.addCenter_eq_univ
(M : Type u_1)
[inst : AddCommSemigroup M]
:
Set.addCenter M = Set.univ
@[simp]
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)
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) }
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) }
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)
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)
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 })
:
def
AddSubsemigroup.instAddCommSemigroupSubtypeMemSubsemigroupToAddInstMembershipInstSetLikeSubsemigroupCenter.proof_1
{M : Type u_1}
[inst : AddSemigroup M]
:
AddMemClass (AddSubsemigroup M) M
Equations
- (_ : AddMemClass (AddSubsemigroup M) M) = (_ : AddMemClass (AddSubsemigroup M) M)
instance
AddSubsemigroup.instAddCommSemigroupSubtypeMemSubsemigroupToAddInstMembershipInstSetLikeSubsemigroupCenter
{M : Type u_1}
[inst : AddSemigroup M]
:
AddCommSemigroup { x // x ∈ AddSubsemigroup.center M }
The center of an additive semigroup is commutative.
Equations
- One or more equations did not get rendered due to their size.
instance
Subsemigroup.instCommSemigroupSubtypeMemSubsemigroupToMulInstMembershipInstSetLikeSubsemigroupCenter
{M : Type u_1}
[inst : Semigroup M]
:
CommSemigroup { x // x ∈ Subsemigroup.center M }
The center of a semigroup is commutative.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
@[simp]