Centralizers of subgroups

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

• 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 H is the additive subgroup of g : G commuting with every h : H.

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 ∈ Subgroup.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 ∈ AddSubgroup.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 ∈ Subgroup.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 ∈ AddSubgroup.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 ∈ Subgroup.centralizer {g} ↔ k * g = g * k

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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_iff_isCommutative {G : Type u_1} [AddGroup G] {K : AddSubgroup G} : K ≤ AddSubgroup.centralizer ↑K ↔ K.IsCommutative

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

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

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

theorem AddSubgroup.closure_le_centralizer_centralizer {G : Type u_1} [AddGroup G] (s : Set G) : AddSubgroup.closure s ≤ AddSubgroup.centralizer ↑(AddSubgroup.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 ↥(Subgroup.closure k)

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

Equations

• Subgroup.closureCommGroupOfComm hcomm = CommGroup.mk ⋯

@[reducible, inline]

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

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

Equations

• AddSubgroup.closureAddCommGroupOfComm hcomm = AddCommGroup.mk ⋯

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 = MulDistribMulAction.mk ⋯ ⋯

@[simp]

theorem Subgroup.instMulDistribMulActionSubtypeMemNormalizer_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 = (Subgroup.centralizer ↑H).subgroupOf H.normalizer