Documentation

Mathlib.GroupTheory.Submonoid.Centralizer

Centralizers of magmas and monoids #

Main definitions #

We provide Subgroup.centralizer, AddSubgroup.centralizer in other files.

source
def Submonoid.centralizer {M : Type u_1} (S : Set M) [Monoid M] :
Submonoid M

The centralizer of a subset of a monoid M.

Instances For
    source
    def AddSubmonoid.centralizer {M : Type u_1} (S : Set M) [AddMonoid M] :
    AddSubmonoid M

    The centralizer of a subset of an additive monoid.

    Instances For
      source
      @[simp]
      theorem Submonoid.coe_centralizer {M : Type u_1} (S : Set M) [Monoid M] :
      ↑(centralizer S) = S.centralizer
      source
      @[simp]
      theorem AddSubmonoid.coe_centralizer {M : Type u_1} (S : Set M) [AddMonoid M] :
      ↑(centralizer S) = S.addCentralizer
      source
      theorem Submonoid.centralizer_toSubsemigroup {M : Type u_1} (S : Set M) [Monoid M] :
      (centralizer S).toSubsemigroup = Subsemigroup.centralizer S
      source
      theorem AddSubmonoid.centralizer_toAddSubsemigroup {M : Type u_1} (S : Set M) [AddMonoid M] :
      (centralizer S).toAddSubsemigroup = AddSubsemigroup.centralizer S
      source
      theorem Submonoid.mem_centralizer_iff {M : Type u_1} {S : Set M} [Monoid M] {z : M} :
      z ∈ centralizer S ↔ ∀ g ∈ S, g * z = z * g
      source
      theorem AddSubmonoid.mem_centralizer_iff {M : Type u_1} {S : Set M} [AddMonoid M] {z : M} :
      z ∈ centralizer S ↔ ∀ g ∈ S, g + z = z + g
      source
      theorem Submonoid.center_le_centralizer {M : Type u_1} [Monoid M] (s : Set M) :
      center M ≤ centralizer s
      source
      theorem AddSubmonoid.center_le_centralizer {M : Type u_1} [AddMonoid M] (s : Set M) :
      center M ≤ centralizer s
      source
      @[implicit_reducible]
      instance Submonoid.decidableMemCentralizer {M : Type u_1} {S : Set M} [Monoid M] (a : M) [Decidable (∀ b ∈ S, b * a = a * b)] :
      Decidable (a ∈ centralizer S)
      source
      @[implicit_reducible]
      instance AddSubmonoid.decidableMemCentralizer {M : Type u_1} {S : Set M} [AddMonoid M] (a : M) [Decidable (∀ b ∈ S, b + a = a + b)] :
      Decidable (a ∈ centralizer S)
      source
      theorem Submonoid.centralizer_le {M : Type u_1} {S T : Set M} [Monoid M] (h : S ⊆ T) :
      centralizer T ≤ centralizer S
      source
      theorem AddSubmonoid.centralizer_le {M : Type u_1} {S T : Set M} [AddMonoid M] (h : S ⊆ T) :
      centralizer T ≤ centralizer S
      source
      @[simp]
      theorem Submonoid.centralizer_eq_top_iff_subset {M : Type u_1} [Monoid M] {s : Set M} :
      centralizer s = ⊤ ↔ s ⊆ ↑(center M)
      source
      @[simp]
      theorem AddSubmonoid.centralizer_eq_top_iff_subset {M : Type u_1} [AddMonoid M] {s : Set M} :
      centralizer s = ⊤ ↔ s ⊆ ↑(center M)
      source
      @[simp]
      theorem Submonoid.centralizer_univ (M : Type u_1) [Monoid M] :
      centralizer Set.univ = center M
      source
      @[simp]
      theorem AddSubmonoid.centralizer_univ (M : Type u_1) [AddMonoid M] :
      centralizer Set.univ = center M
      source
      theorem Submonoid.le_centralizer_centralizer (M : Type u_1) [Monoid M] {s : Submonoid M} :
      s ≤ centralizer ↑(centralizer ↑s)
      source
      theorem AddSubmonoid.le_centralizer_centralizer (M : Type u_1) [AddMonoid M] {s : AddSubmonoid M} :
      s ≤ centralizer ↑(centralizer ↑s)
      source
      @[simp]
      theorem Submonoid.centralizer_centralizer_centralizer (M : Type u_1) [Monoid M] {s : Set M} :
      centralizer s.centralizer.centralizer = centralizer s
      source
      @[simp]
      theorem AddSubmonoid.centralizer_centralizer_centralizer (M : Type u_1) [AddMonoid M] {s : Set M} :
      centralizer s.addCentralizer.addCentralizer = centralizer s
      source
      theorem Submonoid.closure_le_centralizer_centralizer {M : Type u_1} [Monoid M] (s : Set M) :
      closure s ≤ centralizer ↑(centralizer s)
      source
      theorem AddSubmonoid.closure_le_centralizer_centralizer {M : Type u_1} [AddMonoid M] (s : Set M) :
      closure s ≤ centralizer ↑(centralizer s)
      source
      theorem Submonoid.isMulCommutative_closure (M : Type u_1) [Monoid M] {s : Set M} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) :
      IsMulCommutative ↥(closure s)

      If all the elements of a set s commute, then closure s is a commutative monoid.

      source
      theorem AddSubmonoid.isAddCommutative_closure (M : Type u_1) [AddMonoid M] {s : Set M} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a + b = b + a) :
      IsAddCommutative ↥(closure s)

      If all the elements of a set s commute, then closure s forms an additive commutative monoid.

      source
      @[reducible, inline, deprecated Submonoid.isMulCommutative_closure (since := "2026-03-09")]
      abbrev Submonoid.closureCommMonoidOfComm (M : Type u_1) [Monoid M] {s : Set M} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) :
      CommMonoid ↥(closure s)

      If all the elements of a set s commute, then closure s is a commutative monoid.

      Instances For
        source
        @[reducible, inline, deprecated Submonoid.isMulCommutative_closure (since := "2026-03-09")]
        abbrev AddSubmonoid.closureAddCommMonoidOfComm (M : Type u_1) [AddMonoid M] {s : Set M} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a + b = b + a) :
        AddCommMonoid ↥(closure s)

        If all the elements of a set s commute, then closure s forms an additive commutative monoid.

        Instances For
          source
          instance Submonoid.instIsMulCommutative_closure (M : Type u_1) [Monoid M] {S : Type u_2} [SetLike S M] [MulMemClass S M] (s : S) [IsMulCommutative ↥s] :
          IsMulCommutative ↥(closure ↑s)
          source
          instance AddSubmonoid.instIsAddCommutative_closure (M : Type u_1) [AddMonoid M] {S : Type u_2} [SetLike S M] [AddMemClass S M] (s : S) [IsAddCommutative ↥s] :
          IsAddCommutative ↥(closure ↑s)