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
    theorem AddSubgroup.centralizer.proof_2 {G : Type u_1} [AddGroup G] (s : Set G) :
    0 ∈ (AddSubmonoid.centralizer s).carrier
    source
    theorem AddSubgroup.centralizer.proof_1 {G : Type u_1} [AddGroup G] (s : Set G) {a : G} {b : G} :
    a ∈ (AddSubmonoid.centralizer s).carrier → b ∈ (AddSubmonoid.centralizer s).carrier → a + b ∈ (AddSubmonoid.centralizer s).carrier
    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.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 : Subgroup G} {K : Subgroup G} :
      H ≤ Subgroup.centralizer ↑K ↔ K ≤ Subgroup.centralizer ↑H
      source
      theorem AddSubgroup.le_centralizer_iff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {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 : Set G} {t : Set G} (h : s ⊆ t) :
      Subgroup.centralizer t ≤ Subgroup.centralizer s
      source
      theorem AddSubgroup.centralizer_le {G : Type u_1} [AddGroup G] {s : Set G} {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