Documentation

Mathlib.GroupTheory.Subgroup.Centralizer

Centralizers of subgroups #

source
def Subgroup.centralizer {G : Type u_1} [Group G] (s : Set G) :
Subgroup G

The centralizer of H is the subgroup of g : G commuting with every h : H.

Equations
Instances For
    source
    def AddSubgroup.centralizer {G : Type u_1} [AddGroup G] (s : Set G) :
    AddSubgroup G

    The centralizer of H is the additive subgroup of g : G commuting with every h : H.

    Equations
    Instances For
      source
      theorem Subgroup.mem_centralizer_iff {G : Type u_1} [Group G] {g : G} {s : Set G} :
      g ∈ Subgroup.centralizer s ↔ ∀ h ∈ s, h * g = g * h
      source
      theorem AddSubgroup.mem_centralizer_iff {G : Type u_1} [AddGroup G] {g : G} {s : Set G} :
      g ∈ AddSubgroup.centralizer s ↔ ∀ h ∈ s, h + g = g + h
      source
      theorem Subgroup.mem_centralizer_iff_commutator_eq_one {G : Type u_1} [Group G] {g : G} {s : Set G} :
      g ∈ Subgroup.centralizer s ↔ ∀ h ∈ s, h * g * h⁻¹ * g⁻¹ = 1
      source
      theorem AddSubgroup.mem_centralizer_iff_commutator_eq_zero {G : Type u_1} [AddGroup G] {g : G} {s : Set G} :
      g ∈ AddSubgroup.centralizer s ↔ ∀ h ∈ s, h + g + -h + -g = 0
      source
      theorem Subgroup.mem_centralizer_singleton_iff {G : Type u_1} [Group G] {g k : G} :
      k ∈ Subgroup.centralizer {g} ↔ k * g = g * k
      source
      theorem AddSubgroup.mem_centralizer_singleton_iff {G : Type u_1} [AddGroup G] {g k : G} :
      k ∈ AddSubgroup.centralizer {g} ↔ k + g = g + k
      source
      theorem Subgroup.centralizer_univ {G : Type u_1} [Group G] :
      Subgroup.centralizer Set.univ = Subgroup.center G
      source
      theorem AddSubgroup.centralizer_univ {G : Type u_1} [AddGroup G] :
      AddSubgroup.centralizer Set.univ = AddSubgroup.center G
      source
      theorem Subgroup.le_centralizer_iff {G : Type u_1} [Group G] {H K : Subgroup G} :
      H ≤ Subgroup.centralizer ↑K ↔ K ≤ Subgroup.centralizer ↑H
      source
      theorem AddSubgroup.le_centralizer_iff {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} :
      H ≤ AddSubgroup.centralizer ↑K ↔ K ≤ AddSubgroup.centralizer ↑H
      source
      theorem Subgroup.center_le_centralizer {G : Type u_1} [Group G] (s : Set G) :
      Subgroup.center G ≤ Subgroup.centralizer s
      source
      theorem AddSubgroup.center_le_centralizer {G : Type u_1} [AddGroup G] (s : Set G) :
      AddSubgroup.center G ≤ AddSubgroup.centralizer s
      source
      theorem Subgroup.centralizer_le {G : Type u_1} [Group G] {s t : Set G} (h : s ⊆ t) :
      Subgroup.centralizer t ≤ Subgroup.centralizer s
      source
      theorem AddSubgroup.centralizer_le {G : Type u_1} [AddGroup G] {s t : Set G} (h : s ⊆ t) :
      AddSubgroup.centralizer t ≤ AddSubgroup.centralizer s
      source
      @[simp]
      theorem Subgroup.centralizer_eq_top_iff_subset {G : Type u_1} [Group G] {s : Set G} :
      Subgroup.centralizer s = ⊤ ↔ s ⊆ ↑(Subgroup.center G)
      source
      @[simp]
      theorem AddSubgroup.centralizer_eq_top_iff_subset {G : Type u_1} [AddGroup G] {s : Set G} :
      AddSubgroup.centralizer s = ⊤ ↔ s ⊆ ↑(AddSubgroup.center G)
      source
      instance Subgroup.Centralizer.characteristic {G : Type u_1} [Group G] {H : Subgroup G} [hH : H.Characteristic] :
      (Subgroup.centralizer ↑H).Characteristic
      Equations
      • ⋯ = ⋯
      source
      instance AddSubgroup.Centralizer.characteristic {G : Type u_1} [AddGroup G] {H : AddSubgroup G} [hH : H.Characteristic] :
      (AddSubgroup.centralizer ↑H).Characteristic
      Equations
      • ⋯ = ⋯
      source
      theorem Subgroup.le_centralizer_iff_isCommutative {G : Type u_1} [Group G] {K : Subgroup G} :
      K ≤ Subgroup.centralizer ↑K ↔ K.IsCommutative
      source
      theorem AddSubgroup.le_centralizer_iff_isCommutative {G : Type u_1} [AddGroup G] {K : AddSubgroup G} :
      K ≤ AddSubgroup.centralizer ↑K ↔ K.IsCommutative
      source
      theorem Subgroup.le_centralizer {G : Type u_1} [Group G] (H : Subgroup G) [h : H.IsCommutative] :
      H ≤ Subgroup.centralizer ↑H
      source
      theorem AddSubgroup.le_centralizer {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [h : H.IsCommutative] :
      H ≤ AddSubgroup.centralizer ↑H
      source
      theorem Subgroup.closure_le_centralizer_centralizer {G : Type u_1} [Group G] (s : Set G) :
      Subgroup.closure s ≤ Subgroup.centralizer ↑(Subgroup.centralizer s)
      source
      theorem AddSubgroup.closure_le_centralizer_centralizer {G : Type u_1} [AddGroup G] (s : Set G) :
      AddSubgroup.closure s ≤ AddSubgroup.centralizer ↑(AddSubgroup.centralizer s)
      source
      @[reducible, inline]
      abbrev Subgroup.closureCommGroupOfComm {G : Type u_1} [Group G] {k : Set G} (hcomm : ∀ x ∈ k, ∀ y ∈ k, x * y = y * x) :
      CommGroup ↥(Subgroup.closure k)

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

      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev AddSubgroup.closureAddCommGroupOfComm {G : Type u_1} [AddGroup G] {k : Set G} (hcomm : ∀ x ∈ k, ∀ y ∈ k, x + y = y + x) :
        AddCommGroup ↥(AddSubgroup.closure k)

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

        Equations
        Instances For