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₂.

source

theorem commutator_element_eq_one_iff_mul_comm {G : Type u_1} [group G] {g₁ g₂ : G} :

⁅g₁,g₂⁆ = 1 ↔ g₁ * g₂ = g₂ * g₁

source

theorem commutator_element_eq_one_iff_commute {G : Type u_1} [group G] {g₁ g₂ : G} :

⁅g₁,g₂⁆ = 1 ↔ commute g₁ g₂

source

theorem commute.commutator_eq {G : Type u_1} [group G] {g₁ g₂ : G} (h : commute g₁ g₂) :

⁅g₁,g₂⁆ = 1

source

@[simp]

theorem commutator_element_one_right {G : Type u_1} [group G] (g : G) :

⁅g,1⁆ = 1

source

@[simp]

theorem commutator_element_one_left {G : Type u_1} [group G] (g : G) :

⁅1,g⁆ = 1

source

@[simp]

theorem commutator_element_inv {G : Type u_1} [group G] (g₁ g₂ : G) :

⁅g₁,g₂⁆⁻¹ = ⁅g₂,g₁⁆

source

theorem map_commutator_element {G : Type u_1} {G' : Type u_2} {F : Type u_3} [group G] [group G'] [monoid_hom_class F G G'] (f : F) (g₁ g₂ : G) :

⇑f ⁅g₁,g₂⁆ = ⁅⇑f g₁,⇑f g₂⁆

source

theorem conjugate_commutator_element {G : Type u_1} [group G] (g₁ g₂ g₃ : G) :

(g₃ * ⁅g₁,g₂⁆) * g₃⁻¹ = ⁅(g₃ * g₁) * g₃⁻¹,(g₃ * g₂) * g₃⁻¹⁆

source

@[protected, instance]

def subgroup.commutator {G : Type u_1} [group G] :

has_bracket (subgroup G) (subgroup G)

The commutator of two subgroups H₁ and H₂.

Equations

subgroup.commutator = {bracket := λ (H₁ H₂ : subgroup G), subgroup.closure {g : G | ∃ (g₁ : G) (H : g₁ ∈ H₁) (g₂ : G) (H : g₂ ∈ H₂), ⁅g₁,g₂⁆ = g}}

source

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}

source

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₂⁆

source

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₃

source

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₂⁆

source

theorem subgroup.commutator_eq_bot_iff_le_centralizer {G : Type u_1} [group G] {H₁ H₂ : subgroup G} :

⁅H₁,H₂⁆ = ⊥ ↔ H₁ ≤ H₂.centralizer

source

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)

source

theorem subgroup.commutator_comm_le {G : Type u_1} [group G] (H₁ H₂ : subgroup G) :

⁅H₁,H₂⁆ ≤ ⁅H₂,H₁⁆

source

theorem subgroup.commutator_comm {G : Type u_1} [group G] (H₁ H₂ : subgroup G) :

⁅H₁,H₂⁆ = ⁅H₂,H₁⁆

source

@[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

source

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}

source

theorem subgroup.commutator_le_right {G : Type u_1} [group G] (H₁ H₂ : subgroup G) [h : H₂.normal] :

⁅H₁,H₂⁆ ≤ H₂

source

theorem subgroup.commutator_le_left {G : Type u_1} [group G] (H₁ H₂ : subgroup G) [H₁.normal] :

⁅H₁,H₂⁆ ≤ H₁

source

@[simp]

theorem subgroup.commutator_bot_left {G : Type u_1} [group G] (H₁ : subgroup G) :

⁅⊥,H₁⁆ = ⊥

source

@[simp]

theorem subgroup.commutator_bot_right {G : Type u_1} [group G] (H₁ : subgroup G) :

⁅H₁,⊥⁆ = ⊥

source

theorem subgroup.commutator_le_inf {G : Type u_1} [group G] (H₁ H₂ : subgroup G) [H₁.normal] [H₂.normal] :

⁅H₁,H₂⁆ ≤ H₁ ⊓ H₂

source

theorem subgroup.map_commutator {G : Type u_1} {G' : Type u_2} [group G] [group G'] (H₁ H₂ : subgroup G) (f : G →* G') :

subgroup.map f ⁅H₁,H₂⁆ = ⁅subgroup.map f H₁,subgroup.map f H₂⁆

source

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₁ ≤ subgroup.map f H₁) (h₂ : K₂ ≤ subgroup.map f H₂) :

⁅K₁,K₂⁆ ≤ subgroup.map f ⁅H₁,H₂⁆

source

@[protected, instance]

def subgroup.commutator_characteristic {G : Type u_1} [group G] (H₁ H₂ : subgroup G) [h₁ : H₁.characteristic] [h₂ : H₂.characteristic] :

⁅H₁,H₂⁆.characteristic

source

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₂⁆

source

theorem subgroup.commutator_pi_pi_le {η : Type u_1} {Gs : η → Type u_2} [Π (i : η), group (Gs i)] (H K : Π (i : η), subgroup (Gs i)) :

⁅subgroup.pi set.univ H,subgroup.pi set.univ K⁆ ≤ subgroup.pi set.univ (λ (i : η), ⁅H i,K i⁆)

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

See commutator_pi_pi_of_fintype for equality given fintype η.

source

theorem subgroup.commutator_pi_pi_of_fintype {η : Type u_1} [fintype η] {Gs : η → Type u_2} [Π (i : η), group (Gs i)] (H K : Π (i : η), subgroup (Gs i)) :

⁅subgroup.pi set.univ H,subgroup.pi set.univ K⁆ = subgroup.pi set.univ (λ (i : η), ⁅H i,K i⁆)

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