# mathlibdocumentation

group_theory.general_commutator

# General commutators. #

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

## Main definitions #

• general_commutator H₁ H₂ : the commutator of the subgroups H₁ and H₂
@[protected, instance]
def general_commutator {G : Type u_1} [group G] :

The commutator of two subgroups H₁ and H₂.

Equations
theorem general_commutator_def {G : Type u_1} [group G] (H₁ H₂ : subgroup G) :
H₁,H₂ = subgroup.closure {x : G | ∃ (p : G) (H : p H₁) (q : G) (H : q H₂), ((p * q) * p⁻¹) * q⁻¹ = x}
@[protected, instance]
def general_commutator_normal {G : Type u_1} [group G] (H₁ H₂ : subgroup G) [h₁ : H₁.normal] [h₂ : H₂.normal] :
H₁,H₂.normal
theorem general_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 general_commutator_def' {G : Type u_1} [group G] (H₁ H₂ : subgroup G) [H₁.normal] [H₂.normal] :
H₁,H₂ = subgroup.normal_closure {x : G | ∃ (p : G) (H : p H₁) (q : G) (H : q H₂), ((p * q) * p⁻¹) * q⁻¹ = x}
theorem general_commutator_le {G : Type u_1} [group G] (H₁ H₂ K : subgroup G) :
H₁,H₂ K ∀ (p : G), p H₁∀ (q : G), q H₂((p * q) * p⁻¹) * q⁻¹ K
theorem general_commutator_containment {G : Type u_1} [group G] (H₁ H₂ : subgroup G) {p q : G} (hp : p H₁) (hq : q H₂) :
((p * q) * p⁻¹) * q⁻¹ H₁,H₂
theorem general_commutator_comm {G : Type u_1} [group G] (H₁ H₂ : subgroup G) :
H₁,H₂ = H₂,H₁
theorem general_commutator_le_right {G : Type u_1} [group G] (H₁ H₂ : subgroup G) [h : H₂.normal] :
H₁,H₂ H₂
theorem general_commutator_le_left {G : Type u_1} [group G] (H₁ H₂ : subgroup G) [h : H₁.normal] :
H₁,H₂ H₁
@[simp]
theorem general_commutator_bot {G : Type u_1} [group G] (H : subgroup G) :
@[simp]
theorem bot_general_commutator {G : Type u_1} [group G] (H : subgroup G) :
theorem general_commutator_le_inf {G : Type u_1} [group G] (H₁ H₂ : subgroup G) [H₁.normal] [H₂.normal] :
H₁,H₂ H₁ H₂