doc-next-gen

Mathlib.GroupTheory.Commutator.Basic

Module docstring

{"# 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 commutatorElement elsewhere).
  • ⁅H₁, H₂⁆ : the commutator of the subgroups H₁ and H₂. "}
commutatorElement_eq_one_iff_mul_comm theorem
: ⁅g₁, g₂⁆ = 1 ↔ g₁ * g₂ = g₂ * g₁
Full source 
theorem commutatorElement_eq_one_iff_mul_comm : ⁅g₁, g₂⁆⁅g₁, g₂⁆ = 1 ↔ g₁ * g₂ = g₂ * g₁ := by
  rw [commutatorElement_def, mul_inv_eq_one, mul_inv_eq_iff_eq_mul]
Commutator Equals Identity iff Elements Commute: $\lbrack g_1, g_2 \rbrack = 1 \leftrightarrow g_1 g_2 = g_2 g_1$
Informal description
For any two elements $g_1$ and $g_2$ in a group $G$, the commutator $\lbrack g_1, g_2 \rbrack$ equals the identity element $1$ if and only if $g_1$ and $g_2$ commute, i.e., $g_1 g_2 = g_2 g_1$.
commutatorElement_eq_one_iff_commute theorem
: ⁅g₁, g₂⁆ = 1 ↔ Commute g₁ g₂
Full source 
theorem commutatorElement_eq_one_iff_commute : ⁅g₁, g₂⁆⁅g₁, g₂⁆ = 1 ↔ Commute g₁ g₂ :=
  commutatorElement_eq_one_iff_mul_comm
Commutator Vanishes iff Elements Commute: $\lbrack g_1, g_2 \rbrack = 1 \leftrightarrow g_1$ and $g_2$ commute
Informal description
For any two elements $g_1$ and $g_2$ in a group $G$, the commutator $\lbrack g_1, g_2 \rbrack$ equals the identity element $1$ if and only if $g_1$ and $g_2$ commute.
Commute.commutator_eq theorem
(h : Commute g₁ g₂) : ⁅g₁, g₂⁆ = 1
Full source 
theorem Commute.commutator_eq (h : Commute g₁ g₂) : ⁅g₁, g₂⁆ = 1 :=
  commutatorElement_eq_one_iff_commute.mpr h
Commutator Vanishes for Commuting Elements: $\lbrack g_1, g_2 \rbrack = 1$ when $g_1$ and $g_2$ commute
Informal description
If two elements $g_1$ and $g_2$ in a group $G$ commute, then their commutator $\lbrack g_1, g_2 \rbrack$ is equal to the identity element $1$.
commutatorElement_one_right theorem
: ⁅g, (1 : G)⁆ = 1
Full source 
@[simp]
theorem commutatorElement_one_right : ⁅g, (1 : G)⁆ = 1 :=
  (Commute.one_right g).commutator_eq
Commutator with Identity Vanishes: $\lbrack g, 1 \rbrack = 1$
Informal description
For any element $g$ in a group $G$, the commutator of $g$ with the identity element $1$ is equal to $1$, i.e., $\lbrack g, 1 \rbrack = 1$.
commutatorElement_one_left theorem
: ⁅(1 : G), g⁆ = 1
Full source 
@[simp]
theorem commutatorElement_one_left : ⁅(1 : G), g⁆ = 1 :=
  (Commute.one_left g).commutator_eq
Commutator with Identity on the Left is Trivial
Informal description
For any element $g$ in a group $G$, the commutator of the identity element $1$ and $g$ is equal to $1$, i.e., $\lbrack 1, g \rbrack = 1$.
commutatorElement_self theorem
: ⁅g, g⁆ = 1
Full source 
@[simp]
theorem commutatorElement_self : ⁅g, g⁆ = 1 :=
  (Commute.refl g).commutator_eq
Commutator of an Element with Itself Vanishes: $\lbrack g, g \rbrack = 1$
Informal description
For any element $g$ in a group $G$, the commutator $\lbrack g, g \rbrack$ is equal to the identity element $1$.
commutatorElement_inv theorem
: ⁅g₁, g₂⁆⁻¹ = ⁅g₂, g₁⁆
Full source 
@[simp]
theorem commutatorElement_inv : ⁅g₁, g₂⁆⁅g₁, g₂⁆⁻¹ = ⁅g₂, g₁⁆ := by
  simp_rw [commutatorElement_def, mul_inv_rev, inv_inv, mul_assoc]
Inverse of Commutator Equals Swapped Commutator
Informal description
For any elements $g_1, g_2$ in a group $G$, the inverse of their commutator $\lbrack g_1, g_2 \rbrack$ is equal to the commutator $\lbrack g_2, g_1 \rbrack$, i.e., \[ \lbrack g_1, g_2 \rbrack^{-1} = \lbrack g_2, g_1 \rbrack. \]
map_commutatorElement theorem
: (f ⁅g₁, g₂⁆ : G') = ⁅f g₁, f g₂⁆
Full source 
theorem map_commutatorElement : (f ⁅g₁, g₂⁆ : G') = ⁅f g₁, f g₂⁆ := by
  simp_rw [commutatorElement_def, map_mul f, map_inv f]
Homomorphism Preserves Commutator: $f(\lbrack g_1, g_2 \rbrack) = \lbrack f(g_1), f(g_2) \rbrack$
Informal description
For any group homomorphism $f \colon G \to G'$ and any elements $g_1, g_2 \in G$, the image of the commutator $\lbrack g_1, g_2 \rbrack$ under $f$ is equal to the commutator of the images, i.e., \[ f(\lbrack g_1, g_2 \rbrack) = \lbrack f(g_1), f(g_2) \rbrack. \]
conjugate_commutatorElement theorem
: g₃ * ⁅g₁, g₂⁆ * g₃⁻¹ = ⁅g₃ * g₁ * g₃⁻¹, g₃ * g₂ * g₃⁻¹⁆
Full source 
theorem conjugate_commutatorElement : g₃ * ⁅g₁, g₂⁆ * g₃⁻¹ = ⁅g₃ * g₁ * g₃⁻¹, g₃ * g₂ * g₃⁻¹⁆ :=
  map_commutatorElement (MulAut.conj g₃).toMonoidHom g₁ g₂
Conjugation of Commutator Equals Commutator of Conjugates
Informal description
For any elements $g_1, g_2, g_3$ in a group $G$, the conjugate of the commutator $\lbrack g_1, g_2 \rbrack$ by $g_3$ is equal to the commutator of the conjugates of $g_1$ and $g_2$ by $g_3$, i.e., \[ g_3 \lbrack g_1, g_2 \rbrack g_3^{-1} = \lbrack g_3 g_1 g_3^{-1}, g_3 g_2 g_3^{-1} \rbrack. \]
Subgroup.commutator instance
: Bracket (Subgroup G) (Subgroup G)
Full source 
/-- The commutator of two subgroups `H₁` and `H₂`. -/
instance commutator : Bracket (Subgroup G) (Subgroup G) :=
  ⟨fun H₁ H₂ => closure { g | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g }⟩
Commutator Subgroup of Two Subgroups
Informal description
For any group $G$ and subgroups $H_1, H_2$ of $G$, the commutator subgroup $\lbrack H_1, H_2 \rbrack$ is the subgroup of $G$ generated by all commutators $\lbrack h_1, h_2 \rbrack = h_1 h_2 h_1^{-1} h_2^{-1}$ where $h_1 \in H_1$ and $h_2 \in H_2$.
Subgroup.commutator_def theorem
(H₁ H₂ : Subgroup G) : ⁅H₁, H₂⁆ = closure {g | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g}
Full source 
theorem commutator_def (H₁ H₂ : Subgroup G) :
    ⁅H₁, H₂⁆ = closure { g | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g } :=
  rfl
Definition of Commutator Subgroup as Generated Set of Commutators
Informal description
For any group $G$ and subgroups $H_1, H_2$ of $G$, the commutator subgroup $\lbrack H_1, H_2 \rbrack$ is equal to the subgroup generated by the set of all elements $g \in G$ for which there exist $g_1 \in H_1$ and $g_2 \in H_2$ such that the commutator $\lbrack g_1, g_2 \rbrack = g_1 g_2 g_1^{-1} g_2^{-1}$ equals $g$.
Subgroup.commutator_mem_commutator theorem
(h₁ : g₁ ∈ H₁) (h₂ : g₂ ∈ H₂) : ⁅g₁, g₂⁆ ∈ ⁅H₁, H₂⁆
Full source 
theorem commutator_mem_commutator (h₁ : g₁ ∈ H₁) (h₂ : g₂ ∈ H₂) : ⁅g₁, g₂⁆⁅g₁, g₂⁆ ∈ ⁅H₁, H₂⁆ :=
  subset_closure ⟨g₁, h₁, g₂, h₂, rfl⟩
Commutator of Elements Lies in Commutator Subgroup
Informal description
For any group $G$ with subgroups $H_1, H_2$, if $g_1 \in H_1$ and $g_2 \in H_2$, then the commutator $\lbrack g_1, g_2 \rbrack = g_1 g_2 g_1^{-1} g_2^{-1}$ belongs to the commutator subgroup $\lbrack H_1, H_2 \rbrack$.
Subgroup.commutator_le theorem
: ⁅H₁, H₂⁆ ≤ H₃ ↔ ∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅g₁, g₂⁆ ∈ H₃
Full source 
theorem commutator_le : ⁅H₁, H₂⁆⁅H₁, H₂⁆ ≤ H₃ ↔ ∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅g₁, g₂⁆ ∈ H₃ :=
  H₃.closure_le.trans
    ⟨fun h a b c d => h ⟨a, b, c, d, rfl⟩, fun h _g ⟨a, b, c, d, h_eq⟩ => h_eq ▸ h a b c d⟩
Characterization of Commutator Subgroup Containment: $\lbrack H_1, H_2 \rbrack \leq H_3 \leftrightarrow \forall g_1 \in H_1, \forall g_2 \in H_2, \lbrack g_1, g_2 \rbrack \in H_3$
Informal description
For any group $G$ with subgroups $H_1, H_2, H_3$, the commutator subgroup $\lbrack H_1, H_2 \rbrack$ is contained in $H_3$ if and only if for all $g_1 \in H_1$ and $g_2 \in H_2$, the commutator element $\lbrack g_1, g_2 \rbrack$ belongs to $H_3$.
Subgroup.commutator_mono theorem
(h₁ : H₁ ≤ K₁) (h₂ : H₂ ≤ K₂) : ⁅H₁, H₂⁆ ≤ ⁅K₁, K₂⁆
Full source 
theorem commutator_mono (h₁ : H₁ ≤ K₁) (h₂ : H₂ ≤ K₂) : ⁅H₁, H₂⁆ ≤ ⁅K₁, K₂⁆ :=
  commutator_le.mpr fun _g₁ hg₁ _g₂ hg₂ => commutator_mem_commutator (h₁ hg₁) (h₂ hg₂)
Monotonicity of Commutator Subgroups: $\lbrack H_1, H_2 \rbrack \leq \lbrack K_1, K_2 \rbrack$ when $H_1 \leq K_1$ and $H_2 \leq K_2$
Informal description
For any group $G$ with subgroups $H_1, H_2, K_1, K_2$ such that $H_1 \leq K_1$ and $H_2 \leq K_2$, the commutator subgroup $\lbrack H_1, H_2 \rbrack$ is contained in $\lbrack K_1, K_2 \rbrack$.
Subgroup.commutator_eq_bot_iff_le_centralizer theorem
: ⁅H₁, H₂⁆ = ⊥ ↔ H₁ ≤ centralizer H₂
Full source 
theorem commutator_eq_bot_iff_le_centralizer : ⁅H₁, H₂⁆⁅H₁, H₂⁆ = ⊥ ↔ H₁ ≤ centralizer H₂ := by
  rw [eq_bot_iff, commutator_le]
  refine forall_congr' fun p =>
    forall_congr' fun _hp => forall_congr' fun q => forall_congr' fun hq => ?_
  rw [mem_bot, commutatorElement_eq_one_iff_mul_comm, eq_comm]
Triviality of Commutator Subgroup iff Subgroup Centralizes Another: $\lbrack H_1, H_2 \rbrack = 1 \leftrightarrow H_1 \leq C_G(H_2)$
Informal description
For any group $G$ with subgroups $H_1$ and $H_2$, the commutator subgroup $\lbrack H_1, H_2 \rbrack$ is trivial if and only if $H_1$ is contained in the centralizer of $H_2$.
Subgroup.commutator_commutator_eq_bot_of_rotate theorem
(h1 : ⁅⁅H₂, H₃⁆, H₁⁆ = ⊥) (h2 : ⁅⁅H₃, H₁⁆, H₂⁆ = ⊥) : ⁅⁅H₁, H₂⁆, H₃⁆ = ⊥
Full source 
/-- **The Three Subgroups Lemma** (via the Hall-Witt identity) -/
theorem commutator_commutator_eq_bot_of_rotate (h1 : ⁅⁅H₂, H₃⁆, H₁⁆ = ⊥) (h2 : ⁅⁅H₃, H₁⁆, H₂⁆ = ⊥) :
    ⁅⁅H₁, H₂⁆, H₃⁆ = ⊥ := by
  simp_rw [commutator_eq_bot_iff_le_centralizer, commutator_le,
    mem_centralizer_iff_commutator_eq_one, ← commutatorElement_def] at h1 h2 ⊢
  intro x hx y hy z hz
  trans x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹
  -- We avoid `group` here to minimize imports while low in the hierarchy;
  -- typically it would be better to invoke the tactic.
  · simp [commutatorElement_def, mul_assoc]
  · rw [h1 _ (H₂.inv_mem hy) _ hz _ (H₁.inv_mem hx), h2 _ (H₃.inv_mem hz) _ (H₁.inv_mem hx) _ hy]
    simp [commutatorElement_def, mul_assoc]
Three Subgroups Lemma (via Hall-Witt identity)
Informal description
Let $G$ be a group with subgroups $H_1, H_2, H_3$. If the commutator subgroups $\lbrack \lbrack H_2, H_3 \rbrack, H_1 \rbrack$ and $\lbrack \lbrack H_3, H_1 \rbrack, H_2 \rbrack$ are both trivial, then the commutator subgroup $\lbrack \lbrack H_1, H_2 \rbrack, H_3 \rbrack$ is also trivial.
Subgroup.commutator_comm_le theorem
: ⁅H₁, H₂⁆ ≤ ⁅H₂, H₁⁆
Full source 
theorem commutator_comm_le : ⁅H₁, H₂⁆ ≤ ⁅H₂, H₁⁆ :=
  commutator_le.mpr fun g₁ h₁ g₂ h₂ =>
    commutatorElement_inv g₂ g₁ ▸ ⁅H₂, H₁⁆.inv_mem_iff.mpr (commutator_mem_commutator h₂ h₁)
Commutator Subgroup Containment: $\lbrack H_1, H_2 \rbrack \leq \lbrack H_2, H_1 \rbrack$
Informal description
For any subgroups $H_1$ and $H_2$ of a group $G$, the commutator subgroup $\lbrack H_1, H_2 \rbrack$ is contained in the commutator subgroup $\lbrack H_2, H_1 \rbrack$.
Subgroup.commutator_comm theorem
: ⁅H₁, H₂⁆ = ⁅H₂, H₁⁆
Full source 
theorem commutator_comm : ⁅H₁, H₂⁆ = ⁅H₂, H₁⁆ :=
  le_antisymm (commutator_comm_le H₁ H₂) (commutator_comm_le H₂ H₁)
Commutator Subgroup Symmetry: $\lbrack H_1, H_2 \rbrack = \lbrack H_2, H_1 \rbrack$
Informal description
For any subgroups $H_1$ and $H_2$ of a group $G$, the commutator subgroup $\lbrack H_1, H_2 \rbrack$ is equal to the commutator subgroup $\lbrack H_2, H_1 \rbrack$.
Subgroup.commutator_normal instance
[h₁ : H₁.Normal] [h₂ : H₂.Normal] : Normal ⁅H₁, H₂⁆
Full source 
instance commutator_normal [h₁ : H₁.Normal] [h₂ : H₂.Normal] : Normal ⁅H₁, H₂⁆ := by
  let base : Set G := { x | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = x }
  change (closure base).Normal
  suffices h_base : base = Group.conjugatesOfSet base by
    rw [h_base]
    exact Subgroup.normalClosure_normal
  refine Set.Subset.antisymm Group.subset_conjugatesOfSet fun a h => ?_
  simp_rw [Group.mem_conjugatesOfSet_iff, isConj_iff] at h
  rcases h with ⟨b, ⟨c, hc, e, he, rfl⟩, d, rfl⟩
  exact ⟨_, h₁.conj_mem c hc d, _, h₂.conj_mem e he d, (conjugate_commutatorElement c e d).symm⟩
Normality of the Commutator Subgroup of Normal Subgroups
Informal description
For any group $G$ with normal subgroups $H_1$ and $H_2$, the commutator subgroup $\lbrack H_1, H_2 \rbrack$ is also a normal subgroup of $G$.
Subgroup.commutator_def' theorem
[H₁.Normal] [H₂.Normal] : ⁅H₁, H₂⁆ = normalClosure {g | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g}
Full source 
theorem commutator_def' [H₁.Normal] [H₂.Normal] :
    ⁅H₁, H₂⁆ = normalClosure { g | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g } :=
  le_antisymm closure_le_normalClosure (normalClosure_le_normal subset_closure)
Commutator Subgroup as Normal Closure of Commutator Elements
Informal description
For any group $G$ with normal subgroups $H_1$ and $H_2$, the commutator subgroup $\lbrack H_1, H_2 \rbrack$ is equal to the normal closure of the set of all elements $g \in G$ such that there exist $g_1 \in H_1$ and $g_2 \in H_2$ with $\lbrack g_1, g_2 \rbrack = g$.
Subgroup.commutator_le_right theorem
[h : H₂.Normal] : ⁅H₁, H₂⁆ ≤ H₂
Full source 
theorem commutator_le_right [h : H₂.Normal] : ⁅H₁, H₂⁆ ≤ H₂ :=
  commutator_le.mpr fun g₁ _h₁ g₂ h₂ => H₂.mul_mem (h.conj_mem g₂ h₂ g₁) (H₂.inv_mem h₂)
Commutator Subgroup of a Subgroup and a Normal Subgroup is Contained in the Normal Subgroup
Informal description
For any group $G$ with a normal subgroup $H_2$ and any subgroup $H_1$, the commutator subgroup $\lbrack H_1, H_2 \rbrack$ is contained in $H_2$.
Subgroup.commutator_le_left theorem
[H₁.Normal] : ⁅H₁, H₂⁆ ≤ H₁
Full source 
theorem commutator_le_left [H₁.Normal] : ⁅H₁, H₂⁆ ≤ H₁ :=
  commutator_comm H₂ H₁ ▸ commutator_le_right H₂ H₁
Commutator Subgroup of a Normal Subgroup and a Subgroup is Contained in the Normal Subgroup
Informal description
For any group $G$ with a normal subgroup $H_1$ and any subgroup $H_2$, the commutator subgroup $\lbrack H_1, H_2 \rbrack$ is contained in $H_1$.
Subgroup.commutator_bot_left theorem
: ⁅(⊥ : Subgroup G), H₁⁆ = ⊥
Full source 
@[simp]
theorem commutator_bot_left : ⁅(⊥ : Subgroup G), H₁⁆ = ⊥ :=
  le_bot_iff.mp (commutator_le_left ⊥ H₁)
Commutator with Trivial Subgroup on the Left is Trivial: $\lbrack \bot, H_1 \rbrack = \bot$
Informal description
For any subgroup $H_1$ of a group $G$, the commutator subgroup $\lbrack \bot, H_1 \rbrack$ is equal to the trivial subgroup $\bot$ of $G$, where $\bot$ denotes the trivial subgroup.
Subgroup.commutator_bot_right theorem
: ⁅H₁, ⊥⁆ = (⊥ : Subgroup G)
Full source 
@[simp]
theorem commutator_bot_right : ⁅H₁, ⊥⁆ = (⊥ : Subgroup G) :=
  le_bot_iff.mp (commutator_le_right H₁ ⊥)
Commutator with Trivial Subgroup is Trivial: $\lbrack H_1, \bot \rbrack = \bot$
Informal description
For any subgroup $H_1$ of a group $G$, the commutator subgroup $\lbrack H_1, \bot \rbrack$ is equal to the trivial subgroup $\bot$ of $G$.
Subgroup.commutator_le_inf theorem
[Normal H₁] [Normal H₂] : ⁅H₁, H₂⁆ ≤ H₁ ⊓ H₂
Full source 
theorem commutator_le_inf [Normal H₁] [Normal H₂] : ⁅H₁, H₂⁆ ≤ H₁ ⊓ H₂ :=
  le_inf (commutator_le_left H₁ H₂) (commutator_le_right H₁ H₂)
Commutator Subgroup of Two Normal Subgroups is Contained in Their Intersection
Informal description
For any group $G$ with normal subgroups $H_1$ and $H_2$, the commutator subgroup $\lbrack H_1, H_2 \rbrack$ is contained in the intersection $H_1 \cap H_2$.
Subgroup.map_commutator theorem
(f : G →* G') : map f ⁅H₁, H₂⁆ = ⁅map f H₁, map f H₂⁆
Full source 
theorem map_commutator (f : G →* G') : map f ⁅H₁, H₂⁆ = ⁅map f H₁, map f H₂⁆ := by
  simp_rw [le_antisymm_iff, map_le_iff_le_comap, commutator_le, mem_comap, map_commutatorElement]
  constructor
  · intro p hp q hq
    exact commutator_mem_commutator (mem_map_of_mem _ hp) (mem_map_of_mem _ hq)
  · rintro _ ⟨p, hp, rfl⟩ _ ⟨q, hq, rfl⟩
    rw [← map_commutatorElement]
    exact mem_map_of_mem _ (commutator_mem_commutator hp hq)
Homomorphism Preserves Commutator Subgroup: $f(\lbrack H_1, H_2 \rbrack) = \lbrack f(H_1), f(H_2) \rbrack$
Informal description
For any group homomorphism $f \colon G \to G'$ and subgroups $H_1, H_2$ of $G$, the image of the commutator subgroup $\lbrack H_1, H_2 \rbrack$ under $f$ is equal to the commutator subgroup of the images, i.e., \[ f(\lbrack H_1, H_2 \rbrack) = \lbrack f(H_1), f(H_2) \rbrack. \]
Subgroup.commutator_le_map_commutator theorem
{f : G →* G'} {K₁ K₂ : Subgroup G'} (h₁ : K₁ ≤ H₁.map f) (h₂ : K₂ ≤ H₂.map f) : ⁅K₁, K₂⁆ ≤ ⁅H₁, H₂⁆.map f
Full source 
theorem commutator_le_map_commutator {f : G →* G'} {K₁ K₂ : Subgroup G'} (h₁ : K₁ ≤ H₁.map f)
    (h₂ : K₂ ≤ H₂.map f) : ⁅K₁, K₂⁆ ≤ ⁅H₁, H₂⁆.map f :=
  (commutator_mono h₁ h₂).trans (ge_of_eq (map_commutator H₁ H₂ f))
Commutator Subgroup Under Homomorphism: $\lbrack K_1, K_2 \rbrack \leq f(\lbrack H_1, H_2 \rbrack)$ when $K_i \leq f(H_i)$
Informal description
Let $G$ and $G'$ be groups, $f \colon G \to G'$ a group homomorphism, and $H_1, H_2$ subgroups of $G$. For any subgroups $K_1, K_2$ of $G'$ such that $K_1 \leq f(H_1)$ and $K_2 \leq f(H_2)$, the commutator subgroup $\lbrack K_1, K_2 \rbrack$ is contained in $f(\lbrack H_1, H_2 \rbrack)$.
Subgroup.commutator_characteristic instance
[h₁ : Characteristic H₁] [h₂ : Characteristic H₂] : Characteristic ⁅H₁, H₂⁆
Full source 
instance commutator_characteristic [h₁ : Characteristic H₁] [h₂ : Characteristic H₂] :
    Characteristic ⁅H₁, H₂⁆ :=
  characteristic_iff_le_map.mpr fun ϕ =>
    commutator_le_map_commutator (characteristic_iff_le_map.mp h₁ ϕ)
      (characteristic_iff_le_map.mp h₂ ϕ)
Commutator of Characteristic Subgroups is Characteristic
Informal description
For any group $G$ and characteristic subgroups $H_1, H_2$ of $G$, the commutator subgroup $\lbrack H_1, H_2 \rbrack$ is also a characteristic subgroup of $G$.
Subgroup.commutator_prod_prod theorem
(K₁ K₂ : Subgroup G') : ⁅H₁.prod K₁, H₂.prod K₂⁆ = ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆
Full source 
theorem commutator_prod_prod (K₁ K₂ : Subgroup G') :
    ⁅H₁.prod K₁, H₂.prod K₂⁆ = ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆ := by
  apply le_antisymm
  · rw [commutator_le]
    rintro ⟨p₁, p₂⟩ ⟨hp₁, hp₂⟩ ⟨q₁, q₂⟩ ⟨hq₁, hq₂⟩
    exact ⟨commutator_mem_commutator hp₁ hq₁, commutator_mem_commutator hp₂ hq₂⟩
  · rw [prod_le_iff]
    constructor <;>
      · rw [map_commutator]
        apply commutator_mono <;>
          simp [le_prod_iff, map_map, MonoidHom.fst_comp_inl, MonoidHom.snd_comp_inl,
            MonoidHom.fst_comp_inr, MonoidHom.snd_comp_inr]
Commutator of Direct Products Equals Product of Commutators: $\lbrack H_1 \times K_1, H_2 \times K_2 \rbrack = \lbrack H_1, H_2 \rbrack \times \lbrack K_1, K_2 \rbrack$
Informal description
For any group $G$ with subgroups $H_1, H_2 \leq G$, and any group $G'$ with subgroups $K_1, K_2 \leq G'$, the commutator subgroup of the direct products $H_1 \times K_1$ and $H_2 \times K_2$ is equal to the direct product of the commutator subgroups $\lbrack H_1, H_2 \rbrack \times \lbrack K_1, K_2 \rbrack$. In symbols: \[ \lbrack H_1 \times K_1, H_2 \times K_2 \rbrack = \lbrack H_1, H_2 \rbrack \times \lbrack K_1, K_2 \rbrack. \]
Subgroup.commutator_pi_pi_le theorem
{η : Type*} {Gs : η → Type*} [∀ i, Group (Gs i)] (H 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⁆
Full source 
/-- 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 commutator_pi_pi_le {η : Type*} {Gs : η → Type*} [∀ i, Group (Gs i)]
    (H 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⁆ :=
  commutator_le.mpr fun _p hp _q hq i hi => commutator_mem_commutator (hp i hi) (hq i hi)
Commutator of Direct Products is Contained in Product of Commutators
Informal description
For any family of groups $\{G_i\}_{i \in \eta}$ and subgroups $H_i, K_i \leq G_i$ for each $i \in \eta$, the commutator subgroup of the direct products $\prod_{i \in \eta} H_i$ and $\prod_{i \in \eta} K_i$ is contained in the direct product of the commutator subgroups $\prod_{i \in \eta} [H_i, K_i]$. In symbols: \[ \left[\prod_{i \in \eta} H_i, \prod_{i \in \eta} K_i\right] \leq \prod_{i \in \eta} [H_i, K_i]. \]
commutatorSet definition
: Set G
Full source 
/-- The set of commutator elements `⁅g₁, g₂⁆` in `G`. -/
def commutatorSet : Set G :=
  { g | ∃ g₁ g₂ : G, ⁅g₁, g₂⁆ = g }
Commutator set of a group
Informal description
The set of all elements in a group \( G \) that can be expressed as commutators \(\lbrack g_1, g_2 \rbrack = g_1 g_2 g_1^{-1} g_2^{-1}\) for some \( g_1, g_2 \in G \).
commutatorSet_def theorem
: commutatorSet G = {g | ∃ g₁ g₂ : G, ⁅g₁, g₂⁆ = g}
Full source 
theorem commutatorSet_def : commutatorSet G = { g | ∃ g₁ g₂ : G, ⁅g₁, g₂⁆ = g } :=
  rfl
Definition of the Commutator Set via Commutator Elements
Informal description
The commutator set of a group $G$ is equal to the set of all elements $g \in G$ for which there exist elements $g_1, g_2 \in G$ such that the commutator $\lbrack g_1, g_2 \rbrack = g_1 g_2 g_1^{-1} g_2^{-1}$ equals $g$. In other words, \[ \text{commutatorSet}(G) = \{ g \in G \mid \exists g_1, g_2 \in G, \lbrack g_1, g_2 \rbrack = g \}. \]
mem_commutatorSet_iff theorem
: g ∈ commutatorSet G ↔ ∃ g₁ g₂ : G, ⁅g₁, g₂⁆ = g
Full source 
theorem mem_commutatorSet_iff : g ∈ commutatorSet Gg ∈ commutatorSet G ↔ ∃ g₁ g₂ : G, ⁅g₁, g₂⁆ = g :=
  Iff.rfl
Characterization of Commutator Set Membership: $g \in \text{commutatorSet}(G) \leftrightarrow \exists g_1, g_2 \in G, \lbrack g_1, g_2 \rbrack = g$
Informal description
An element $g$ of a group $G$ belongs to the commutator set of $G$ if and only if there exist elements $g_1, g_2 \in G$ such that the commutator $\lbrack g_1, g_2 \rbrack = g_1 g_2 g_1^{-1} g_2^{-1}$ equals $g$.