Commutators of Subgroups

If G is a group and H₁ H₂ : Subgroup G then the commutator ⁅H₁, H₂⁆ : Subgroup G is the subgroup of G generated by the commutators h₁ * h₂ * h₁⁻¹ * h₂⁻¹.

Main definitions

• ⁅g₁, g₂⁆ : the commutator of the elements g₁ and g₂ (defined by commutatorElement elsewhere).
• ⁅H₁, H₂⁆ : the commutator of the subgroups H₁ and H₂.

theorem commutatorElement_eq_one_iff_mul_comm {G : Type u_1} [Group G] {g₁ : G} {g₂ : G} : ⁅g₁, g₂⁆ = 1 ↔ g₁ * g₂ = g₂ * g₁

theorem commutatorElement_eq_one_iff_commute {G : Type u_1} [Group G] {g₁ : G} {g₂ : G} : ⁅g₁, g₂⁆ = 1 ↔ Commute g₁ g₂

theorem Commute.commutator_eq {G : Type u_1} [Group G] {g₁ : G} {g₂ : G} (h : Commute g₁ g₂) : ⁅g₁, g₂⁆ = 1

@[simp]

theorem commutatorElement_one_right {G : Type u_1} [Group G] (g : G) : ⁅g, 1⁆ = 1

@[simp]

theorem commutatorElement_one_left {G : Type u_1} [Group G] (g : G) : ⁅1, g⁆ = 1

@[simp]

theorem commutatorElement_self {G : Type u_1} [Group G] (g : G) : ⁅g, g⁆ = 1

@[simp]

theorem commutatorElement_inv {G : Type u_1} [Group G] (g₁ : G) (g₂ : G) : ⁅g₁, g₂⁆⁻¹ = ⁅g₂, g₁⁆

theorem map_commutatorElement {G : Type u_1} {G' : Type u_2} {F : Type u_3} [Group G] [Group G'] [FunLike F G G'] [MonoidHomClass F G G'] (f : F) (g₁ : G) (g₂ : G) : f ⁅g₁, g₂⁆ = ⁅f g₁, f g₂⁆

theorem conjugate_commutatorElement {G : Type u_1} [Group G] (g₁ : G) (g₂ : G) (g₃ : G) : g₃ * ⁅g₁, g₂⁆ * g₃⁻¹ = ⁅g₃ * g₁ * g₃⁻¹, g₃ * g₂ * g₃⁻¹⁆

instance Subgroup.commutator {G : Type u_1} [Group G] : Bracket (Subgroup G) (Subgroup G)

The commutator of two subgroups H₁ and H₂.

Equations

• Subgroup.commutator = { bracket := fun (H₁ H₂ : Subgroup G) => Subgroup.closure {g : G | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g} }

theorem Subgroup.commutator_def {G : Type u_1} [Group G] (H₁ : Subgroup G) (H₂ : Subgroup G) : ⁅H₁, H₂⁆ = Subgroup.closure {g : G | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g}

theorem Subgroup.commutator_mem_commutator {G : Type u_1} [Group G] {g₁ : G} {g₂ : G} {H₁ : Subgroup G} {H₂ : Subgroup G} (h₁ : g₁ ∈ H₁) (h₂ : g₂ ∈ H₂) : ⁅g₁, g₂⁆ ∈ ⁅H₁, H₂⁆

theorem Subgroup.commutator_le {G : Type u_1} [Group G] {H₁ : Subgroup G} {H₂ : Subgroup G} {H₃ : Subgroup G} : ⁅H₁, H₂⁆ ≤ H₃ ↔ ∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅g₁, g₂⁆ ∈ H₃

theorem Subgroup.commutator_mono {G : Type u_1} [Group G] {H₁ : Subgroup G} {H₂ : Subgroup G} {K₁ : Subgroup G} {K₂ : Subgroup G} (h₁ : H₁ ≤ K₁) (h₂ : H₂ ≤ K₂) : ⁅H₁, H₂⁆ ≤ ⁅K₁, K₂⁆

theorem Subgroup.commutator_eq_bot_iff_le_centralizer {G : Type u_1} [Group G] {H₁ : Subgroup G} {H₂ : Subgroup G} : ⁅H₁, H₂⁆ = ⊥ ↔ H₁ ≤ Subgroup.centralizer ↑H₂

theorem Subgroup.commutator_commutator_eq_bot_of_rotate {G : Type u_1} [Group G] {H₁ : Subgroup G} {H₂ : Subgroup G} {H₃ : Subgroup G} (h1 : ⁅⁅H₂, H₃⁆, H₁⁆ = ⊥) (h2 : ⁅⁅H₃, H₁⁆, H₂⁆ = ⊥) : ⁅⁅H₁, H₂⁆, H₃⁆ = ⊥

The Three Subgroups Lemma (via the Hall-Witt identity)

theorem Subgroup.commutator_comm_le {G : Type u_1} [Group G] (H₁ : Subgroup G) (H₂ : Subgroup G) : ⁅H₁, H₂⁆ ≤ ⁅H₂, H₁⁆

theorem Subgroup.commutator_comm {G : Type u_1} [Group G] (H₁ : Subgroup G) (H₂ : Subgroup G) : ⁅H₁, H₂⁆ = ⁅H₂, H₁⁆

instance Subgroup.commutator_normal {G : Type u_1} [Group G] (H₁ : Subgroup G) (H₂ : Subgroup G) [h₁ : Subgroup.Normal H₁] [h₂ : Subgroup.Normal H₂] : Subgroup.Normal ⁅H₁, H₂⁆

Equations

• (_ : Subgroup.Normal ⁅H₁, H₂⁆) = (_ : let base := {x : G | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = x}; Subgroup.Normal (Subgroup.closure base))

theorem Subgroup.commutator_def' {G : Type u_1} [Group G] (H₁ : Subgroup G) (H₂ : Subgroup G) [Subgroup.Normal H₁] [Subgroup.Normal H₂] : ⁅H₁, H₂⁆ = Subgroup.normalClosure {g : G | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g}

theorem Subgroup.commutator_le_right {G : Type u_1} [Group G] (H₁ : Subgroup G) (H₂ : Subgroup G) [h : Subgroup.Normal H₂] : ⁅H₁, H₂⁆ ≤ H₂

theorem Subgroup.commutator_le_left {G : Type u_1} [Group G] (H₁ : Subgroup G) (H₂ : Subgroup G) [Subgroup.Normal H₁] : ⁅H₁, H₂⁆ ≤ H₁

@[simp]

theorem Subgroup.commutator_bot_left {G : Type u_1} [Group G] (H₁ : Subgroup G) : ⁅⊥, H₁⁆ = ⊥

@[simp]

theorem Subgroup.commutator_bot_right {G : Type u_1} [Group G] (H₁ : Subgroup G) : ⁅H₁, ⊥⁆ = ⊥

theorem Subgroup.commutator_le_inf {G : Type u_1} [Group G] (H₁ : Subgroup G) (H₂ : Subgroup G) [Subgroup.Normal H₁] [Subgroup.Normal H₂] : ⁅H₁, H₂⁆ ≤ H₁ ⊓ H₂

theorem Subgroup.map_commutator {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H₁ : Subgroup G) (H₂ : Subgroup G) (f : G →* G') : Subgroup.map f ⁅H₁, H₂⁆ = ⁅Subgroup.map f H₁, Subgroup.map f H₂⁆

theorem Subgroup.commutator_le_map_commutator {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {H₁ : Subgroup G} {H₂ : Subgroup G} {f : G →* G'} {K₁ : Subgroup G'} {K₂ : Subgroup G'} (h₁ : K₁ ≤ Subgroup.map f H₁) (h₂ : K₂ ≤ Subgroup.map f H₂) : ⁅K₁, K₂⁆ ≤ Subgroup.map f ⁅H₁, H₂⁆

instance Subgroup.commutator_characteristic {G : Type u_1} [Group G] (H₁ : Subgroup G) (H₂ : Subgroup G) [h₁ : Subgroup.Characteristic H₁] [h₂ : Subgroup.Characteristic H₂] : Subgroup.Characteristic ⁅H₁, H₂⁆

Equations

• (_ : Subgroup.Characteristic ⁅H₁, H₂⁆) = (_ : Subgroup.Characteristic ⁅H₁, H₂⁆)

theorem Subgroup.commutator_prod_prod {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H₁ : Subgroup G) (H₂ : Subgroup G) (K₁ : Subgroup G') (K₂ : Subgroup G') : ⁅Subgroup.prod H₁ K₁, Subgroup.prod H₂ K₂⁆ = Subgroup.prod ⁅H₁, H₂⁆ ⁅K₁, K₂⁆

theorem Subgroup.commutator_pi_pi_le {η : Type u_4} {Gs : η → Type u_5} [(i : η) → Group (Gs i)] (H : (i : η) → Subgroup (Gs i)) (K : (i : η) → Subgroup (Gs i)) : ⁅Subgroup.pi Set.univ H, Subgroup.pi Set.univ K⁆ ≤ Subgroup.pi Set.univ fun (i : η) => ⁅H i, K i⁆

The commutator of direct product is contained in the direct product of the commutators.

See commutator_pi_pi_of_finite for equality given Fintype η.

theorem Subgroup.commutator_pi_pi_of_finite {η : Type u_4} [Finite η] {Gs : η → Type u_5} [(i : η) → Group (Gs i)] (H : (i : η) → Subgroup (Gs i)) (K : (i : η) → Subgroup (Gs i)) : ⁅Subgroup.pi Set.univ H, Subgroup.pi Set.univ K⁆ = Subgroup.pi Set.univ fun (i : η) => ⁅H i, K i⁆

The commutator of a finite direct product is contained in the direct product of the commutators.

def commutatorSet (G : Type u_1) [Group G] : Set G

The set of commutator elements ⁅g₁, g₂⁆ in G.

Equations

• commutatorSet G = {g : G | ∃ (g₁ : G) (g₂ : G), ⁅g₁, g₂⁆ = g}

theorem commutatorSet_def (G : Type u_1) [Group G] : commutatorSet G = {g : G | ∃ (g₁ : G) (g₂ : G), ⁅g₁, g₂⁆ = g}

theorem one_mem_commutatorSet (G : Type u_1) [Group G] : 1 ∈ commutatorSet G

instance instNonemptyElemCommutatorSet (G : Type u_1) [Group G] : Nonempty ↑(commutatorSet G)

Equations

• (_ : Nonempty ↑(commutatorSet G)) = (_ : Nonempty ↑(commutatorSet G))

theorem mem_commutatorSet_iff {G : Type u_1} [Group G] {g : G} : g ∈ commutatorSet G ↔ ∃ (g₁ : G) (g₂ : G), ⁅g₁, g₂⁆ = g

theorem commutator_mem_commutatorSet {G : Type u_1} [Group G] (g₁ : G) (g₂ : G) : ⁅g₁, g₂⁆ ∈ commutatorSet G