mathlib3documentation

group_theory.commutator

Commutators of Subgroups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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) :
g, 1 = 1
@[simp]
theorem commutator_element_one_left {G : Type u_1} [group G] (g : G) :
1, g = 1
@[simp]
theorem commutator_element_self {G : Type u_1} [group G] (g : G) :
g, g = 1
@[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₂ =
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.

def commutator_set (G : Type u_1) [group G] :
set G

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

Equations
Instances for ↥commutator_set
theorem commutator_set_def (G : Type u_1) [group G] :
= {g : G | (g₁ g₂ : G), g₁, g₂ = g}
theorem one_mem_commutator_set (G : Type u_1) [group G] :
@[protected, instance]
def commutator_set.nonempty (G : Type u_1) [group G] :
theorem mem_commutator_set_iff {G : Type u_1} [group G] {g : G} :
(g₁ g₂ : G), g₁, g₂ = g
theorem commutator_mem_commutator_set {G : Type u_1} [group G] (g₁ g₂ : G) :
g₁, g₂