Centers of monoids #
Main definitions #
Submonoid.center
: the center of a monoidAddSubmonoid.center
: the center of an additive monoid
We provide Subgroup.center
, AddSubgroup.center
, Subsemiring.center
, and Subring.center
in
other files.
The center of a monoid M
is the set of elements that commute with everything in M
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : 0 ∈ Set.addCenter M) = (_ : 0 ∈ Set.addCenter M)
def
AddSubmonoid.center.proof_1
(M : Type u_1)
[inst : AddMonoid 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)
theorem
AddSubmonoid.coe_center
(M : Type u_1)
[inst : AddMonoid M]
:
↑(AddSubmonoid.center M) = Set.addCenter M
@[simp]
theorem
AddSubmonoid.center_toAddSubsemigroup
(M : Type u_1)
[inst : AddMonoid M]
:
(AddSubmonoid.center M).toAddSubsemigroup = AddSubsemigroup.center M
@[simp]
theorem
Submonoid.center_toSubsemigroup
(M : Type u_1)
[inst : Monoid M]
:
(Submonoid.center M).toSubsemigroup = Subsemigroup.center M
instance
AddSubmonoid.decidableMemCenter
{M : Type u_1}
[inst : AddMonoid M]
(a : M)
[inst : Decidable (∀ (b : M), b + a = a + b)]
:
Decidable (a ∈ AddSubmonoid.center M)
Equations
- AddSubmonoid.decidableMemCenter a = decidable_of_iff' (∀ (g : M), g + a = a + g) (_ : a ∈ AddSubmonoid.center M ↔ ∀ (g : M), g + a = a + g)
instance
Submonoid.decidableMemCenter
{M : Type u_1}
[inst : Monoid M]
(a : M)
[inst : Decidable (∀ (b : M), b * a = a * b)]
:
Decidable (a ∈ Submonoid.center M)
Equations
- Submonoid.decidableMemCenter a = decidable_of_iff' (∀ (g : M), g * a = a * g) (_ : a ∈ Submonoid.center M ↔ ∀ (g : M), g * a = a * g)
instance
Submonoid.center.commMonoid
{M : Type u_1}
[inst : Monoid M]
:
CommMonoid { x // x ∈ Submonoid.center M }
The center of a monoid is commutative.
Equations
- Submonoid.center.commMonoid = let src := Submonoid.toMonoid (Submonoid.center M); CommMonoid.mk (_ : ∀ (x b : { x // x ∈ Submonoid.center M }), x * b = b * x)
instance
Submonoid.center.smulCommClass_left
{M : Type u_1}
[inst : Monoid M]
:
SMulCommClass { x // x ∈ Submonoid.center M } M M
The center of a monoid acts commutatively on that monoid.
instance
Submonoid.center.smulCommClass_right
{M : Type u_1}
[inst : Monoid M]
:
SMulCommClass M { x // x ∈ Submonoid.center M } M
The center of a monoid acts commutatively on that monoid.
Note that smulCommClass (center M) (center M) M
is already implied by
Submonoid.smulCommClass_right
@[simp]