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.

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.

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_addCommutator_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.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.

@[reducible, inline, deprecated Subgroup.isMulCommutative_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.

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)

@[implicit_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.

@[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).

@[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)