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

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_self {G : Type u_1} [group G] (g : G) :

⁅g, 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₁ ≤ subgroup.centralizer ↑H₂

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_finite for equality given fintype η.

source

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)) :