Centralizers of subgroups

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

• One or more equations did not get rendered due to their size.

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) : Subgroup 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; { toSubmonoid := { toSubsemigroup := { carrier := Set.centralizer s, mul_mem' := ⋯ }, one_mem' := ⋯ }, inv_mem' := ⋯ }

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 : AddSubgroup.Characteristic H] : AddSubgroup.Characteristic (AddSubgroup.centralizer ↑H)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

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

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