Documentation

Mathlib.GroupTheory.Commutator.Basic

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 #

theorem commutatorElement_eq_one_iff_mul_comm {G : Type u_1} [Group G] {g₁ : G} {g₂ : G} :
g₁, g₂ = 1 g₁ * g₂ = g₂ * g₁
theorem commutatorElement_eq_one_iff_commute {G : Type u_1} [Group G] {g₁ : G} {g₂ : G} :
g₁, g₂ = 1 Commute g₁ g₂
theorem Commute.commutator_eq {G : Type u_1} [Group G] {g₁ : G} {g₂ : G} (h : Commute g₁ g₂) :
g₁, g₂ = 1
@[simp]
theorem commutatorElement_one_right {G : Type u_1} [Group G] (g : G) :
g, 1 = 1
@[simp]
theorem commutatorElement_one_left {G : Type u_1} [Group G] (g : G) :
1, g = 1
@[simp]
theorem commutatorElement_self {G : Type u_1} [Group G] (g : G) :
g, g = 1
@[simp]
theorem commutatorElement_inv {G : Type u_1} [Group G] (g₁ : G) (g₂ : G) :
g₁, g₂⁻¹ = g₂, g₁
theorem map_commutatorElement {G : Type u_1} {G' : Type u_2} {F : Type u_3} [Group G] [Group G'] [FunLike F G G'] [MonoidHomClass F G G'] (f : F) (g₁ : G) (g₂ : G) :
f g₁, g₂ = f g₁, f g₂
theorem conjugate_commutatorElement {G : Type u_1} [Group G] (g₁ : G) (g₂ : G) (g₃ : G) :
g₃ * g₁, g₂ * g₃⁻¹ = g₃ * g₁ * g₃⁻¹, g₃ * g₂ * g₃⁻¹
instance 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₁ : Subgroup G) (H₂ : Subgroup G) :
H₁, H₂ = Subgroup.closure {g : G | g₁H₁, g₂H₂, g₁, g₂ = g}
theorem Subgroup.commutator_mem_commutator {G : Type u_1} [Group G] {g₁ : G} {g₂ : G} {H₁ : Subgroup G} {H₂ : Subgroup G} (h₁ : g₁ H₁) (h₂ : g₂ H₂) :
g₁, g₂ H₁, H₂
theorem Subgroup.commutator_le {G : Type u_1} [Group G] {H₁ : Subgroup G} {H₂ : Subgroup G} {H₃ : Subgroup G} :
H₁, H₂ H₃ g₁H₁, g₂H₂, g₁, g₂ H₃
theorem Subgroup.commutator_mono {G : Type u_1} [Group G] {H₁ : Subgroup G} {H₂ : Subgroup G} {K₁ : Subgroup G} {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₁ : Subgroup G} {H₂ : Subgroup G} :
H₁, H₂ = H₁ Subgroup.centralizer H₂
theorem Subgroup.commutator_commutator_eq_bot_of_rotate {G : Type u_1} [Group G] {H₁ : Subgroup G} {H₂ : Subgroup G} {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₁ : Subgroup G) (H₂ : Subgroup G) :
H₁, H₂ H₂, H₁
theorem Subgroup.commutator_comm {G : Type u_1} [Group G] (H₁ : Subgroup G) (H₂ : Subgroup G) :
H₁, H₂ = H₂, H₁
instance Subgroup.commutator_normal {G : Type u_1} [Group G] (H₁ : Subgroup G) (H₂ : Subgroup G) [h₁ : H₁.Normal] [h₂ : H₂.Normal] :
H₁, H₂.Normal
Equations
  • =
theorem Subgroup.commutator_def' {G : Type u_1} [Group G] (H₁ : Subgroup G) (H₂ : Subgroup G) [H₁.Normal] [H₂.Normal] :
H₁, H₂ = Subgroup.normalClosure {g : G | g₁H₁, g₂H₂, g₁, g₂ = g}
theorem Subgroup.commutator_le_right {G : Type u_1} [Group G] (H₁ : Subgroup G) (H₂ : Subgroup G) [h : H₂.Normal] :
H₁, H₂ H₂
theorem Subgroup.commutator_le_left {G : Type u_1} [Group G] (H₁ : Subgroup G) (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₁ : Subgroup G) (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₁ : Subgroup G) (H₂ : Subgroup G) (f : G →* G') :
theorem Subgroup.commutator_le_map_commutator {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {H₁ : Subgroup G} {H₂ : Subgroup G} {f : G →* G'} {K₁ : Subgroup G'} {K₂ : Subgroup G'} (h₁ : K₁ Subgroup.map f H₁) (h₂ : K₂ Subgroup.map f H₂) :
K₁, K₂ Subgroup.map f H₁, H₂
instance Subgroup.commutator_characteristic {G : Type u_1} [Group G] (H₁ : Subgroup G) (H₂ : Subgroup G) [h₁ : H₁.Characteristic] [h₂ : H₂.Characteristic] :
H₁, H₂.Characteristic
Equations
  • =
theorem Subgroup.commutator_prod_prod {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H₁ : Subgroup G) (H₂ : Subgroup G) (K₁ : Subgroup G') (K₂ : Subgroup G') :
H₁.prod K₁, H₂.prod K₂ = H₁, H₂.prod K₁, K₂
theorem Subgroup.commutator_pi_pi_le {η : Type u_4} {Gs : ηType u_5} [(i : η) → Group (Gs i)] (H : (i : η) → Subgroup (Gs i)) (K : (i : η) → Subgroup (Gs i)) :
Subgroup.pi Set.univ H, Subgroup.pi Set.univ K Subgroup.pi Set.univ fun (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 η.

def commutatorSet (G : Type u_1) [Group G] :
Set G

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

Equations
Instances For
    theorem commutatorSet_def (G : Type u_1) [Group G] :
    commutatorSet G = {g : G | ∃ (g₁ : G) (g₂ : G), g₁, g₂ = g}
    Equations
    • =
    theorem mem_commutatorSet_iff {G : Type u_1} [Group G] {g : G} :
    g commutatorSet G ∃ (g₁ : G) (g₂ : G), g₁, g₂ = g
    theorem commutator_mem_commutatorSet {G : Type u_1} [Group G] (g₁ : G) (g₂ : G) :