Centralizers of magmas and monoids #
Main definitions #
Submonoid.centralizer
: the centralizer of a subset of a monoidAddSubmonoid.centralizer
: the centralizer of a subset of an additive monoid
We provide Subgroup.centralizer
, AddSubgroup.centralizer
in other files.
def
AddSubmonoid.centralizer.proof_2
{M : Type u_1}
(S : Set M)
[inst : AddMonoid M]
:
0 ∈ Set.addCentralizer S
Equations
- (_ : 0 ∈ Set.addCentralizer S) = (_ : 0 ∈ Set.addCentralizer S)
The centralizer of a subset of an additive monoid.
Equations
- One or more equations did not get rendered due to their size.
def
AddSubmonoid.centralizer.proof_1
{M : Type u_1}
(S : Set M)
[inst : AddMonoid M]
:
∀ {a b : M}, a ∈ Set.addCentralizer S → b ∈ Set.addCentralizer S → a + b ∈ Set.addCentralizer S
Equations
- (_ : a ∈ Set.addCentralizer S → b ∈ Set.addCentralizer S → a + b ∈ Set.addCentralizer S) = (_ : a ∈ Set.addCentralizer S → b ∈ Set.addCentralizer S → a + b ∈ Set.addCentralizer S)
@[simp]
@[simp]
theorem
Submonoid.centralizer_toSubsemigroup
{M : Type u_1}
(S : Set M)
[inst : Monoid M]
:
(Submonoid.centralizer S).toSubsemigroup = Subsemigroup.centralizer S
theorem
AddSubmonoid.centralizer_toAddSubsemigroup
{M : Type u_1}
[inst : AddMonoid M]
(S : Set M)
:
(AddSubmonoid.centralizer S).toAddSubsemigroup = AddSubsemigroup.centralizer S
instance
AddSubmonoid.decidableMemCentralizer
{M : Type u_1}
{S : Set M}
[inst : AddMonoid M]
(a : M)
[inst : Decidable (∀ (b : M), b ∈ S → b + a = a + b)]
:
Equations
- AddSubmonoid.decidableMemCentralizer a = decidable_of_iff' (∀ (g : M), g ∈ S → g + a = a + g) (_ : a ∈ AddSubmonoid.centralizer S ↔ ∀ (g : M), g ∈ S → g + a = a + g)
instance
Submonoid.decidableMemCentralizer
{M : Type u_1}
{S : Set M}
[inst : Monoid M]
(a : M)
[inst : Decidable (∀ (b : M), b ∈ S → b * a = a * b)]
:
Decidable (a ∈ Submonoid.centralizer S)
Equations
- Submonoid.decidableMemCentralizer a = decidable_of_iff' (∀ (g : M), g ∈ S → g * a = a * g) (_ : a ∈ Submonoid.centralizer S ↔ ∀ (g : M), g ∈ S → g * a = a * g)
@[simp]
theorem
AddSubmonoid.centralizer_univ
(M : Type u_1)
[inst : AddMonoid M]
:
AddSubmonoid.centralizer Set.univ = AddSubmonoid.center M
@[simp]
theorem
Submonoid.centralizer_univ
(M : Type u_1)
[inst : Monoid M]
:
Submonoid.centralizer Set.univ = Submonoid.center M