Documentation

Mathlib.GroupTheory.Subgroup.Centralizer

Centralizers of subgroups #

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

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

Equations

AddSubgroup.centralizer s = let __src := AddSubmonoid.centralizer s; { carrier := s.addCentralizer, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

Instances For

theorem AddSubgroup.centralizer.proof_2 {G : Type u_1} [AddGroup G] (s : Set G) :

0 ∈ (AddSubmonoid.centralizer s).carrier

theorem AddSubgroup.centralizer.proof_1 {G : Type u_1} [AddGroup G] (s : Set G) :

∀ {a b : G}, a ∈ (AddSubmonoid.centralizer s).carrier → b ∈ (AddSubmonoid.centralizer s).carrier → a + b ∈ (AddSubmonoid.centralizer s).carrier

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

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

Equations

Subgroup.centralizer s = let __src := Submonoid.centralizer s; { carrier := s.centralizer, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

Instances For

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

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

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

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

theorem AddSubgroup.centralizer_univ {G : Type u_1} [AddGroup G] :

AddSubgroup.centralizer Set.univ = AddSubgroup.center G

theorem Subgroup.centralizer_univ {G : Type u_1} [Group G] :

Subgroup.centralizer Set.univ = Subgroup.center G

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

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

theorem AddSubgroup.center_le_centralizer {G : Type u_1} [AddGroup G] (s : Set G) :

AddSubgroup.center G ≤ AddSubgroup.centralizer s

theorem Subgroup.center_le_centralizer {G : Type u_1} [Group G] (s : Set G) :

Subgroup.center G ≤ Subgroup.centralizer s

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

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

@[simp]

theorem AddSubgroup.centralizer_eq_top_iff_subset {G : Type u_1} [AddGroup G] {s : Set G} :

AddSubgroup.centralizer s = ⊤ ↔ s ⊆ ↑(AddSubgroup.center G)

@[simp]

theorem Subgroup.centralizer_eq_top_iff_subset {G : Type u_1} [Group G] {s : Set G} :

Subgroup.centralizer s = ⊤ ↔ s ⊆ ↑(Subgroup.center G)

instance AddSubgroup.Centralizer.characteristic {G : Type u_1} [AddGroup G] {H : AddSubgroup G} [hH : H.Characteristic] :

(AddSubgroup.centralizer ↑H).Characteristic

Equations

⋯ = ⋯

instance Subgroup.Centralizer.characteristic {G : Type u_1} [Group G] {H : Subgroup G} [hH : H.Characteristic] :

(Subgroup.centralizer ↑H).Characteristic

Equations

⋯ = ⋯

theorem AddSubgroup.le_centralizer_iff_isCommutative {G : Type u_1} [AddGroup G] {K : AddSubgroup G} :

K ≤ AddSubgroup.centralizer ↑K ↔ K.IsCommutative

theorem Subgroup.le_centralizer_iff_isCommutative {G : Type u_1} [Group G] {K : Subgroup G} :

K ≤ Subgroup.centralizer ↑K ↔ K.IsCommutative

theorem AddSubgroup.le_centralizer {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [h : H.IsCommutative] :

H ≤ AddSubgroup.centralizer ↑H

theorem Subgroup.le_centralizer {G : Type u_1} [Group G] (H : Subgroup G) [h : H.IsCommutative] :

H ≤ Subgroup.centralizer ↑H