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₂.
• commutator: defines the commutator of a group G as a subgroup of G.

theorem conj_eq_commutatorElement_mul {G : Type u_1} [Group G] {g₁ g₂ : G} : (MulAut.conj g₁) g₂ = ⁅g₁, g₂⁆ * g₂

theorem addConj_eq_addCommutatorElement_add {G : Type u_1} [AddGroup G] {g₁ g₂ : G} : (AddAut.addConj g₁) g₂ = ⁅g₁, g₂⁆ + g₂

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

theorem addCommutatorElement_eq_zero_iff_add_comm {G : Type u_1} [AddGroup G] {g₁ g₂ : G} : ⁅g₁, g₂⁆ = 0 ↔ g₁ + g₂ = g₂ + g₁

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

theorem addCommutatorElement_eq_zero_iff_addCommute {G : Type u_1} [AddGroup G] {g₁ g₂ : G} : ⁅g₁, g₂⁆ = 0 ↔ AddCommute g₁ g₂

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

theorem AddCommute.addCommutator_eq {G : Type u_1} [AddGroup G] {g₁ g₂ : G} (h : AddCommute g₁ g₂) : ⁅g₁, g₂⁆ = 0

@[simp]

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

@[simp]

theorem addCommutatorElement_zero_right {G : Type u_1} [AddGroup G] (g : G) : ⁅g, 0⁆ = 0

@[simp]

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

@[simp]

theorem addCommutatorElement_zero_left {G : Type u_1} [AddGroup G] (g : G) : ⁅0, g⁆ = 0

@[simp]

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

@[simp]

theorem addCommutatorElement_self {G : Type u_1} [AddGroup G] (g : G) : ⁅g, g⁆ = 0

@[simp]

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

@[simp]

theorem addCommutatorElement_neg {G : Type u_1} [AddGroup G] (g₁ g₂ : G) : -⁅g₁, g₂⁆ = ⁅g₂, g₁⁆

@[simp]

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) : f ⁅g₁, g₂⁆ = ⁅f g₁, f g₂⁆

@[simp]

theorem map_addCommutatorElement {G : Type u_1} {G' : Type u_2} {F : Type u_3} [AddGroup G] [AddGroup G'] [FunLike F G G'] [AddMonoidHomClass F G G'] (f : F) (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₃⁻¹⁆

theorem conjugate_addCommutatorElement {G : Type u_1} [AddGroup G] (g₁ g₂ g₃ : G) : g₃ + ⁅g₁, g₂⁆ + -g₃ = ⁅g₃ + g₁ + -g₃, g₃ + g₂ + -g₃⁆

theorem commutatorElement_mul_left_eq_conj_mul {G : Type u_1} [Group G] (a b c : G) : ⁅a * b, c⁆ = a * ⁅b, c⁆ * a⁻¹ * ⁅a, c⁆

theorem addCommutatorElement_add_left_eq_addConj_add {G : Type u_1} [AddGroup G] (a b c : G) : ⁅a + b, c⁆ = a + ⁅b, c⁆ + -a + ⁅a, c⁆

theorem commutatorElement_mul_right_eq_mul_conj {G : Type u_1} [Group G] (a b c : G) : ⁅a, b * c⁆ = ⁅a, b⁆ * b * ⁅a, c⁆ * b⁻¹

theorem addCommutatorElement_add_right_eq_add_addConj {G : Type u_1} [AddGroup G] (a b c : G) : ⁅a, b + c⁆ = ⁅a, b⁆ + b + ⁅a, c⁆ + -b

theorem commutatorElement_inv_left {G : Type u_1} [Group G] (a b : G) : ⁅a⁻¹, b⁆ = a⁻¹ * ⁅b, a⁆ * a

theorem addCommutatorElement_neg_left {G : Type u_1} [AddGroup G] (a b : G) : ⁅-a, b⁆ = -a + ⁅b, a⁆ + a

theorem commutatorElement_inv_right {G : Type u_1} [Group G] (a b : G) : ⁅a, b⁻¹⁆ = b⁻¹ * ⁅b, a⁆ * b

theorem addCommutatorElement_neg_right {G : Type u_1} [AddGroup G] (a b : G) : ⁅a, -b⁆ = -b + ⁅b, a⁆ + b

theorem conj_commutatorElement_left_commutatorElement_mul {G : Type u_1} [Group G] (a b c : G) : a * ⁅⁅a⁻¹, b⁆, c⁆ * a⁻¹ * c * ⁅⁅c⁻¹, a⁆, b⁆ * c⁻¹ * b * ⁅⁅b⁻¹, c⁆, a⁆ * b⁻¹ = 1

The Hall-Witt identity

theorem addConj_addCommutatorElement_left_addCommutatorElement_add {G : Type u_1} [AddGroup G] (a b c : G) : a + ⁅⁅-a, b⁆, c⁆ + -a + c + ⁅⁅-c, a⁆, b⁆ + -c + b + ⁅⁅-b, c⁆, a⁆ + -b = 0

The Hall-Witt identity

theorem conj_commutatorElement_right_commutatorElement_mul {G : Type u_1} [Group G] (a b c : G) : b * ⁅a, ⁅b⁻¹, c⁆⁆ * b⁻¹ * c * ⁅b, ⁅c⁻¹, a⁆⁆ * c⁻¹ * a * ⁅c, ⁅a⁻¹, b⁆⁆ * a⁻¹ = 1

The Hall-Witt identity

theorem addConj_addCommutatorElement_right_addCommutatorElement_add {G : Type u_1} [AddGroup G] (a b c : G) : b + ⁅a, ⁅-b, c⁆⁆ + -b + c + ⁅b, ⁅-c, a⁆⁆ + -c + a + ⁅c, ⁅-a, b⁆⁆ + -a = 0

The Hall-Witt identity

theorem commutatorElement_commutatorElement_conj_mul {G : Type u_1} [Group G] (a b c : G) : ⁅⁅a, b⁆, b * c * b⁻¹⁆ * ⁅⁅b, c⁆, c * a * c⁻¹⁆ * ⁅⁅c, a⁆, a * b * a⁻¹⁆ = 1

The Hall-Witt identity

theorem addCommutatorElement_addCommutatorElement_addConj_add {G : Type u_1} [AddGroup G] (a b c : G) : ⁅⁅a, b⁆, b + c + -b⁆ + ⁅⁅b, c⁆, c + a + -c⁆ + ⁅⁅c, a⁆, a + b + -a⁆ = 0

The Hall-Witt identity

theorem commutatorElement_conj_commutatorElement_mul {G : Type u_1} [Group G] (a b c : G) : ⁅a * b * a⁻¹, ⁅c, a⁆⁆ * ⁅c * a * c⁻¹, ⁅b, c⁆⁆ * ⁅b * c * b⁻¹, ⁅a, b⁆⁆ = 1

The Hall-Witt identity

theorem addCommutatorElement_addConj_addCommutatorElement_add {G : Type u_1} [AddGroup G] (a b c : G) : ⁅a + b + -a, ⁅c, a⁆⁆ + ⁅c + a + -c, ⁅b, c⁆⁆ + ⁅b + c + -b, ⁅a, b⁆⁆ = 0

The Hall-Witt identity

theorem commutatorElement_mul_left_mul {G : Type u_1} [Group G] (a b c : G) : ⁅a * b, c⁆ * ⁅c * a, b⁆ * ⁅b * c, a⁆ = 1

theorem addCommutatorElement_add_left_add {G : Type u_1} [AddGroup G] (a b c : G) : ⁅a + b, c⁆ + ⁅c + a, b⁆ + ⁅b + c, a⁆ = 0

theorem commutatorElement_mul_right_mul {G : Type u_1} [Group G] (a b c : G) : ⁅a, b * c⁆ * ⁅b, c * a⁆ * ⁅c, a * b⁆ = 1

theorem addCommutatorElement_add_right_add {G : Type u_1} [AddGroup G] (a b c : G) : ⁅a, b + c⁆ + ⁅b, c + a⁆ + ⁅c, a + b⁆ = 0

@[implicit_reducible]

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} }

@[implicit_reducible]

instance AddSubgroup.addCommutator {G : Type u_1} [AddGroup G] : Bracket (AddSubgroup G) (AddSubgroup G)

The commutator of two additive subgroups H₁ and H₂.

Equations

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

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

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

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

theorem AddSubgroup.addCommutator_mem_addCommutator {G : Type u_1} [AddGroup G] {g₁ g₂ : G} {H₁ H₂ : AddSubgroup G} (h₁ : g₁ ∈ H₁) (h₂ : g₂ ∈ H₂) : ⁅g₁, g₂⁆ ∈ ⁅H₁, H₂⁆

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

theorem AddSubgroup.addCommutator_le {G : Type u_1} [AddGroup G] {H₁ H₂ H₃ : AddSubgroup G} : ⁅H₁, H₂⁆ ≤ H₃ ↔ ∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅g₁, g₂⁆ ∈ H₃

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

theorem AddSubgroup.addCommutator_mono {G : Type u_1} [AddGroup G] {H₁ H₂ K₁ K₂ : AddSubgroup 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₁ H₂ : Subgroup G} : ⁅H₁, H₂⁆ = ⊥ ↔ H₁ ≤ centralizer ↑H₂

theorem AddSubgroup.addCommutator_eq_bot_iff_le_centralizer {G : Type u_1} [AddGroup G] {H₁ H₂ : AddSubgroup G} : ⁅H₁, H₂⁆ = ⊥ ↔ H₁ ≤ centralizer ↑H₂

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

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

theorem AddSubgroup.addCommutator_addCommutator_eq_bot_of_rotate {G : Type u_1} [AddGroup G] {H₁ H₂ H₃ : AddSubgroup 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₁ H₂ : Subgroup G) : ⁅H₁, H₂⁆ ≤ ⁅H₂, H₁⁆

theorem AddSubgroup.addCommutator_comm_le {G : Type u_1} [AddGroup G] (H₁ H₂ : AddSubgroup G) : ⁅H₁, H₂⁆ ≤ ⁅H₂, H₁⁆

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

theorem AddSubgroup.addCommutator_comm {G : Type u_1} [AddGroup G] (H₁ H₂ : AddSubgroup G) : ⁅H₁, H₂⁆ = ⁅H₂, H₁⁆

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

instance AddSubgroup.addCommutator_normal {G : Type u_1} [AddGroup G] (H₁ H₂ : AddSubgroup G) [h₁ : H₁.Normal] [h₂ : H₂.Normal] : ⁅H₁, H₂⁆.Normal

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

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

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

theorem AddSubgroup.addCommutator_le_right {G : Type u_1} [AddGroup G] (H₁ H₂ : AddSubgroup G) [h : H₂.Normal] : ⁅H₁, H₂⁆ ≤ H₂

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

theorem AddSubgroup.addCommutator_le_left {G : Type u_1} [AddGroup G] (H₁ H₂ : AddSubgroup G) [H₁.Normal] : ⁅H₁, H₂⁆ ≤ H₁

theorem Subgroup.commutator_top_left_le_iff {G : Type u_1} [Group G] {H : Subgroup G} : ⁅⊤, H⁆ ≤ H ↔ H.Normal

theorem AddSubgroup.addCommutator_top_left_le_iff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : ⁅⊤, H⁆ ≤ H ↔ H.Normal

theorem Subgroup.commutator_top_right_le_iff {G : Type u_1} [Group G] {H : Subgroup G} : ⁅H, ⊤⁆ ≤ H ↔ H.Normal

theorem AddSubgroup.addCommutator_top_right_le_iff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : ⁅H, ⊤⁆ ≤ H ↔ H.Normal

theorem Subgroup.le_normalizer_iff_commutator_le_right {G : Type u_1} [Group G] {H K : Subgroup G} : H ≤ normalizer ↑K ↔ ⁅H, K⁆ ≤ K

theorem AddSubgroup.le_normalizer_iff_addCommutator_le_right {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} : H ≤ normalizer ↑K ↔ ⁅H, K⁆ ≤ K

theorem Subgroup.le_normalizer_iff_commutator_le_left {G : Type u_1} [Group G] {H K : Subgroup G} : H ≤ normalizer ↑K ↔ ⁅K, H⁆ ≤ K

theorem AddSubgroup.le_normalizer_iff_addCommutator_le_left {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} : H ≤ normalizer ↑K ↔ ⁅K, H⁆ ≤ K

@[simp]

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

@[simp]

theorem AddSubgroup.addCommutator_bot_left {G : Type u_1} [AddGroup G] (H₁ : AddSubgroup G) : ⁅⊥, H₁⁆ = ⊥

@[simp]

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

@[simp]

theorem AddSubgroup.addCommutator_bot_right {G : Type u_1} [AddGroup G] (H₁ : AddSubgroup G) : ⁅H₁, ⊥⁆ = ⊥

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

theorem AddSubgroup.addCommutator_le_inf {G : Type u_1} [AddGroup G] (H₁ H₂ : AddSubgroup G) [H₁.Normal] [H₂.Normal] : ⁅H₁, H₂⁆ ≤ H₁ ⊓ H₂

theorem Subgroup.commutator_eq_bot_of_disjoint {G : Type u_1} [Group G] {H₁ H₂ : Subgroup G} [H₁.Normal] [H₂.Normal] (h : Disjoint H₁ H₂) : ⁅H₁, H₂⁆ = ⊥

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

theorem AddSubgroup.addCommutator_le_sup {G : Type u_1} [AddGroup G] (H₁ H₂ : AddSubgroup G) : ⁅H₁, H₂⁆ ≤ H₁ ⊔ H₂

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

theorem AddSubgroup.normalizer_addCommutator_ge_left {G : Type u_1} [AddGroup G] (H₁ H₂ : AddSubgroup G) : H₁ ≤ normalizer ↑⁅H₁, H₂⁆

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

theorem AddSubgroup.normalizer_addCommutator_ge_right {G : Type u_1} [AddGroup G] (H₁ H₂ : AddSubgroup G) : H₂ ≤ normalizer ↑⁅H₁, H₂⁆

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

instance AddSubgroup.normal_addSubgroupOf_addCommutator_sup {G : Type u_1} [AddGroup G] (H₁ H₂ : AddSubgroup G) : (⁅H₁, H₂⁆.addSubgroupOf (H₁ ⊔ H₂)).Normal

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

theorem AddSubgroup.map_addCommutator {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H₁ H₂ : AddSubgroup G) (f : G →+ G') : map f ⁅H₁, H₂⁆ = ⁅map f H₁, map f H₂⁆

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

theorem AddSubgroup.addCommutator_le_map_addCommutator {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] {H₁ H₂ : AddSubgroup G} {f : G →+ G'} {K₁ K₂ : AddSubgroup G'} (h₁ : K₁ ≤ map f H₁) (h₂ : K₂ ≤ map f H₂) : ⁅K₁, K₂⁆ ≤ map f ⁅H₁, H₂⁆

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

instance AddSubgroup.addCommutator_characteristic {G : Type u_1} [AddGroup G] (H₁ H₂ : AddSubgroup G) [h₁ : H₁.Characteristic] [h₂ : H₂.Characteristic] : ⁅H₁, H₂⁆.Characteristic

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

theorem AddSubgroup.addCommutator_sum_sum {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H₁ H₂ : AddSubgroup G) (K₁ K₂ : AddSubgroup G') : ⁅H₁.prod K₁, H₂.prod K₂⁆ = ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆

theorem Subgroup.commutator_pi_pi_le {η : Type u_4} {Gs : η → Type u_5} [(i : η) → Group (Gs i)] (H K : (i : η) → Subgroup (Gs i)) : ⁅pi Set.univ H, pi Set.univ K⁆ ≤ 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 AddSubgroup.addCommutator_pi_pi_le {η : Type u_4} {Gs : η → Type u_5} [(i : η) → AddGroup (Gs i)] (H K : (i : η) → AddSubgroup (Gs i)) : ⁅pi Set.univ H, pi Set.univ K⁆ ≤ 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 η.

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}

def addCommutatorSet (G : Type u_1) [AddGroup G] : Set G

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

Equations

• addCommutatorSet 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 addCommutatorSet_def (G : Type u_1) [AddGroup G] : addCommutatorSet G = {g : G | ∃ (g₁ : G) (g₂ : G), ⁅g₁, g₂⁆ = g}

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

theorem zero_mem_addCommutatorSet (G : Type u_1) [AddGroup G] : 0 ∈ addCommutatorSet G

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

instance instNonemptyElemAddCommutatorSet (G : Type u_1) [AddGroup G] : Nonempty ↑(addCommutatorSet G)

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

theorem mem_addCommutatorSet_iff {G : Type u_1} [AddGroup G] {g : G} : g ∈ addCommutatorSet G ↔ ∃ (g₁ : G) (g₂ : G), ⁅g₁, g₂⁆ = g

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

theorem addCommutator_mem_addCommutatorSet {G : Type u_1} [AddGroup G] (g₁ g₂ : G) : ⁅g₁, g₂⁆ ∈ addCommutatorSet G

def commutator (G : Type u_1) [Group G] : Subgroup G

The commutator subgroup of a group G is the normal subgroup generated by the commutators [p,q] = p * q * p⁻¹ * q⁻¹.

Equations

• commutator G = ⁅⊤, ⊤⁆

def addCommutator (G : Type u_1) [AddGroup G] : AddSubgroup G

The commutator subgroup of an additive group G is the normal additive subgroup generated by the additive commutators [p,q] = p + q + -p + -q.

Equations

• addCommutator G = ⁅⊤, ⊤⁆

instance instNormalCommutator (G : Type u_1) [Group G] : (commutator G).Normal

instance instCharacteristicCommutator (G : Type u_1) [Group G] : (commutator G).Characteristic

instance instNormalAddCommutator (G : Type u_1) [AddGroup G] : (addCommutator G).Normal

instance instCharacteristicAddCommutator (G : Type u_1) [AddGroup G] : (addCommutator G).Characteristic

theorem commutator_def (G : Type u_1) [Group G] : commutator G = ⁅⊤, ⊤⁆

theorem addCommutator_def (G : Type u_1) [AddGroup G] : addCommutator G = ⁅⊤, ⊤⁆

theorem commutator_eq_closure (G : Type u_1) [Group G] : commutator G = Subgroup.closure (commutatorSet G)

theorem addCommutator_eq_closure (G : Type u_1) [AddGroup G] : addCommutator G = AddSubgroup.closure (addCommutatorSet G)

theorem commutator_eq_normalClosure (G : Type u_1) [Group G] : commutator G = Subgroup.normalClosure (commutatorSet G)

theorem addCommutator_eq_normalClosure (G : Type u_1) [AddGroup G] : addCommutator G = AddSubgroup.normalClosure (addCommutatorSet G)

theorem Subgroup.map_subtype_commutator {G : Type u_1} [Group G] (H : Subgroup G) : map H.subtype (_root_.commutator ↥H) = ⁅H, H⁆

theorem AddSubgroup.map_subtype_addCommutator {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : map H.subtype (_root_.addCommutator ↥H) = ⁅H, H⁆

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

theorem AddSubgroup.addCommutator_le_self {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : ⁅H, H⁆ ≤ H

theorem Subgroup.Normal.of_commutator_le (G : Type u_1) [Group G] {H : Subgroup G} (h : _root_.commutator G ≤ H) : H.Normal

theorem AddSubgroup.Normal.of_addCommutator_le (G : Type u_1) [AddGroup G] {H : AddSubgroup G} (h : _root_.addCommutator G ≤ H) : H.Normal

theorem commutator_eq_bot_iff_center_eq_top (G : Type u_1) [Group G] : commutator G = ⊥ ↔ Subgroup.center G = ⊤

theorem addCommutator_eq_bot_iff_center_eq_top (G : Type u_1) [AddGroup G] : addCommutator G = ⊥ ↔ AddSubgroup.center G = ⊤

theorem commutator_eq_bot_iff (G : Type u_1) [Group G] : commutator G = ⊥ ↔ IsMulCommutative G

theorem addCommutator_eq_bot_iff (G : Type u_1) [AddGroup G] : addCommutator G = ⊥ ↔ IsAddCommutative G

theorem commutator_eq_bot (G : Type u_1) [Group G] [hG : IsMulCommutative G] : commutator G = ⊥

theorem addCommutator_eq_bot (G : Type u_1) [AddGroup G] [hG : IsAddCommutative G] : addCommutator G = ⊥

theorem commutator_centralizer_commutator_le_center (G : Type u_1) [Group G] : ⁅Subgroup.centralizer ↑(commutator G), Subgroup.centralizer ↑(commutator G)⁆ ≤ Subgroup.center G

theorem addCommutator_centralizer_addCommutator_le_center (G : Type u_1) [AddGroup G] : ⁅AddSubgroup.centralizer ↑(addCommutator G), AddSubgroup.centralizer ↑(addCommutator G)⁆ ≤ AddSubgroup.center G

theorem mem_commutatorSet_of_isConj_sq (G : Type u_1) [Group G] {g : G} (hg : IsConj g (g ^ 2)) : g ∈ commutatorSet G

If g is conjugate to g ^ 2, then g is a commutator

theorem mem_addCommutatorSet_of_isAddConj_sq (G : Type u_1) [AddGroup G] {g : G} (hg : IsAddConj g (2 • g)) : g ∈ addCommutatorSet G

If g is conjugate to 2 • g, then g is an additive commutator

theorem map_commutator_eq (G : Type u_1) [Group G] {H : Type u_4} [Group H] (f : G →* H) : Subgroup.map f (commutator G) = ⁅f.range, f.range⁆

theorem map_addCommutator_eq (G : Type u_1) [AddGroup G] {H : Type u_4} [AddGroup H] (f : G →+ H) : AddSubgroup.map f (addCommutator G) = ⁅f.range, f.range⁆

def commutatorRepresentatives (G : Type u_1) [Group G] : Set (G × G)

Representatives (g₁, g₂) : G × G of commutators ⁅g₁, g₂⁆ ∈ G.

Equations

• commutatorRepresentatives G = Set.range fun (g : ↑(commutatorSet G)) => (Exists.choose ⋯, ⋯.choose)

def addCommutatorRepresentatives (G : Type u_1) [AddGroup G] : Set (G × G)

Representatives (g₁, g₂) : G × G of additive commutators ⁅g₁, g₂⁆ ∈ G.

Equations

• addCommutatorRepresentatives G = Set.range fun (g : ↑(addCommutatorSet G)) => (Exists.choose ⋯, ⋯.choose)

def closureCommutatorRepresentatives (G : Type u_1) [Group G] : Subgroup G

Subgroup generated by representatives g₁ g₂ : G of commutators ⁅g₁, g₂⁆ ∈ G.

Equations

• closureCommutatorRepresentatives G = Subgroup.closure (Prod.fst '' commutatorRepresentatives G ∪ Prod.snd '' commutatorRepresentatives G)

def closureAddCommutatorRepresentatives (G : Type u_1) [AddGroup G] : AddSubgroup G

Additive subgroup generated by representatives g₁ g₂ : G of additive commutators ⁅g₁, g₂⁆ ∈ G.

Equations

• closureAddCommutatorRepresentatives G = AddSubgroup.closure (Prod.fst '' addCommutatorRepresentatives G ∪ Prod.snd '' addCommutatorRepresentatives G)

theorem image_commutatorSet_closureCommutatorRepresentatives (G : Type u_1) [Group G] : ⇑(closureCommutatorRepresentatives G).subtype '' commutatorSet ↥(closureCommutatorRepresentatives G) = commutatorSet G

theorem image_addCommutatorSet_closureAddCommutatorRepresentatives (G : Type u_1) [AddGroup G] : ⇑(closureAddCommutatorRepresentatives G).subtype '' addCommutatorSet ↥(closureAddCommutatorRepresentatives G) = addCommutatorSet G

theorem Subgroup.Normal.quotient_commutative_iff_commutator_le {G : Type u_1} [Group G] {N : Subgroup G} [N.Normal] : IsMulCommutative (G ⧸ N) ↔ _root_.commutator G ≤ N

theorem AddSubgroup.Normal.quotient_commutative_iff_addCommutator_le {G : Type u_1} [AddGroup G] {N : AddSubgroup G} [N.Normal] : IsAddCommutative (G ⧸ N) ↔ _root_.addCommutator G ≤ N

theorem Subgroup.Normal.commutator_le_of_self_sup_commutative_eq_top {G : Type u_1} [Group G] {N : Subgroup G} [N.Normal] {H : Subgroup G} (hHN : N ⊔ H = ⊤) (hH : IsMulCommutative ↥H) : _root_.commutator G ≤ N

If N is a normal subgroup of G and H a commutative subgroup such that H ⊔ N = ⊤, then N contains commutator G.

theorem AddSubgroup.Normal.addCommutator_le_of_self_sup_commutative_eq_top {G : Type u_1} [AddGroup G] {N : AddSubgroup G} [N.Normal] {H : AddSubgroup G} (hHN : N ⊔ H = ⊤) (hH : IsAddCommutative ↥H) : _root_.addCommutator G ≤ N

If N is a normal additive subgroup of G and H a commutative additive subgroup such that H ⊔ N = ⊤, then N contains addCommutator G.