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 = { toSubmonoid := Submonoid.centralizer s, 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 = { toAddSubmonoid := AddSubmonoid.centralizer s, 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⁆ = 1

theorem AddSubgroup.mem_centralizer_iff_addCommutator_eq_zero {G : Type u_1} [AddGroup G] {g : G} {s : Set G} : g ∈ centralizer s ↔ ∀ h ∈ s, ⁅h, g⁆ = 0

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

theorem AddSubgroup.mem_centralizer_iff_addCommutator_eq_zero' {G : Type u_1} [AddGroup G] {g : G} {s : Set G} : g ∈ centralizer s ↔ ∀ h ∈ s, ⁅g, h⁆ = 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)

@[simp]

theorem Subgroup.centralizer_center {G : Type u_1} [Group G] : centralizer ↑(center G) = ⊤

@[simp]

theorem AddSubgroup.centralizer_center {G : Type u_1} [AddGroup G] : centralizer ↑(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.normal_centralizer {G : Type u_1} [Group G] {H : Subgroup G} [H.Normal] : (centralizer ↑H).Normal

instance AddSubgroup.normal_centralizer {G : Type u_1} [AddGroup G] {H : AddSubgroup G} [H.Normal] : (centralizer ↑H).Normal

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

instance AddSubgroup.characteristic_centralizer {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

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)

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

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

theorem Subgroup.centralizer_eq_iInf {G : Type u_1} [Group G] (s : Set G) : centralizer s = ⨅ g ∈ s, centralizer {g}

theorem AddSubgroup.centralizer_eq_iInf {G : Type u_1} [AddGroup G] (s : Set G) : centralizer s = ⨅ g ∈ s, centralizer {g}

theorem Subgroup.center_eq_iInf {G : Type u_1} [Group G] {s : Set G} (hs : closure s = ⊤) : center G = ⨅ g ∈ s, centralizer {g}

theorem AddSubgroup.center_eq_iInf {G : Type u_1} [AddGroup G] {s : Set G} (hs : closure s = ⊤) : center G = ⨅ g ∈ s, centralizer {g}

theorem Subgroup.center_eq_infi' {G : Type u_1} [Group G] {s : Set G} (hs : closure s = ⊤) : center G = ⨅ (g : ↑s), centralizer {↑g}

theorem AddSubgroup.center_eq_infi' {G : Type u_1} [AddGroup G] {s : Set G} (hs : closure s = ⊤) : center G = ⨅ (g : ↑s), centralizer {↑g}

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

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

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

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

@[reducible, inline, deprecated Subgroup.isMulCommutative_closure (since := "2026-03-10")]

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 = inferInstance

@[reducible, inline, deprecated AddSubgroup.isAddCommutative_closure (since := "2026-03-10")]

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 = inferInstance

instance Subgroup.instIsMulCommutative_closure {G : Type u_1} [Group G] {S : Type u_3} [SetLike S G] [MulMemClass S G] (s : S) [IsMulCommutative ↥s] : IsMulCommutative ↥(closure ↑s)

instance AddSubgroup.instIsAddCommutative_closure {G : Type u_1} [AddGroup G] {S : Type u_3} [SetLike S G] [AddMemClass S G] (s : S) [IsAddCommutative ↥s] : IsAddCommutative ↥(closure ↑s)

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

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

instance Subgroup.normal_subgroupOf_centralizer_normalizer {G : Type u_1} [Group G] (s : Set G) : ((centralizer s).subgroupOf (normalizer s)).Normal

instance AddSubgroup.normal_addSubgroupOf_centralizer_normalizer {G : Type u_1} [AddGroup G] (s : Set G) : ((centralizer s).addSubgroupOf (normalizer s)).Normal

theorem Subgroup.normalizer_singleton {G : Type u_1} [Group G] (g : G) : normalizer {g} = centralizer {g}

theorem AddSubgroup.normalizer_singleton {G : Type u_1} [AddGroup G] (g : G) : normalizer {g} = centralizer {g}

@[instance_reducible]

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

The conjugation action of N(H) on H.

Equations

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

@[simp]

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

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

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

Equations

• H.normalizerMonoidHom = MulDistribMulAction.toMulAut ↥(Subgroup.normalizer ↑H) ↥H

@[simp]

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

@[simp]

theorem Subgroup.normalizerMonoidHom_apply_apply_coe {G : Type u_1} [Group G] (H : Subgroup G) (x : ↥(normalizer ↑H)) (a✝ : ↥H) : ↑((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 (normalizer ↑H)