Documentation

Mathlib.Algebra.Group.Centralizer

Centralizers of magmas and semigroups #

Main definitions #

See Mathlib.GroupTheory.Subsemigroup.Centralizer for the definition of the centralizer as a subsemigroup:

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

source
def Set.addCentralizer {M : Type u_1} (S : Set M) [Add M] :
Set M

The centralizer of a subset of an additive magma.

Equations
  • S.addCentralizer = {c : M | ∀ m ∈ S, m + c = c + m}
Instances For
    source
    def Set.centralizer {M : Type u_1} (S : Set M) [Mul M] :
    Set M

    The centralizer of a subset of a magma.

    Equations
    • S.centralizer = {c : M | ∀ m ∈ S, m * c = c * m}
    Instances For
      source
      theorem Set.mem_addCentralizer {M : Type u_1} {S : Set M} [Add M] {c : M} :
      c ∈ S.addCentralizer ↔ ∀ m ∈ S, m + c = c + m
      source
      theorem Set.mem_centralizer_iff {M : Type u_1} {S : Set M} [Mul M] {c : M} :
      c ∈ S.centralizer ↔ ∀ m ∈ S, m * c = c * m
      source
      instance Set.decidableMemAddCentralizer {M : Type u_1} {S : Set M} [Add M] [(a : M) → Decidable (∀ b ∈ S, b + a = a + b)] :
      DecidablePred fun (x : M) => x ∈ S.addCentralizer
      Equations
      source
      instance Set.decidableMemCentralizer {M : Type u_1} {S : Set M} [Mul M] [(a : M) → Decidable (∀ b ∈ S, b * a = a * b)] :
      DecidablePred fun (x : M) => x ∈ S.centralizer
      Equations
      source
      @[simp]
      theorem Set.zero_mem_addCentralizer {M : Type u_1} (S : Set M) [AddZeroClass M] :
      0 ∈ S.addCentralizer
      source
      @[simp]
      theorem Set.one_mem_centralizer {M : Type u_1} (S : Set M) [MulOneClass M] :
      1 ∈ S.centralizer
      source
      @[simp]
      theorem Set.zero_mem_centralizer {M : Type u_1} (S : Set M) [MulZeroClass M] :
      0 ∈ S.centralizer
      source
      @[simp]
      theorem Set.add_mem_addCentralizer {M : Type u_1} {S : Set M} {a : M} {b : M} [AddSemigroup M] (ha : a ∈ S.addCentralizer) (hb : b ∈ S.addCentralizer) :
      a + b ∈ S.addCentralizer
      source
      @[simp]
      theorem Set.mul_mem_centralizer {M : Type u_1} {S : Set M} {a : M} {b : M} [Semigroup M] (ha : a ∈ S.centralizer) (hb : b ∈ S.centralizer) :
      a * b ∈ S.centralizer
      source
      @[simp]
      theorem Set.neg_mem_addCentralizer {M : Type u_1} {S : Set M} {a : M} [AddGroup M] (ha : a ∈ S.addCentralizer) :
      -a ∈ S.addCentralizer
      source
      @[simp]
      theorem Set.inv_mem_centralizer {M : Type u_1} {S : Set M} {a : M} [Group M] (ha : a ∈ S.centralizer) :
      a⁻¹ ∈ S.centralizer
      source
      @[simp]
      theorem Set.inv_mem_centralizer₀ {M : Type u_1} {S : Set M} {a : M} [GroupWithZero M] (ha : a ∈ S.centralizer) :
      a⁻¹ ∈ S.centralizer
      source
      @[simp]
      theorem Set.sub_mem_addCentralizer {M : Type u_1} {S : Set M} {a : M} {b : M} [AddGroup M] (ha : a ∈ S.addCentralizer) (hb : b ∈ S.addCentralizer) :
      a - b ∈ S.addCentralizer
      source
      @[simp]
      theorem Set.div_mem_centralizer {M : Type u_1} {S : Set M} {a : M} {b : M} [Group M] (ha : a ∈ S.centralizer) (hb : b ∈ S.centralizer) :
      a / b ∈ S.centralizer
      source
      @[simp]
      theorem Set.div_mem_centralizer₀ {M : Type u_1} {S : Set M} {a : M} {b : M} [GroupWithZero M] (ha : a ∈ S.centralizer) (hb : b ∈ S.centralizer) :
      a / b ∈ S.centralizer
      source
      theorem Set.addCentralizer_subset {M : Type u_1} {S : Set M} {T : Set M} [Add M] (h : S ⊆ T) :
      T.addCentralizer ⊆ S.addCentralizer
      source
      theorem Set.centralizer_subset {M : Type u_1} {S : Set M} {T : Set M} [Mul M] (h : S ⊆ T) :
      T.centralizer ⊆ S.centralizer
      source
      theorem Set.addCenter_subset_addCentralizer {M : Type u_1} [Add M] (S : Set M) :
      Set.addCenter M ⊆ S.addCentralizer
      source
      theorem Set.center_subset_centralizer {M : Type u_1} [Mul M] (S : Set M) :
      Set.center M ⊆ S.centralizer
      source
      @[simp]
      theorem Set.addCentralizer_eq_top_iff_subset {M : Type u_1} {s : Set M} [AddSemigroup M] :
      s.addCentralizer = Set.univ ↔ s ⊆ Set.addCenter M
      source
      @[simp]
      theorem Set.centralizer_eq_top_iff_subset {M : Type u_1} {s : Set M} [Semigroup M] :
      s.centralizer = Set.univ ↔ s ⊆ Set.center M
      source
      @[simp]
      theorem Set.addCentralizer_univ (M : Type u_1) [AddSemigroup M] :
      Set.univ.addCentralizer = Set.addCenter M
      source
      @[simp]
      theorem Set.centralizer_univ (M : Type u_1) [Semigroup M] :
      Set.univ.centralizer = Set.center M
      source
      @[simp]
      theorem Set.addCentralizer_eq_univ {M : Type u_1} (S : Set M) [AddCommSemigroup M] :
      S.addCentralizer = Set.univ
      source
      @[simp]
      theorem Set.centralizer_eq_univ {M : Type u_1} (S : Set M) [CommSemigroup M] :
      S.centralizer = Set.univ
      source
      theorem Set.subset_addCentralizer_addCentralizer {M : Type u_1} [Add M] {s : Set M} :
      s ⊆ s.addCentralizer.addCentralizer
      source
      theorem Set.subset_centralizer_centralizer {M : Type u_1} [Mul M] {s : Set M} :
      s ⊆ s.centralizer.centralizer
      source
      @[simp]
      theorem Set.addCentralizer_addCentralizer_addCentralizer {M : Type u_1} [Add M] {s : Set M} :
      s.addCentralizer.addCentralizer.addCentralizer = s.addCentralizer
      source
      @[simp]
      theorem Set.centralizer_centralizer_centralizer {M : Type u_1} [Mul M] {s : Set M} :
      s.centralizer.centralizer.centralizer = s.centralizer