doc-next-gen

Mathlib.GroupTheory.Abelianization

Module docstring

{"# The abelianization of a group

This file defines the commutator and the abelianization of a group. It furthermore prepares for the result that the abelianization is left adjoint to the forgetful functor from abelian groups to groups, which can be found in Algebra/Category/Group/Adjunctions.

Main definitions

  • commutator: defines the commutator of a group G as a subgroup of G.
  • Abelianization: defines the abelianization of a group G as the quotient of a group by its commutator subgroup.
  • Abelianization.map: lifts a group homomorphism to a homomorphism between the abelianizations
  • MulEquiv.abelianizationCongr: Equivalent groups have equivalent abelianizations

"}

commutator definition
: Subgroup G
Full source 
/-- The commutator subgroup of a group G is the normal subgroup
  generated by the commutators [p,q]=`p*q*p⁻¹*q⁻¹`. -/
def commutator : Subgroup G := ⁅(⊤ : Subgroup G), ⊤⁆
Commutator subgroup of a group
Informal description
The commutator subgroup of a group $G$ is the subgroup generated by all commutators $[g, h] = ghg^{-1}h^{-1}$ for $g, h \in G$.
commutator_def theorem
: commutator G = ⁅(⊤ : Subgroup G), ⊤⁆
Full source 
theorem commutator_def : commutator G = ⁅(⊤ : Subgroup G), ⊤⁆ :=
  rfl
Commutator Subgroup as Trivial Subgroup Commutator
Informal description
The commutator subgroup of a group $G$ is equal to the commutator of the trivial subgroup $\top$ with itself, i.e., $\text{commutator}(G) = [\top, \top]$.
Subgroup.map_subtype_commutator theorem
(H : Subgroup G) : (_root_.commutator H).map H.subtype = ⁅H, H⁆
Full source 
theorem Subgroup.map_subtype_commutator (H : Subgroup G) :
    (_root_.commutator H).map H.subtype = ⁅H, H⁆ := by
  rw [_root_.commutator_def, map_commutator, ← MonoidHom.range_eq_map, H.range_subtype]
Inclusion Map Preserves Commutator Subgroup: $\text{im}(\text{commutator}(H)) = \lbrack H, H \rbrack$
Informal description
For any subgroup $H$ of a group $G$, the image of the commutator subgroup of $H$ under the inclusion map $H \hookrightarrow G$ is equal to the commutator subgroup $\lbrack H, H \rbrack$ in $G$.
instFGSubtypeMemSubgroupCommutatorOfFiniteElemCommutatorSet instance
[Finite (commutatorSet G)] : Group.FG (commutator G)
Full source 
instance [Finite (commutatorSet G)] : Group.FG (commutator G) := by
  rw [commutator_eq_closure]
  apply Group.closure_finite_fg
Finitely Generated Commutator Subgroup from Finite Commutator Set
Informal description
For any group $G$ with finite commutator set, the commutator subgroup of $G$ is finitely generated.
rank_commutator_le_card theorem
[Finite (commutatorSet G)] : Group.rank (commutator G) ≤ Nat.card (commutatorSet G)
Full source 
theorem rank_commutator_le_card [Finite (commutatorSet G)] :
    Group.rank (commutator G) ≤ Nat.card (commutatorSet G) := by
  rw [Subgroup.rank_congr (commutator_eq_closure G)]
  apply Subgroup.rank_closure_finite_le_nat_card
Rank Bound for Commutator Subgroup: $\text{rank}(\text{commutator}(G)) \leq |\text{commutatorSet}(G)|$
Informal description
For any group $G$ with finite commutator set, the rank of the commutator subgroup $\text{commutator}(G)$ is bounded above by the cardinality of the commutator set $\text{commutatorSet}(G)$, i.e., \[ \text{rank}(\text{commutator}(G)) \leq |\text{commutatorSet}(G)|. \]
commutator_centralizer_commutator_le_center theorem
: ⁅centralizer (commutator G : Set G), centralizer (commutator G)⁆ ≤ Subgroup.center G
Full source 
theorem commutator_centralizer_commutator_le_center :
    ⁅centralizer (commutator G : Set G), centralizer (commutator G)⁆ ≤ Subgroup.center G := by
  rw [← Subgroup.centralizer_univ, ← Subgroup.coe_top, ←
    Subgroup.commutator_eq_bot_iff_le_centralizer]
  suffices ⁅⁅⊤, centralizer (commutator G : Set G)⁆, centralizer (commutator G : Set G)⁆ = ⊥ by
    refine Subgroup.commutator_commutator_eq_bot_of_rotate ?_ this
    rwa [Subgroup.commutator_comm (centralizer (commutator G : Set G))]
  rw [Subgroup.commutator_comm, Subgroup.commutator_eq_bot_iff_le_centralizer]
  exact Set.centralizer_subset (Subgroup.commutator_mono le_top le_top)
Commutator of Centralizers of Commutator Subgroup is Central
Informal description
Let $G$ be a group. The commutator subgroup of the centralizer of the commutator subgroup of $G$ is contained in the center of $G$, i.e., \[ \big[ C_G([G,G]), C_G([G,G]) \big] \leq Z(G). \]
mem_commutatorSet_of_isConj_sq theorem
{g : G} (hg : IsConj g (g ^ 2)) : g ∈ commutatorSet G
Full source 
/-- If g is conjugate to g ^ 2, then g is a commutator -/
theorem mem_commutatorSet_of_isConj_sq {g : G} (hg : IsConj g (g ^ 2)) :
    g ∈ commutatorSet G := by
  obtain ⟨h, hg⟩ := hg
  use h, g
  rw [commutatorElement_def, hg]
  simp only [IsUnit.mul_inv_cancel_right, Units.isUnit, mul_inv_eq_iff_eq_mul, pow_two]
Conjugate-to-square implies commutator
Informal description
Let $G$ be a group and $g \in G$ an element such that $g$ is conjugate to $g^2$. Then $g$ is a commutator, i.e., there exist elements $g_1, g_2 \in G$ such that $g = [g_1, g_2] = g_1 g_2 g_1^{-1} g_2^{-1}$.
map_commutator_eq theorem
{H : Type*} [Group H] (f : G →* H) : Subgroup.map f (_root_.commutator G) = ⁅f.range, f.range⁆
Full source 
theorem map_commutator_eq {H : Type*} [Group H] (f : G →* H) :
    Subgroup.map f (_root_.commutator G) = ⁅f.range, f.range⁆ := by
  rw [_root_.commutator_def, Subgroup.map_commutator]
  apply congr_arg₂ <;>
  · rw [Subgroup.map_eq_range_iff]
    rw [codisjoint_iff, top_sup_eq]
Image of Commutator Subgroup under Homomorphism Equals Commutator of Range
Informal description
For any group homomorphism $f \colon G \to H$, the image of the commutator subgroup of $G$ under $f$ is equal to the commutator subgroup of the range of $f$, i.e., \[ f([G, G]) = [f(G), f(G)]. \]
Abelianization definition
: Type u
Full source 
/-- The abelianization of G is the quotient of G by its commutator subgroup. -/
def Abelianization : Type u :=
  G ⧸ commutator G
Abelianization of a group
Informal description
The abelianization of a group $G$ is the quotient group $G / [G, G]$, where $[G, G]$ is the commutator subgroup of $G$ (the subgroup generated by all commutators $[g, h] = ghg^{-1}h^{-1}$ for $g, h \in G$).
Abelianization.commGroup instance
: CommGroup (Abelianization G)
Full source 
instance commGroup : CommGroup (Abelianization G) where
  __ := QuotientGroup.Quotient.group _
  mul_comm x y := Quotient.inductionOn₂ x y fun a b ↦ Quotient.sound' <|
    QuotientGroup.leftRel_apply.mpr <| Subgroup.subset_closure
      -- We avoid `group` here to minimize imports while low in the hierarchy;
      -- typically it would be better to invoke the tactic.
      ⟨b⁻¹, Subgroup.mem_top _, a⁻¹, Subgroup.mem_top _, by simp [commutatorElement_def, mul_assoc]⟩
Commutative Group Structure on the Abelianization
Informal description
The abelianization of a group $G$ is a commutative group.
Abelianization.instInhabited instance
: Inhabited (Abelianization G)
Full source 
instance : Inhabited (Abelianization G) :=
  ⟨1⟩
Abelianization is Inhabited
Informal description
The abelianization of any group $G$ is an inhabited type, meaning it has at least one element.
Abelianization.instUnique instance
[Unique G] : Unique (Abelianization G)
Full source 
instance [Unique G] : Unique (Abelianization G) := Quotient.instUniqueQuotient _
Abelianization of a Unique Group is Unique
Informal description
If $G$ is a unique group (i.e., a group with exactly one element), then its abelianization $\text{Abelianization}(G)$ is also unique.
Abelianization.instFinite instance
[Finite G] : Finite (Abelianization G)
Full source 
instance [Finite G] : Finite (Abelianization G) :=
  Quotient.finite _
Finiteness of the Abelianization of a Finite Group
Informal description
For any finite group $G$, its abelianization $G / [G, G]$ is also finite.
Abelianization.of definition
: G →* Abelianization G
Full source 
/-- `of` is the canonical projection from G to its abelianization. -/
def of : G →* Abelianization G where
  toFun := QuotientGroup.mk
  map_one' := rfl
  map_mul' _ _ := rfl
Canonical projection to the abelianization of a group
Informal description
The canonical projection homomorphism from a group $G$ to its abelianization $G^{\text{ab}} = G / [G, G]$, where $[G, G]$ is the commutator subgroup of $G$. This homomorphism sends each element $g \in G$ to its equivalence class in the quotient group.
Abelianization.mk_eq_of theorem
(a : G) : Quot.mk _ a = of a
Full source 
@[simp]
theorem mk_eq_of (a : G) : Quot.mk _ a = of a :=
  rfl
Equivalence Class in Abelianization Equals Canonical Projection
Informal description
For any element $a$ in a group $G$, the equivalence class of $a$ in the quotient group $G / [G, G]$ (where $[G, G]$ is the commutator subgroup) is equal to the image of $a$ under the canonical projection homomorphism $\text{of} \colon G \to G^{\text{ab}}$.
Abelianization.ker_of theorem
: of.ker = commutator G
Full source 
@[simp]
theorem ker_of : of.ker = commutator G :=
  QuotientGroup.ker_mk' (commutator G)
Kernel of Abelianization Projection Equals Commutator Subgroup
Informal description
The kernel of the canonical projection homomorphism $\text{of} \colon G \to G^{\text{ab}}$ is equal to the commutator subgroup $[G, G]$, i.e., $\ker(\text{of}) = [G, G]$.
Abelianization.commutator_subset_ker theorem
: commutator G ≤ f.ker
Full source 
theorem commutator_subset_ker : commutator G ≤ f.ker := by
  rw [commutator_eq_closure, Subgroup.closure_le]
  rintro x ⟨p, q, rfl⟩
  simp [MonoidHom.mem_ker, mul_right_comm (f p) (f q), commutatorElement_def]
Commutator Subgroup is Contained in Kernel of Homomorphism to Abelian Group
Informal description
For any group homomorphism $f \colon G \to A$ where $A$ is an abelian group, the commutator subgroup of $G$ is contained in the kernel of $f$, i.e., $\text{commutator}(G) \leq \ker(f)$.
Abelianization.lift definition
: (G →* A) ≃ (Abelianization G →* A)
Full source 
/-- If `f : G → A` is a group homomorphism to an abelian group, then `lift f` is the unique map
  from the abelianization of a `G` to `A` that factors through `f`. -/
def lift : (G →* A) ≃ (Abelianization G →* A) where
  toFun f := QuotientGroup.lift _ f fun _ h => MonoidHom.mem_ker.2 <| commutator_subset_ker _ h
  invFun F := F.comp of
  left_inv _ := MonoidHom.ext fun _ => rfl
  right_inv _ := MonoidHom.ext fun x => QuotientGroup.induction_on x fun _ => rfl
Lift of a group homomorphism to the abelianization
Informal description
Given a group homomorphism $f \colon G \to A$ to an abelian group $A$, the function $\text{lift}(f)$ is the unique group homomorphism from the abelianization of $G$ to $A$ that factors through $f$, i.e., $\text{lift}(f) \circ \text{of} = f$, where $\text{of} \colon G \to G^{\text{ab}}$ is the canonical projection. This establishes a bijection between group homomorphisms from $G$ to $A$ and group homomorphisms from the abelianization of $G$ to $A$.
Abelianization.lift.of theorem
(x : G) : lift f (of x) = f x
Full source 
@[simp]
theorem lift.of (x : G) : lift f (of x) = f x :=
  rfl
Lift of Homomorphism Commutes with Canonical Projection
Informal description
For any group homomorphism $f \colon G \to A$ to an abelian group $A$ and any element $x \in G$, the lift of $f$ to the abelianization of $G$ satisfies $\text{lift}(f)(\text{of}(x)) = f(x)$, where $\text{of} \colon G \to G^{\text{ab}}$ is the canonical projection.
Abelianization.lift.unique theorem
(φ : Abelianization G →* A) -- hφ : φ agrees with f on the image of G in Gᵃᵇ (hφ : ∀ x : G, φ (Abelianization.of x) = f x) {x : Abelianization G} : φ x = lift f x
Full source 
theorem lift.unique (φ : AbelianizationAbelianization G →* A)
    -- hφ : φ agrees with f on the image of G in Gᵃᵇ
    (hφ : ∀ x : G, φ (Abelianization.of x) = f x)
    {x : Abelianization G} : φ x = lift f x :=
  QuotientGroup.induction_on x hφ
Uniqueness of the Lift from the Abelianization
Informal description
Let $G$ be a group with abelianization $G^{\text{ab}} = G / [G, G]$, and let $A$ be an abelian group. Given a group homomorphism $f \colon G \to A$, the lift $\text{lift}(f) \colon G^{\text{ab}} \to A$ is the unique group homomorphism such that for any homomorphism $\varphi \colon G^{\text{ab}} \to A$ satisfying $\varphi \circ \pi = f$ (where $\pi \colon G \to G^{\text{ab}}$ is the canonical projection), it holds that $\varphi(x) = \text{lift}(f)(x)$ for all $x \in G^{\text{ab}}$.
Abelianization.lift_of theorem
: lift of = MonoidHom.id (Abelianization G)
Full source 
@[simp]
theorem lift_of : lift of = MonoidHom.id (Abelianization G) :=
  lift.apply_symm_apply <| MonoidHom.id _
Lift of Canonical Projection is Identity on Abelianization
Informal description
The lift of the canonical projection homomorphism $\text{of} \colon G \to G^{\text{ab}}$ to the abelianization $G^{\text{ab}}$ is the identity homomorphism on $G^{\text{ab}}$, i.e., $\text{lift}(\text{of}) = \text{id}_{G^{\text{ab}}}$.
Abelianization.hom_ext theorem
(φ ψ : Abelianization G →* A) (h : φ.comp of = ψ.comp of) : φ = ψ
Full source 
/-- See note [partially-applied ext lemmas]. -/
@[ext]
theorem hom_ext (φ ψ : AbelianizationAbelianization G →* A) (h : φ.comp of = ψ.comp of) : φ = ψ :=
  MonoidHom.ext fun x => QuotientGroup.induction_on x <| DFunLike.congr_fun h
Uniqueness of Homomorphisms from the Abelianization
Informal description
Let $G$ be a group with abelianization $G^{\text{ab}} = G / [G, G]$, and let $A$ be an abelian group. For any two group homomorphisms $\varphi, \psi \colon G^{\text{ab}} \to A$, if $\varphi \circ \pi = \psi \circ \pi$ where $\pi \colon G \to G^{\text{ab}}$ is the canonical projection, then $\varphi = \psi$.
Abelianization.map definition
: Abelianization G →* Abelianization H
Full source 
/-- The map operation of the `Abelianization` functor -/
def map : AbelianizationAbelianization G →* Abelianization H :=
  lift (of.comp f)
Induced homomorphism on abelianizations
Informal description
Given a group homomorphism $f \colon G \to H$, the function $\text{map}(f)$ is the induced group homomorphism from the abelianization of $G$ to the abelianization of $H$, defined by lifting the composition of $f$ with the canonical projection $\text{of} \colon H \to H^{\text{ab}}$.
Abelianization.lift_of_comp theorem
: Abelianization.lift (Abelianization.of.comp f) = Abelianization.map f
Full source 
/-- Use `map` as the preferred simp normal form. -/
@[simp] theorem lift_of_comp :
    Abelianization.lift (Abelianization.of.comp f) = Abelianization.map f := rfl
Lift of Composition Equals Induced Homomorphism on Abelianizations
Informal description
Given a group homomorphism $f \colon G \to H$, the lift of the composition of the canonical projection $\text{of} \colon H \to H^{\text{ab}}$ with $f$ is equal to the induced homomorphism $\text{map}(f) \colon G^{\text{ab}} \to H^{\text{ab}}$. In other words, the following diagram commutes: \[ \text{lift}(\text{of} \circ f) = \text{map}(f) \] where $G^{\text{ab}}$ and $H^{\text{ab}}$ denote the abelianizations of $G$ and $H$ respectively.
Abelianization.map_of theorem
(x : G) : map f (of x) = of (f x)
Full source 
@[simp]
theorem map_of (x : G) : map f (of x) = of (f x) :=
  rfl
Commutativity of the abelianization map with canonical projection
Informal description
For any group homomorphism $f \colon G \to H$ and any element $x \in G$, the induced homomorphism $\text{map}(f)$ on the abelianizations satisfies $\text{map}(f)(\text{of}(x)) = \text{of}(f(x))$, where $\text{of}$ denotes the canonical projection to the abelianization.
Abelianization.map_id theorem
: map (MonoidHom.id G) = MonoidHom.id (Abelianization G)
Full source 
@[simp]
theorem map_id : map (MonoidHom.id G) = MonoidHom.id (Abelianization G) :=
  hom_ext _ _ rfl
Identity Homomorphism Induces Identity on Abelianization
Informal description
The induced homomorphism on the abelianization of a group $G$ by the identity homomorphism $\mathrm{id}_G \colon G \to G$ is equal to the identity homomorphism on the abelianization of $G$, i.e., $\mathrm{map}(\mathrm{id}_G) = \mathrm{id}_{G^{\text{ab}}}$ where $G^{\text{ab}} = G / [G, G]$.
Abelianization.map_comp theorem
{I : Type w} [Group I] (g : H →* I) : (map g).comp (map f) = map (g.comp f)
Full source 
@[simp]
theorem map_comp {I : Type w} [Group I] (g : H →* I) : (map g).comp (map f) = map (g.comp f) :=
  hom_ext _ _ rfl
Composition of Induced Abelianization Homomorphisms Equals Induced Composition
Informal description
Let $G$, $H$, and $I$ be groups, and let $f \colon G \to H$ and $g \colon H \to I$ be group homomorphisms. Then the composition of the induced homomorphisms on the abelianizations satisfies $(g^{\text{ab}} \circ f^{\text{ab}}) = (g \circ f)^{\text{ab}}$, where $(-)^{\text{ab}}$ denotes the induced homomorphism on the abelianization.
Abelianization.map_map_apply theorem
{I : Type w} [Group I] {g : H →* I} {x : Abelianization G} : map g (map f x) = map (g.comp f) x
Full source 
@[simp]
theorem map_map_apply {I : Type w} [Group I] {g : H →* I} {x : Abelianization G} :
    map g (map f x) = map (g.comp f) x :=
  DFunLike.congr_fun (map_comp _ _) x
Compatibility of Abelianization with Homomorphism Composition
Informal description
Let $G$, $H$, and $I$ be groups, and let $f \colon G \to H$ and $g \colon H \to I$ be group homomorphisms. For any element $x$ in the abelianization of $G$, the following equality holds: \[ g^{\text{ab}}(f^{\text{ab}}(x)) = (g \circ f)^{\text{ab}}(x) \] where $(-)^{\text{ab}}$ denotes the induced homomorphism on the abelianization.
MulEquiv.abelianizationCongr definition
(e : G ≃* H) : Abelianization G ≃* Abelianization H
Full source 
/-- Equivalent groups have equivalent abelianizations -/
def MulEquiv.abelianizationCongr (e : G ≃* H) : AbelianizationAbelianization G ≃* Abelianization H where
  toFun := Abelianization.map e.toMonoidHom
  invFun := Abelianization.map e.symm.toMonoidHom
  left_inv := by
    rintro ⟨a⟩
    simp
  right_inv := by
    rintro ⟨a⟩
    simp
  map_mul' := MonoidHom.map_mul _
Isomorphism of abelianizations induced by a group isomorphism
Informal description
Given a group isomorphism $e \colon G \to H$, the function $\text{abelianizationCongr}(e)$ is the induced group isomorphism between the abelianization of $G$ and the abelianization of $H$, defined by lifting $e$ and its inverse to the respective abelianizations.
abelianizationCongr_of theorem
(e : G ≃* H) (x : G) : e.abelianizationCongr (Abelianization.of x) = Abelianization.of (e x)
Full source 
@[simp]
theorem abelianizationCongr_of (e : G ≃* H) (x : G) :
    e.abelianizationCongr (Abelianization.of x) = Abelianization.of (e x) :=
  rfl
Compatibility of abelianization with group isomorphism on elements
Informal description
Given a group isomorphism $e \colon G \to H$ and an element $x \in G$, the image of the canonical projection of $x$ under the induced isomorphism of abelianizations equals the canonical projection of $e(x)$. That is, $e^{\text{ab}}(\overline{x}) = \overline{e(x)}$, where $\overline{x}$ denotes the image of $x$ in the abelianization of $G$.
abelianizationCongr_refl theorem
: (MulEquiv.refl G).abelianizationCongr = MulEquiv.refl (Abelianization G)
Full source 
@[simp]
theorem abelianizationCongr_refl :
    (MulEquiv.refl G).abelianizationCongr = MulEquiv.refl (Abelianization G) :=
  MulEquiv.toMonoidHom_injective Abelianization.lift_of
Identity Induces Identity on Abelianizations
Informal description
The isomorphism between the abelianizations induced by the identity group isomorphism $\text{refl}_G \colon G \to G$ is equal to the identity isomorphism on the abelianization of $G$, i.e., $(\text{refl}_G)^{\text{ab}} = \text{refl}_{G^{\text{ab}}}$.
abelianizationCongr_symm theorem
(e : G ≃* H) : e.abelianizationCongr.symm = e.symm.abelianizationCongr
Full source 
@[simp]
theorem abelianizationCongr_symm (e : G ≃* H) :
    e.abelianizationCongr.symm = e.symm.abelianizationCongr :=
  rfl
Inverse of Abelianization-Induced Isomorphism Equals Isomorphism Induced by Inverse
Informal description
For any group isomorphism $e \colon G \to H$, the inverse of the induced isomorphism $\text{abelianizationCongr}(e) \colon \text{Abelianization}(G) \to \text{Abelianization}(H)$ is equal to the isomorphism $\text{abelianizationCongr}(e^{-1}) \colon \text{Abelianization}(H) \to \text{Abelianization}(G)$ induced by the inverse isomorphism $e^{-1} \colon H \to G$.
abelianizationCongr_trans theorem
{I : Type v} [Group I] (e : G ≃* H) (e₂ : H ≃* I) : e.abelianizationCongr.trans e₂.abelianizationCongr = (e.trans e₂).abelianizationCongr
Full source 
@[simp]
theorem abelianizationCongr_trans {I : Type v} [Group I] (e : G ≃* H) (e₂ : H ≃* I) :
    e.abelianizationCongr.trans e₂.abelianizationCongr = (e.trans e₂).abelianizationCongr :=
  MulEquiv.toMonoidHom_injective (Abelianization.hom_ext _ _ rfl)
Composition of Induced Abelianization Isomorphisms
Informal description
Let $G$, $H$, and $I$ be groups, and let $e \colon G \to H$ and $e_2 \colon H \to I$ be group isomorphisms. Then the composition of the induced isomorphisms on the abelianizations, $e^{\text{ab}} \colon G^{\text{ab}} \to H^{\text{ab}}$ and $e_2^{\text{ab}} \colon H^{\text{ab}} \to I^{\text{ab}}$, is equal to the isomorphism induced by the composition $e \circ e_2 \colon G \to I$ on the abelianizations, i.e., $(e \circ e_2)^{\text{ab}} = e^{\text{ab}} \circ e_2^{\text{ab}}$.
Abelianization.equivOfComm definition
{H : Type*} [CommGroup H] : H ≃* Abelianization H
Full source 
/-- An Abelian group is equivalent to its own abelianization. -/
@[simps]
def Abelianization.equivOfComm {H : Type*} [CommGroup H] : H ≃* Abelianization H :=
  { Abelianization.of with
    toFun := Abelianization.of
    invFun := Abelianization.lift (MonoidHom.id H)
    left_inv := fun _ => rfl
    right_inv := by
      rintro ⟨a⟩
      rfl }
Isomorphism between an abelian group and its abelianization
Informal description
For any abelian group $H$, there is a group isomorphism between $H$ and its abelianization, where the forward map is the canonical projection and the inverse map is the unique lift of the identity homomorphism on $H$.
commutatorRepresentatives definition
: Set (G × G)
Full source 
/-- Representatives `(g₁, g₂) : G × G` of commutators `⁅g₁, g₂⁆ ∈ G`. -/
def commutatorRepresentatives : Set (G × G) :=
  Set.range fun g : commutatorSet G => (g.2.choose, g.2.choose_spec.choose)
Representatives of commutators in a group
Informal description
The set of pairs $(g_1, g_2) \in G \times G$ such that the commutator $\lbrack g_1, g_2 \rbrack$ represents an element in the commutator set of $G$. In other words, for each element $g$ in the commutator set of $G$, there exists a pair $(g_1, g_2)$ such that $g = \lbrack g_1, g_2 \rbrack = g_1 g_2 g_1^{-1} g_2^{-1}$.
instFiniteElemProdCommutatorRepresentativesOfCommutatorSet instance
[Finite (commutatorSet G)] : Finite (commutatorRepresentatives G)
Full source 
instance [Finite (commutatorSet G)] : Finite (commutatorRepresentatives G) :=
  Set.finite_coe_iff.mpr (Set.finite_range _)
Finiteness of Commutator Representatives from Finite Commutator Set
Informal description
If the commutator set of a group $G$ is finite, then the set of pairs $(g_1, g_2) \in G \times G$ representing commutators is also finite.
closureCommutatorRepresentatives definition
: Subgroup G
Full source 
/-- Subgroup generated by representatives `g₁ g₂ : G` of commutators `⁅g₁, g₂⁆ ∈ G`. -/
def closureCommutatorRepresentatives : Subgroup G :=
  closure (Prod.fstProd.fst '' commutatorRepresentatives GProd.fst '' commutatorRepresentatives G ∪ Prod.snd '' commutatorRepresentatives G)
Subgroup generated by commutator representatives
Informal description
The subgroup of $G$ generated by all elements $g_1$ and $g_2$ such that $(g_1, g_2)$ is a pair in the set of commutator representatives of $G$. In other words, it is the smallest subgroup containing all first and second components of the pairs that generate the commutators of $G$.
rank_closureCommutatorRepresentatives_le theorem
[Finite (commutatorSet G)] : Group.rank (closureCommutatorRepresentatives G) ≤ 2 * Nat.card (commutatorSet G)
Full source 
theorem rank_closureCommutatorRepresentatives_le [Finite (commutatorSet G)] :
    Group.rank (closureCommutatorRepresentatives G) ≤ 2 * Nat.card (commutatorSet G) := by
  rw [two_mul]
  exact
    (Subgroup.rank_closure_finite_le_nat_card _).trans
      ((Set.card_union_le _ _).trans
        (add_le_add ((Finite.card_image_le _).trans (Finite.card_range_le _))
          ((Finite.card_image_le _).trans (Finite.card_range_le _))))
Rank Bound for Subgroup Generated by Commutator Representatives
Informal description
For any group $G$ with finite commutator set, the rank of the subgroup generated by commutator representatives is at most twice the cardinality of the commutator set of $G$, i.e., \[ \text{rank}(\text{closureCommutatorRepresentatives}(G)) \leq 2 \cdot |\text{commutatorSet}(G)|. \]
image_commutatorSet_closureCommutatorRepresentatives theorem
: (closureCommutatorRepresentatives G).subtype '' commutatorSet (closureCommutatorRepresentatives G) = commutatorSet G
Full source 
theorem image_commutatorSet_closureCommutatorRepresentatives :
    (closureCommutatorRepresentatives G).subtype ''
        commutatorSet (closureCommutatorRepresentatives G) =
      commutatorSet G := by
  apply Set.Subset.antisymm
  · rintro - ⟨-, ⟨g₁, g₂, rfl⟩, rfl⟩
    exact ⟨g₁, g₂, rfl⟩
  · exact fun g hg =>
      ⟨_,
        ⟨⟨_, subset_closure (Or.inl ⟨_, ⟨⟨g, hg⟩, rfl⟩, rfl⟩)⟩,
          ⟨_, subset_closure (Or.inr ⟨_, ⟨⟨g, hg⟩, rfl⟩, rfl⟩)⟩, rfl⟩,
        hg.choose_spec.choose_spec⟩
Commutator Set Preservation under Subgroup Inclusion
Informal description
The image of the commutator set of the subgroup generated by commutator representatives under the inclusion map is equal to the commutator set of the original group $G$. In other words, the commutator set of the subgroup $\text{closureCommutatorRepresentatives}(G)$ maps exactly to the commutator set of $G$ via the subgroup inclusion.
card_commutatorSet_closureCommutatorRepresentatives theorem
: Nat.card (commutatorSet (closureCommutatorRepresentatives G)) = Nat.card (commutatorSet G)
Full source 
theorem card_commutatorSet_closureCommutatorRepresentatives :
    Nat.card (commutatorSet (closureCommutatorRepresentatives G)) = Nat.card (commutatorSet G) := by
  rw [← image_commutatorSet_closureCommutatorRepresentatives G]
  exact Nat.card_congr (Equiv.Set.image _ _ (subtype_injective _))
Cardinality Equality of Commutator Sets in Group and Its Subgroup
Informal description
The cardinality of the commutator set of the subgroup generated by commutator representatives of a group $G$ is equal to the cardinality of the commutator set of $G$ itself. In other words, $|\text{commutatorSet}(\text{closureCommutatorRepresentatives}(G))| = |\text{commutatorSet}(G)|$.
card_commutator_closureCommutatorRepresentatives theorem
: Nat.card (commutator (closureCommutatorRepresentatives G)) = Nat.card (commutator G)
Full source 
theorem card_commutator_closureCommutatorRepresentatives :
    Nat.card (commutator (closureCommutatorRepresentatives G)) = Nat.card (commutator G) := by
  rw [commutator_eq_closure G, ← image_commutatorSet_closureCommutatorRepresentatives, ←
    MonoidHom.map_closure, ← commutator_eq_closure]
  exact Nat.card_congr (Equiv.Set.image _ _ (subtype_injective _))
Cardinality Equality of Commutator Subgroups in Group and Its Subgroup
Informal description
The cardinality of the commutator subgroup of the subgroup generated by commutator representatives of $G$ is equal to the cardinality of the commutator subgroup of $G$ itself. In other words, $|\text{commutator}(\text{closureCommutatorRepresentatives}(G))| = |\text{commutator}(G)|$.
instFiniteElemSubtypeMemSubgroupClosureCommutatorRepresentativesCommutatorSet instance
[Finite (commutatorSet G)] : Finite (commutatorSet (closureCommutatorRepresentatives G))
Full source 
instance [Finite (commutatorSet G)] :
    Finite (commutatorSet (closureCommutatorRepresentatives G)) := by
  apply Nat.finite_of_card_ne_zero
  rw [card_commutatorSet_closureCommutatorRepresentatives]
  exact Finite.card_pos.ne'
Finiteness of Commutator Set in Generated Subgroup
Informal description
If the commutator set of a group $G$ is finite, then the commutator set of the subgroup generated by commutator representatives of $G$ is also finite.
Subgroup.Normal.quotient_commutative_iff_commutator_le theorem
{N : Subgroup G} [N.Normal] : Std.Commutative (· * · : G ⧸ N → _ → _) ↔ _root_.commutator G ≤ N
Full source 
theorem Subgroup.Normal.quotient_commutative_iff_commutator_le {N : Subgroup G} [N.Normal] :
    Std.CommutativeStd.Commutative (· * · : G ⧸ N → _ → _) ↔ _root_.commutator G ≤ N := by
  constructor
  · intro hcomm
    rw [commutator_eq_normalClosure]
    rw [← Subgroup.normalClosure_subset_iff]
    rintro x ⟨p, q, rfl⟩
    rw [SetLike.mem_coe, ← QuotientGroup.eq_one_iff, commutatorElement_def]
    simp only [SetLike.mem_coe, ← QuotientGroup.eq_one_iff, commutatorElement_def,
      QuotientGroup.mk_mul, QuotientGroup.mk_inv]
    simp only [← commutatorElement_def, commutatorElement_eq_one_iff_mul_comm]
    apply hcomm.comm
  · intro hGN
    apply Std.Commutative.mk
    rintro x'; obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective N x'
    intro y'; obtain ⟨y, rfl⟩ := QuotientGroup.mk'_surjective N y'
    rw [← commutatorElement_eq_one_iff_mul_comm, ← map_commutatorElement,
      QuotientGroup.mk'_apply, QuotientGroup.eq_one_iff]
    apply hGN
    rw [commutator_eq_closure]
    exact Subgroup.subset_closure (commutator_mem_commutatorSet x y)
Quotient group is commutative iff commutator subgroup is contained in normal subgroup
Informal description
Let $G$ be a group and $N$ a normal subgroup of $G$. The quotient group $G/N$ is commutative if and only if the commutator subgroup of $G$ is contained in $N$. In other words, the multiplication operation in the quotient group $G/N$ is commutative precisely when $\text{commutator}(G) \subseteq N$.
Subgroup.Normal.commutator_le_of_self_sup_commutative_eq_top theorem
{N : Subgroup G} [N.Normal] {H : Subgroup G} (hHN : N ⊔ H = ⊤) (hH : IsMulCommutative H) : _root_.commutator G ≤ N
Full source 
/-- If `N` is a normal subgroup of `G` and `H` a commutative subgroup such that `H ⊔ N = ⊤`,
  then `N` contains `commutator G`. -/
theorem Subgroup.Normal.commutator_le_of_self_sup_commutative_eq_top {N : Subgroup G} [N.Normal]
    {H : Subgroup G} (hHN : N ⊔ H = ⊤) (hH : IsMulCommutative H) :
    _root_.commutator G ≤ N := by
  -- It is enough to prove that Q = G ⧸ N is commutative
  rw [← quotient_commutative_iff_commutator_le]
  -- Q is a quotient of H
  let φ : H →ₙ* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)
  -- It is enough to prove that φ is surjective
  apply Function.Surjective.mul_comm (f := φ) _ hH.is_comm
  rw [MulHom.coe_coe, ← MonoidHom.range_eq_top]
  -- We have to prove that `MonoidHom.range φ = ⊤`
  simp only [φ, MonoidHom.range_eq_map, ← Subgroup.map_map]
  have : Subgroup.map (QuotientGroup.mk' N) ⊤ = ⊤ := by
    rw [← MonoidHom.range_eq_map, MonoidHom.range_eq_top]
    exact QuotientGroup.mk'_surjective N
  simp only [← this, Subgroup.map_eq_map_iff, QuotientGroup.ker_mk', sup_comm, ← hHN]
  simp [← MonoidHom.range_eq_map]
Commutator subgroup containment under normal-complementary commutative subgroup condition
Informal description
Let $G$ be a group, $N$ a normal subgroup of $G$, and $H$ a commutative subgroup of $G$ such that $N \sqcup H = \top$ (i.e., $N$ and $H$ generate $G$). Then the commutator subgroup of $G$ is contained in $N$, i.e., $\text{commutator}(G) \leq N$.