Mathlib.GroupTheory.Solvable

derivedSeries definition

: ℕ → Subgroup G

Full source

/-- The derived series of the group `G`, obtained by starting from the subgroup `⊤` and repeatedly
  taking the commutator of the previous subgroup with itself for `n` times. -/
def derivedSeries : ℕ → Subgroup G
  | 0 => ⊤
  | n + 1 => ⁅derivedSeries n, derivedSeries n⁆

Derived series of a group

Informal description

The derived series of a group $G$ is a sequence of subgroups $(G^{(n)})_{n \in \mathbb{N}}$ defined recursively by: - $G^{(0)} = G$ (the entire group) - $G^{(n+1)} = [G^{(n)}, G^{(n)}]$ (the commutator subgroup of $G^{(n)}$ with itself) where $[H, K]$ denotes the subgroup generated by all commutators $[h,k] = hkh^{-1}k^{-1}$ for $h \in H$ and $k \in K$.

derivedSeries_zero theorem

: derivedSeries G 0 = ⊤

Full source

@[simp]
theorem derivedSeries_zero : derivedSeries G 0 = ⊤ :=
  rfl

Base Case of Derived Series: $G^{(0)} = G$

Informal description

The zeroth term of the derived series of a group $G$ is equal to $G$ itself, i.e., $G^{(0)} = G$.

derivedSeries_succ theorem

(n : ℕ) : derivedSeries G (n + 1) = ⁅derivedSeries G n, derivedSeries G n⁆

Full source

@[simp]
theorem derivedSeries_succ (n : ℕ) :
    derivedSeries G (n + 1) = ⁅derivedSeries G n, derivedSeries G n⁆ :=
  rfl

Recursive Definition of Derived Series: $G^{(n+1)} = [G^{(n)}, G^{(n)}]$

Informal description

For any natural number $n$, the $(n+1)$-th term in the derived series of a group $G$ is equal to the commutator subgroup of the $n$-th term with itself, i.e., $G^{(n+1)} = [G^{(n)}, G^{(n)}]$.

derivedSeries_normal theorem

(n : ℕ) : (derivedSeries G n).Normal

Full source

theorem derivedSeries_normal (n : ℕ) : (derivedSeries G n).Normal := by
  induction n with
  | zero => exact (⊤ : Subgroup G).normal_of_characteristic
  | succ n ih => exact Subgroup.commutator_normal (derivedSeries G n) (derivedSeries G n)

Normality of Derived Series Terms

Informal description

For any natural number $n$, the $n$-th term $G^{(n)}$ in the derived series of a group $G$ is a normal subgroup of $G$.

derivedSeries_one theorem

: derivedSeries G 1 = commutator G

Full source

@[simp 1100]
theorem derivedSeries_one : derivedSeries G 1 = commutator G :=
  rfl

First Derived Subgroup Equals Commutator Subgroup

Informal description

The first term in the derived series of a group $G$ is equal to its commutator subgroup, i.e., $G^{(1)} = [G, G]$.

map_derivedSeries_le_derivedSeries theorem

(n : ℕ) : (derivedSeries G n).map f ≤ derivedSeries G' n

Full source

theorem map_derivedSeries_le_derivedSeries (n : ℕ) :
    (derivedSeries G n).map f ≤ derivedSeries G' n := by
  induction n with
  | zero => exact le_top
  | succ n ih => simp only [derivedSeries_succ, map_commutator, commutator_mono, ih]

Image of Derived Series under Homomorphism is Contained in Target's Derived Series

Informal description

For any group homomorphism $f \colon G \to G'$ and any natural number $n$, the image of the $n$-th term of the derived series of $G$ under $f$ is contained in the $n$-th term of the derived series of $G'$, i.e., \[ f(G^{(n)}) \leq G'^{(n)}. \]

derivedSeries_le_map_derivedSeries theorem

(hf : Function.Surjective f) (n : ℕ) : derivedSeries G' n ≤ (derivedSeries G n).map f

Full source

theorem derivedSeries_le_map_derivedSeries (hf : Function.Surjective f) (n : ℕ) :
    derivedSeries G' n ≤ (derivedSeries G n).map f := by
  induction n with
  | zero => exact (map_top_of_surjective f hf).ge
  | succ n ih => exact commutator_le_map_commutator ih ih

Inclusion of Derived Series under Surjective Homomorphism: $G'^{(n)} \leq f(G^{(n)})$

Informal description

Let $f \colon G \to G'$ be a surjective group homomorphism. For any natural number $n$, the $n$-th term of the derived series of $G'$ is contained in the image under $f$ of the $n$-th term of the derived series of $G$, i.e., \[ G'^{(n)} \leq f(G^{(n)}). \]

map_derivedSeries_eq theorem

(hf : Function.Surjective f) (n : ℕ) : (derivedSeries G n).map f = derivedSeries G' n

Full source

theorem map_derivedSeries_eq (hf : Function.Surjective f) (n : ℕ) :
    (derivedSeries G n).map f = derivedSeries G' n :=
  le_antisymm (map_derivedSeries_le_derivedSeries f n) (derivedSeries_le_map_derivedSeries hf n)

Equality of Derived Series Images under Surjective Homomorphism: $f(G^{(n)}) = G'^{(n)}$

Informal description

Let $f \colon G \to G'$ be a surjective group homomorphism. For any natural number $n$, the image of the $n$-th term of the derived series of $G$ under $f$ is equal to the $n$-th term of the derived series of $G'$, i.e., \[ f(G^{(n)}) = G'^{(n)}. \]

IsSolvable structure

Full source

/-- A group `G` is solvable if its derived series is eventually trivial. We use this definition
  because it's the most convenient one to work with. -/
@[mk_iff isSolvable_def]
class IsSolvable : Prop where
  /-- A group `G` is solvable if its derived series is eventually trivial. -/
  solvable : ∃ n : ℕ, derivedSeries G n = ⊥

Solvable Group

Informal description

A group $G$ is solvable if its derived series eventually becomes the trivial subgroup. The derived series is defined by iteratively taking the commutator subgroup starting from $G$ itself.

CommGroup.isSolvable instance

{G : Type*} [CommGroup G] : IsSolvable G

Full source

instance (priority := 100) CommGroup.isSolvable {G : Type*} [CommGroup G] : IsSolvable G :=
  ⟨⟨1, le_bot_iff.mp (Abelianization.commutator_subset_ker (MonoidHom.id G))⟩⟩

Commutative Groups are Solvable

Informal description

Every commutative group is solvable.

isSolvable_of_comm theorem

{G : Type*} [hG : Group G] (h : ∀ a b : G, a * b = b * a) : IsSolvable G

Full source

theorem isSolvable_of_comm {G : Type*} [hG : Group G] (h : ∀ a b : G, a * b = b * a) :
    IsSolvable G := by
  letI hG' : CommGroup G := { hG with mul_comm := h }
  cases hG
  exact CommGroup.isSolvable

Commutative Groups are Solvable

Informal description

Let $G$ be a group such that every pair of elements $a, b \in G$ commutes (i.e., $a * b = b * a$). Then $G$ is solvable.

isSolvable_of_top_eq_bot theorem

(h : (⊤ : Subgroup G) = ⊥) : IsSolvable G

Full source

theorem isSolvable_of_top_eq_bot (h : (⊤ : Subgroup G) = ⊥) : IsSolvable G :=
  ⟨⟨0, h⟩⟩

Trivial Group is Solvable

Informal description

If the trivial subgroup $\{1\}$ equals the entire group $G$ (i.e., $G$ is the trivial group), then $G$ is solvable.

isSolvable_of_subsingleton instance

[Subsingleton G] : IsSolvable G

Full source

instance (priority := 100) isSolvable_of_subsingleton [Subsingleton G] : IsSolvable G :=
  isSolvable_of_top_eq_bot G (by simp [eq_iff_true_of_subsingleton])

Subsingleton Groups are Solvable

Informal description

Every group with at most one element is solvable.

solvable_of_ker_le_range theorem

 {G' G'' : Type*} [Group G'] [Group G''] (f : G' →* G) (g : G →* G'') (hfg : g.ker ≤ f.range) [hG' : IsSolvable G']
  [hG'' : IsSolvable G''] : IsSolvable G

Full source

theorem solvable_of_ker_le_range {G' G'' : Type*} [Group G'] [Group G''] (f : G' →* G)
    (g : G →* G'') (hfg : g.ker ≤ f.range) [hG' : IsSolvable G'] [hG'' : IsSolvable G''] :
    IsSolvable G := by
  obtain ⟨n, hn⟩ := id hG''
  obtain ⟨m, hm⟩ := id hG'
  refine ⟨⟨n + m, le_bot_iff.mp (Subgroup.map_bot f ▸ hm ▸ ?_)⟩⟩
  clear hm
  induction' m with m hm
  · exact f.range_eq_map ▸ ((derivedSeries G n).map_eq_bot_iff.mp
      (le_bot_iff.mp ((map_derivedSeries_le_derivedSeries g n).trans hn.le))).trans hfg
  · exact commutator_le_map_commutator hm hm

Solvability via Kernel-Image Condition: $G$ is solvable when $G'$ and $G''$ are solvable and $\ker g \leq \operatorname{range} f$

Informal description

Let $G'$, $G$, and $G''$ be groups with homomorphisms $f \colon G' \to G$ and $g \colon G \to G''$ such that the kernel of $g$ is contained in the image of $f$ (i.e., $\ker g \leq \operatorname{range} f$). If both $G'$ and $G''$ are solvable, then $G$ is also solvable.

solvable_of_solvable_injective theorem

(hf : Function.Injective f) [IsSolvable G'] : IsSolvable G

Full source

theorem solvable_of_solvable_injective (hf : Function.Injective f) [IsSolvable G'] :
    IsSolvable G :=
  solvable_of_ker_le_range (1 : G' →* G) f ((f.ker_eq_bot_iff.mpr hf).symm ▸ bot_le)

Solvability Preserved under Injective Homomorphism: If $G'$ is solvable and $f \colon G' \to G$ is injective, then $G$ is solvable.

Informal description

Let $f \colon G' \to G$ be an injective group homomorphism. If $G'$ is solvable, then $G$ is also solvable.

subgroup_solvable_of_solvable instance

(H : Subgroup G) [IsSolvable G] : IsSolvable H

Full source

instance subgroup_solvable_of_solvable (H : Subgroup G) [IsSolvable G] : IsSolvable H :=
  solvable_of_solvable_injective H.subtype_injective

Subgroups of Solvable Groups are Solvable

Informal description

Every subgroup $H$ of a solvable group $G$ is solvable.

solvable_of_surjective theorem

(hf : Function.Surjective f) [IsSolvable G] : IsSolvable G'

Full source

theorem solvable_of_surjective (hf : Function.Surjective f) [IsSolvable G] : IsSolvable G' :=
  solvable_of_ker_le_range f (1 : G' →* G) (f.range_eq_top_of_surjective hf ▸ le_top)

Solvability is preserved under surjective homomorphisms

Informal description

Let $f \colon G \to G'$ be a surjective group homomorphism. If $G$ is solvable, then $G'$ is also solvable.

solvable_quotient_of_solvable instance

(H : Subgroup G) [H.Normal] [IsSolvable G] : IsSolvable (G ⧸ H)

Full source

instance solvable_quotient_of_solvable (H : Subgroup G) [H.Normal] [IsSolvable G] :
    IsSolvable (G ⧸ H) :=
  solvable_of_surjective (QuotientGroup.mk'_surjective H)

Solvability of Quotient Groups from Solvable Groups

Informal description

For any group $G$ with a normal subgroup $H$, if $G$ is solvable, then the quotient group $G/H$ is also solvable.

solvable_prod instance

{G' : Type*} [Group G'] [IsSolvable G] [IsSolvable G'] : IsSolvable (G × G')

Full source

instance solvable_prod {G' : Type*} [Group G'] [IsSolvable G] [IsSolvable G'] :
    IsSolvable (G × G') :=
  solvable_of_ker_le_range (MonoidHom.inl G G') (MonoidHom.snd G G') fun x hx =>
    ⟨x.1, Prod.ext rfl hx.symm⟩

Solvability of Direct Product of Solvable Groups

Informal description

For any solvable groups $G$ and $G'$, the direct product $G \times G'$ is also solvable.

IsSolvable.commutator_lt_top_of_nontrivial theorem

[hG : IsSolvable G] [Nontrivial G] : commutator G < ⊤

Full source

theorem IsSolvable.commutator_lt_top_of_nontrivial [hG : IsSolvable G] [Nontrivial G] :
    commutator G < ⊤ := by
  rw [lt_top_iff_ne_top]
  obtain ⟨n, hn⟩ := hG
  contrapose! hn
  refine ne_of_eq_of_ne ?_ top_ne_bot
  induction' n with n h
  · exact derivedSeries_zero G
  · rwa [derivedSeries_succ, h]

Commutator Subgroup is Proper in Nontrivial Solvable Groups

Informal description

For any nontrivial solvable group $G$, the commutator subgroup $[G, G]$ is strictly contained in $G$ (i.e., $[G, G] < G$).

IsSolvable.commutator_lt_of_ne_bot theorem

[IsSolvable G] {H : Subgroup G} (hH : H ≠ ⊥) : ⁅H, H⁆ < H

Full source

theorem IsSolvable.commutator_lt_of_ne_bot [IsSolvable G] {H : Subgroup G} (hH : H ≠ ⊥) :
    ⁅H, H⁆ < H := by
  rw [← nontrivial_iff_ne_bot] at hH
  rw [← H.range_subtype, MonoidHom.range_eq_map, ← map_commutator, map_subtype_lt_map_subtype]
  exact commutator_lt_top_of_nontrivial H

Commutator Subgroup is Proper in Nontrivial Subgroups of Solvable Groups

Informal description

For any solvable group $G$ and any nontrivial subgroup $H$ of $G$ (i.e., $H \neq \{\text{id}\}$), the commutator subgroup $[H, H]$ is strictly contained in $H$ (i.e., $[H, H] < H$).

isSolvable_iff_commutator_lt theorem

[WellFoundedLT (Subgroup G)] : IsSolvable G ↔ ∀ H : Subgroup G, H ≠ ⊥ → ⁅H, H⁆ < H

Full source

theorem isSolvable_iff_commutator_lt [WellFoundedLT (Subgroup G)] :
    IsSolvableIsSolvable G ↔ ∀ H : Subgroup G, H ≠ ⊥ → ⁅H, H⁆ < H := by
  refine ⟨fun _ _ ↦ IsSolvable.commutator_lt_of_ne_bot, fun h ↦ ?_⟩
  suffices h : IsSolvable (⊤ : Subgroup G) from
    solvable_of_surjective (MonoidHom.range_eq_top.mp (range_subtype ⊤))
  refine WellFoundedLT.induction (C := fun (H : Subgroup G) ↦ IsSolvable H) ⊤ fun H hH ↦ ?_
  rcases eq_or_ne H ⊥ with rfl | h'
  · infer_instance
  · obtain ⟨n, hn⟩ := hH ⁅H, H⁆ (h H h')
    use n + 1
    rw [← (map_injective (subtype_injective _)).eq_iff, Subgroup.map_bot] at hn ⊢
    rw [← hn]
    clear hn
    induction' n with n ih
    · rw [derivedSeries_succ, derivedSeries_zero, derivedSeries_zero, map_commutator,
        ← MonoidHom.range_eq_map, ← MonoidHom.range_eq_map, range_subtype, range_subtype]
    · rw [derivedSeries_succ, map_commutator, ih, derivedSeries_succ, map_commutator]

Solvability Criterion: $G$ is solvable $\iff$ $[H,H] < H$ for all nontrivial $H \leq G$

Informal description

A group $G$ is solvable if and only if for every nontrivial subgroup $H$ of $G$ (i.e., $H \neq \{\text{id}\}$), the commutator subgroup $[H, H]$ is strictly contained in $H$ (i.e., $[H, H] < H$). This equivalence holds under the assumption that the strict partial order on subgroups of $G$ is well-founded.

IsSimpleGroup.derivedSeries_succ theorem

{n : ℕ} : derivedSeries G n.succ = commutator G

Full source

theorem IsSimpleGroup.derivedSeries_succ {n : ℕ} : derivedSeries G n.succ = commutator G := by
  induction n with
  | zero => exact derivedSeries_one G
  | succ n ih =>
    rw [_root_.derivedSeries_succ, ih, _root_.commutator]
    rcases (commutator_normal (⊤ : Subgroup G) (⊤ : Subgroup G)).eq_bot_or_eq_top with h | h
    · rw [h, commutator_bot_left]
    · rwa [h]

Derived Series of Simple Group Stabilizes at Commutator Subgroup

Informal description

For any natural number $n$, the $(n+1)$-th term in the derived series of a simple group $G$ is equal to the commutator subgroup of $G$, i.e., $G^{(n+1)} = [G, G]$.

IsSimpleGroup.comm_iff_isSolvable theorem

: (∀ a b : G, a * b = b * a) ↔ IsSolvable G

Full source

theorem IsSimpleGroup.comm_iff_isSolvable : (∀ a b : G, a * b = b * a) ↔ IsSolvable G :=
  ⟨isSolvable_of_comm, fun ⟨⟨n, hn⟩⟩ => by
    cases n
    · intro a b
      refine (mem_bot.1 ?_).trans (mem_bot.1 ?_).symm <;>
        · rw [← hn]
          exact mem_top _
    · rw [IsSimpleGroup.derivedSeries_succ] at hn
      intro a b
      rw [← mul_inv_eq_one, mul_inv_rev, ← mul_assoc, ← mem_bot, ← hn, commutator_eq_closure]
      exact subset_closure ⟨a, b, rfl⟩⟩

Solvability Equivalence: Commutative iff Solvable Group

Informal description

A group $G$ is solvable if and only if it is commutative, i.e., for all elements $a, b \in G$, the equality $a * b = b * a$ holds.

not_solvable_of_mem_derivedSeries theorem

{g : G} (h1 : g ≠ 1) (h2 : ∀ n : ℕ, g ∈ derivedSeries G n) : ¬IsSolvable G

Full source

theorem not_solvable_of_mem_derivedSeries {g : G} (h1 : g ≠ 1)
    (h2 : ∀ n : ℕ, g ∈ derivedSeries G n) : ¬IsSolvable G :=
  mt (isSolvable_def _).mp
    (not_exists_of_forall_not fun n h =>
      h1 (Subgroup.mem_bot.mp ((congr_arg (g ∈ ·) h).mp (h2 n))))

Non-solvability Criterion via Derived Series Membership

Informal description

For any group $G$ and any non-identity element $g \in G$ ($g \neq 1$), if $g$ belongs to every term of the derived series of $G$ (i.e., $g \in G^{(n)}$ for all $n \in \mathbb{N}$), then $G$ is not solvable.

Equiv.Perm.fin_5_not_solvable theorem

: ¬IsSolvable (Equiv.Perm (Fin 5))

Full source

theorem Equiv.Perm.fin_5_not_solvable : ¬IsSolvable (Equiv.Perm (Fin 5)) := by
  let x : Equiv.Perm (Fin 5) := ⟨![1, 2, 0, 3, 4], ![2, 0, 1, 3, 4], by decide, by decide⟩
  let y : Equiv.Perm (Fin 5) := ⟨![3, 4, 2, 0, 1], ![3, 4, 2, 0, 1], by decide, by decide⟩
  let z : Equiv.Perm (Fin 5) := ⟨![0, 3, 2, 1, 4], ![0, 3, 2, 1, 4], by decide, by decide⟩
  have key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹ := by unfold x y z; decide
  refine not_solvable_of_mem_derivedSeries (show x ≠ 1 by decide) fun n => ?_
  induction n with
  | zero => exact mem_top x
  | succ n ih =>
    rw [key, (derivedSeries_normal _ _).mem_comm_iff, inv_mul_cancel_left]
    exact commutator_mem_commutator ih ((derivedSeries_normal _ _).conj_mem _ ih _)

Non-solvability of the Symmetric Group $S_5$

Informal description

The symmetric group $S_5$ (the group of all permutations of a 5-element set) is not solvable.

Equiv.Perm.not_solvable theorem

(X : Type*) (hX : 5 ≤ Cardinal.mk X) : ¬IsSolvable (Equiv.Perm X)

Full source

theorem Equiv.Perm.not_solvable (X : Type*) (hX : 5 ≤ Cardinal.mk X) :
    ¬IsSolvable (Equiv.Perm X) := by
  intro h
  have key : Nonempty (FinFin 5 ↪ X) := by
    rwa [← Cardinal.lift_mk_le, Cardinal.mk_fin, Cardinal.lift_natCast, Cardinal.lift_id]
  exact
    Equiv.Perm.fin_5_not_solvable
      (solvable_of_solvable_injective (Equiv.Perm.viaEmbeddingHom_injective (Nonempty.some key)))

Non-solvability of Symmetric Groups on Sets with at Least 5 Elements

Informal description

For any type $X$ with at least 5 elements (i.e., $5 \leq |X|$), the symmetric group $\mathrm{Perm}(X)$ (the group of all permutations of $X$) is not solvable.

Main definitions