mathlib documentation

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 #

source
@[protected, instance]
def general_commutator {G : Type u_1} [group G] :
has_bracket (subgroup G) (subgroup G)

The commutator of two subgroups H₁ and H₂.

Equations
source
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}
source
@[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
source
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₂⁆
source
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}
source
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
source
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₂⁆
source
theorem general_commutator_comm {G : Type u_1} [group G] (H₁ H₂ : subgroup G) :
⁅H₁,H₂⁆ = ⁅H₂,H₁⁆
source
theorem general_commutator_le_right {G : Type u_1} [group G] (H₁ H₂ : subgroup G) [h : H₂.normal] :
⁅H₁,H₂⁆ ≤ H₂
source
theorem general_commutator_le_left {G : Type u_1} [group G] (H₁ H₂ : subgroup G) [h : H₁.normal] :
⁅H₁,H₂⁆ ≤ H₁
source
@[simp]
theorem general_commutator_bot {G : Type u_1} [group G] (H : subgroup G) :
⁅H,⊥⁆ = ⊥
source
@[simp]
theorem bot_general_commutator {G : Type u_1} [group G] (H : subgroup G) :
⁅⊥,H⁆ = ⊥
source
theorem general_commutator_le_inf {G : Type u_1} [group G] (H₁ H₂ : subgroup G) [H₁.normal] [H₂.normal] :
⁅H₁,H₂⁆ ≤ H₁ ⊓ H₂
source
theorem map_general_commutator {G : Type u_1} [group G] {G₂ : Type u_2} [group G₂] (f : G →* G₂) (H₁ H₂ : subgroup G) :
subgroup.map f ⁅H₁,H₂⁆ = ⁅subgroup.map f H₁,subgroup.map f H₂⁆
source
theorem general_commutator_prod_prod {G : Type u_1} [group G] {G₂ : Type u_2} [group G₂] (H₁ K₁ : subgroup G) (H₂ K₂ : subgroup G₂) :
⁅H₁.prod H₂,K₁.prod K₂⁆ = ⁅H₁,K₁⁆.prod ⁅H₂,K₂⁆