Documentation

Mathlib.GroupTheory.Subsemigroup.Centralizer

Centralizers in semigroups, as subsemigroups. #

Main definitions #

We provide Monoid.centralizer, AddMonoid.centralizer, Subgroup.centralizer, and AddSubgroup.centralizer in other files.

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

The centralizer of a subset of a semigroup M.

Equations
    Instances For
      source
      def AddSubsemigroup.centralizer {M : Type u_1} (S : Set M) [AddSemigroup M] :
      AddSubsemigroup M

      The centralizer of a subset of an additive semigroup.

      Equations
        Instances For
          source
          @[simp]
          theorem Subsemigroup.coe_centralizer {M : Type u_1} (S : Set M) [Semigroup M] :
          ↑(centralizer S) = S.centralizer
          source
          @[simp]
          theorem AddSubsemigroup.coe_centralizer {M : Type u_1} (S : Set M) [AddSemigroup M] :
          ↑(centralizer S) = S.addCentralizer
          source
          theorem Subsemigroup.mem_centralizer_iff {M : Type u_1} {S : Set M} [Semigroup M] {z : M} :
          z ∈ centralizer S ↔ ∀ g ∈ S, g * z = z * g
          source
          theorem AddSubsemigroup.mem_centralizer_iff {M : Type u_1} {S : Set M} [AddSemigroup M] {z : M} :
          z ∈ centralizer S ↔ ∀ g ∈ S, g + z = z + g
          source
          instance Subsemigroup.decidableMemCentralizer {M : Type u_1} {S : Set M} [Semigroup M] (a : M) [Decidable (∀ b ∈ S, b * a = a * b)] :
          Decidable (a ∈ centralizer S)
          Equations
            source
            instance AddSubsemigroup.decidableMemCentralizer {M : Type u_1} {S : Set M} [AddSemigroup M] (a : M) [Decidable (∀ b ∈ S, b + a = a + b)] :
            Decidable (a ∈ centralizer S)
            Equations
              source
              theorem Subsemigroup.center_le_centralizer {M : Type u_1} [Semigroup M] (S : Set M) :
              center M ≤ centralizer S
              source
              theorem AddSubsemigroup.center_le_centralizer {M : Type u_1} [AddSemigroup M] (S : Set M) :
              center M ≤ centralizer S
              source
              theorem Subsemigroup.centralizer_le {M : Type u_1} {S T : Set M} [Semigroup M] (h : S ⊆ T) :
              centralizer T ≤ centralizer S
              source
              theorem AddSubsemigroup.centralizer_le {M : Type u_1} {S T : Set M} [AddSemigroup M] (h : S ⊆ T) :
              centralizer T ≤ centralizer S
              source
              @[simp]
              theorem Subsemigroup.centralizer_eq_top_iff_subset {M : Type u_1} [Semigroup M] {s : Set M} :
              centralizer s = ⊤ ↔ s ⊆ ↑(center M)
              source
              @[simp]
              theorem AddSubsemigroup.centralizer_eq_top_iff_subset {M : Type u_1} [AddSemigroup M] {s : Set M} :
              centralizer s = ⊤ ↔ s ⊆ ↑(center M)
              source
              @[simp]
              theorem Subsemigroup.centralizer_univ (M : Type u_1) [Semigroup M] :
              centralizer Set.univ = center M
              source
              @[simp]
              theorem AddSubsemigroup.centralizer_univ (M : Type u_1) [AddSemigroup M] :
              centralizer Set.univ = center M
              source
              theorem Subsemigroup.closure_le_centralizer_centralizer {M : Type u_1} [Semigroup M] (s : Set M) :
              closure s ≤ centralizer ↑(centralizer s)
              source
              theorem AddSubsemigroup.closure_le_centralizer_centralizer {M : Type u_1} [AddSemigroup M] (s : Set M) :
              closure s ≤ centralizer ↑(centralizer s)
              source
              @[reducible, inline]
              abbrev Subsemigroup.closureCommSemigroupOfComm (M : Type u_1) [Semigroup M] {s : Set M} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) :
              CommSemigroup ↥(closure s)

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

              Equations
                Instances For
                  source
                  @[reducible, inline]
                  abbrev AddSubsemigroup.closureAddCommSemigroupOfComm (M : Type u_1) [AddSemigroup M] {s : Set M} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a + b = b + a) :
                  AddCommSemigroup ↥(closure s)

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

                  Equations
                    Instances For