# mathlibdocumentation

group_theory.commutator

# 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 commutator_element elsewhere).
• ⁅H₁, H₂⁆ : the commutator of the subgroups H₁ and H₂.
theorem commutator_element_eq_one_iff_mul_comm {G : Type u_1} [group G] {g₁ g₂ : G} :
g₁,g₂ = 1 g₁ * g₂ = g₂ * g₁
theorem commutator_element_eq_one_iff_commute {G : Type u_1} [group G] {g₁ g₂ : G} :
g₁,g₂ = 1 commute g₁ g₂
theorem commute.commutator_eq {G : Type u_1} [group G] {g₁ g₂ : G} (h : commute g₁ g₂) :
g₁,g₂ = 1
@[simp]
theorem commutator_element_one_right {G : Type u_1} [group G] (g : G) :
@[simp]
theorem commutator_element_one_left {G : Type u_1} [group G] (g : G) :
@[simp]
theorem commutator_element_inv {G : Type u_1} [group G] (g₁ g₂ : G) :
g₁,g₂⁻¹ = g₂,g₁
theorem map_commutator_element {G : Type u_1} {G' : Type u_2} {F : Type u_3} [group G] [group G'] [ G'] (f : F) (g₁ g₂ : G) :
f g₁,g₂ = f g₁,f g₂
theorem conjugate_commutator_element {G : Type u_1} [group G] (g₁ g₂ g₃ : G) :
g₃ * g₁,g₂ * g₃⁻¹ = g₃ * g₁ * g₃⁻¹,g₃ * g₂ * g₃⁻¹
@[protected, instance]
def subgroup.commutator {G : Type u_1} [group G] :

The commutator of two subgroups H₁ and H₂.

Equations
theorem subgroup.commutator_def {G : Type u_1} [group G] (H₁ H₂ : subgroup G) :
H₁,H₂ = subgroup.closure {g : G | ∃ (g₁ : G) (H : g₁ H₁) (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 subgroup.commutator_le {G : Type u_1} [group G] {H₁ H₂ H₃ : subgroup G} :
H₁,H₂ H₃ ∀ (g₁ : G), g₁ H₁∀ (g₂ : G), 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 subgroup.commutator_eq_bot_iff_le_centralizer {G : Type u_1} [group G] {H₁ H₂ : subgroup G} :
H₁,H₂ = H₁ H₂.centralizer
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 subgroup.commutator_comm_le {G : Type u_1} [group G] (H₁ H₂ : subgroup G) :
H₁,H₂ H₂,H₁
theorem subgroup.commutator_comm {G : Type u_1} [group G] (H₁ H₂ : subgroup G) :
H₁,H₂ = H₂,H₁
@[protected, instance]
def subgroup.commutator_normal {G : Type u_1} [group G] (H₁ H₂ : subgroup 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₂ = subgroup.normal_closure {g : G | ∃ (g₁ : G) (H : g₁ H₁) (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 subgroup.commutator_le_left {G : Type u_1} [group G] (H₁ H₂ : subgroup G) [H₁.normal] :
H₁,H₂ H₁
@[simp]
theorem subgroup.commutator_bot_left {G : Type u_1} [group G] (H₁ : subgroup G) :
@[simp]
theorem subgroup.commutator_bot_right {G : Type u_1} [group G] (H₁ : subgroup G) :
theorem subgroup.commutator_le_inf {G : Type u_1} [group G] (H₁ H₂ : subgroup G) [H₁.normal] [H₂.normal] :
H₁,H₂ H₁ H₂
theorem subgroup.map_commutator {G : Type u_1} {G' : Type u_2} [group G] [group G'] (H₁ H₂ : subgroup G) (f : G →* G') :
H₁,H₂ = H₁, 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₁ H₁) (h₂ : K₂ H₂) :
K₁,K₂ H₁,H₂
@[protected, instance]
def subgroup.commutator_characteristic {G : Type u_1} [group G] (H₁ H₂ : subgroup G) [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 subgroup.commutator_pi_pi_le {η : Type u_1} {Gs : η → Type u_2} [Π (i : η), group (Gs i)] (H K : Π (i : η), subgroup (Gs i)) :
(λ (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_1} [finite η] {Gs : η → Type u_2} [Π (i : η), group (Gs i)] (H K : Π (i : η), subgroup (Gs i)) :
= (λ (i : η), H i,K i)

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