Centralizers of subgroups

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

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

Equations

• Subgroup.centralizer s = { carrier := s.centralizer, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

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

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

Equations

• AddSubgroup.centralizer s = { carrier := s.addCentralizer, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

theorem Subgroup.mem_centralizer_iff {G : Type u_1} [Group G] {g : G} {s : Set G} : g ∈ centralizer s ↔ ∀ h ∈ s, h * g = g * h

theorem AddSubgroup.mem_centralizer_iff {G : Type u_1} [AddGroup G] {g : G} {s : Set G} : g ∈ centralizer s ↔ ∀ h ∈ s, h + g = g + h

theorem Subgroup.mem_centralizer_iff_commutator_eq_one {G : Type u_1} [Group G] {g : G} {s : Set G} : g ∈ centralizer s ↔ ∀ h ∈ s, h * g * h⁻¹ * g⁻¹ = 1

theorem AddSubgroup.mem_centralizer_iff_commutator_eq_zero {G : Type u_1} [AddGroup G] {g : G} {s : Set G} : g ∈ centralizer s ↔ ∀ h ∈ s, h + g + -h + -g = 0

theorem Subgroup.mem_centralizer_singleton_iff {G : Type u_1} [Group G] {g k : G} : k ∈ centralizer {g} ↔ k * g = g * k

theorem AddSubgroup.mem_centralizer_singleton_iff {G : Type u_1} [AddGroup G] {g k : G} : k ∈ centralizer {g} ↔ k + g = g + k

theorem Subgroup.centralizer_univ {G : Type u_1} [Group G] : centralizer Set.univ = center G

theorem AddSubgroup.centralizer_univ {G : Type u_1} [AddGroup G] : centralizer Set.univ = center G

theorem Subgroup.le_centralizer_iff {G : Type u_1} [Group G] {H K : Subgroup G} : H ≤ centralizer ↑K ↔ K ≤ centralizer ↑H

theorem AddSubgroup.le_centralizer_iff {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} : H ≤ centralizer ↑K ↔ K ≤ centralizer ↑H

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

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

theorem Subgroup.centralizer_le {G : Type u_1} [Group G] {s t : Set G} (h : s ⊆ t) : centralizer t ≤ centralizer s

theorem AddSubgroup.centralizer_le {G : Type u_1} [AddGroup G] {s t : Set G} (h : s ⊆ t) : centralizer t ≤ centralizer s

@[simp]

theorem Subgroup.centralizer_eq_top_iff_subset {G : Type u_1} [Group G] {s : Set G} : centralizer s = ⊤ ↔ s ⊆ ↑(center G)

@[simp]

theorem AddSubgroup.centralizer_eq_top_iff_subset {G : Type u_1} [AddGroup G] {s : Set G} : centralizer s = ⊤ ↔ s ⊆ ↑(center G)

theorem Subgroup.map_centralizer_le_centralizer_image {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (s : Set G) (f : G →* G') : map f (centralizer s) ≤ centralizer (⇑f '' s)

theorem AddSubgroup.map_centralizer_le_centralizer_image {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (s : Set G) (f : G →+ G') : map f (centralizer s) ≤ centralizer (⇑f '' s)

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

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

theorem Subgroup.le_centralizer_iff_isMulCommutative {G : Type u_1} [Group G] {K : Subgroup G} : K ≤ centralizer ↑K ↔ IsMulCommutative ↥K

theorem AddSubgroup.le_centralizer_iff_isAddCommutative {G : Type u_1} [AddGroup G] {K : AddSubgroup G} : K ≤ centralizer ↑K ↔ IsAddCommutative ↥K

@[deprecated Subgroup.le_centralizer_iff_isMulCommutative (since := "2025-04-09")]

theorem Subgroup.le_centralizer_iff_isCommutative {G : Type u_1} [Group G] {K : Subgroup G} : K ≤ centralizer ↑K ↔ IsMulCommutative ↥K

Alias of Subgroup.le_centralizer_iff_isMulCommutative.

@[deprecated AddSubgroup.le_centralizer_iff_isAddCommutative (since := "2025-04-09")]

theorem AddSubgroup.le_centralizer_iff_isCommutative {G : Type u_1} [AddGroup G] {K : AddSubgroup G} : K ≤ centralizer ↑K ↔ IsAddCommutative ↥K

Alias of AddSubgroup.le_centralizer_iff_isAddCommutative.

theorem Subgroup.le_centralizer {G : Type u_1} [Group G] (H : Subgroup G) [h : IsMulCommutative ↥H] : H ≤ centralizer ↑H

theorem AddSubgroup.le_centralizer {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [h : IsAddCommutative ↥H] : H ≤ centralizer ↑H

theorem Subgroup.closure_le_centralizer_centralizer {G : Type u_1} [Group G] (s : Set G) : closure s ≤ centralizer ↑(centralizer s)

theorem AddSubgroup.closure_le_centralizer_centralizer {G : Type u_1} [AddGroup G] (s : Set G) : closure s ≤ centralizer ↑(centralizer s)

@[reducible, inline]

abbrev Subgroup.closureCommGroupOfComm {G : Type u_1} [Group G] {k : Set G} (hcomm : ∀ x ∈ k, ∀ y ∈ k, x * y = y * x) : CommGroup ↥(closure k)

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

Equations

• Subgroup.closureCommGroupOfComm hcomm = { toGroup := (Subgroup.closure k).toGroup, mul_comm := ⋯ }

@[reducible, inline]

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

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

Equations

• AddSubgroup.closureAddCommGroupOfComm hcomm = { toAddGroup := (AddSubgroup.closure k).toAddGroup, add_comm := ⋯ }

instance Subgroup.instMulDistribMulActionSubtypeMemNormalizer {G : Type u_1} [Group G] (H : Subgroup G) : MulDistribMulAction ↥H.normalizer ↥H

The conjugation action of N(H) on H.

Equations

• H.instMulDistribMulActionSubtypeMemNormalizer = { smul := fun (g : ↥H.normalizer) (h : ↥H) => ⟨↑g * ↑h * ↑g⁻¹, ⋯⟩, one_smul := ⋯, mul_smul := ⋯, smul_mul := ⋯, smul_one := ⋯ }

@[simp]

theorem Subgroup.smul_coe {G : Type u_1} [Group G] (H : Subgroup G) (g : ↥H.normalizer) (h : ↥H) : ↑(SMul.smul g h) = ↑g * ↑h * ↑g⁻¹

def Subgroup.normalizerMonoidHom {G : Type u_1} [Group G] (H : Subgroup G) : ↥H.normalizer →* MulAut ↥H

The homomorphism N(H) → Aut(H) with kernel C(H).

Equations

• H.normalizerMonoidHom = MulDistribMulAction.toMulAut ↥H.normalizer ↥H

@[simp]

theorem Subgroup.normalizerMonoidHom_apply_apply_coe {G : Type u_1} [Group G] (H : Subgroup G) (x : ↥H.normalizer) (a✝ : ↥H) : ↑((H.normalizerMonoidHom x) a✝) = ↑x * ↑a✝ * (↑x)⁻¹

@[simp]

theorem Subgroup.normalizerMonoidHom_apply_symm_apply_coe {G : Type u_1} [Group G] (H : Subgroup G) (x : ↥H.normalizer) (a✝ : ↥H) : ↑((MulEquiv.symm (H.normalizerMonoidHom x)) a✝) = (↑x)⁻¹ * ↑a✝ * ↑x

theorem Subgroup.normalizerMonoidHom_ker {G : Type u_1} [Group G] (H : Subgroup G) : H.normalizerMonoidHom.ker = (centralizer ↑H).subgroupOf H.normalizer