Documentation

Mathlib.GroupTheory.Solvable

Solvable Groups #

In this file we introduce the notion of a solvable group. We define a solvable group as one whose derived series is eventually trivial. This requires defining the commutator of two subgroups and the derived series of a group.

Main definitions #

def derivedSeries (G : Type u_1) [Group G] :

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.

Equations
Instances For
    @[simp]
    theorem derivedSeries_zero (G : Type u_1) [Group G] :
    @[simp]
    theorem derivedSeries_succ (G : Type u_1) [Group G] (n : ) :
    @[simp]
    theorem derivedSeries_one (G : Type u_1) [Group G] :
    theorem map_derivedSeries_le_derivedSeries {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (n : ) :
    theorem derivedSeries_le_map_derivedSeries {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {f : G →* G'} (hf : Function.Surjective f) (n : ) :
    theorem map_derivedSeries_eq {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {f : G →* G'} (hf : Function.Surjective f) (n : ) :
    theorem isSolvable_def (G : Type u_1) [Group G] :
    class IsSolvable (G : Type u_1) [Group G] :
    • solvable : n, derivedSeries G n =

      A group G is solvable if its derived series is eventually trivial.

    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.

    Instances
      theorem isSolvable_of_comm {G : Type u_3} [hG : Group G] (h : ∀ (a b : G), a * b = b * a) :
      theorem solvable_of_ker_le_range {G : Type u_1} [Group G] {G' : Type u_3} {G'' : Type u_4} [Group G'] [Group G''] (f : G' →* G) (g : G →* G'') (hfg : MonoidHom.ker g MonoidHom.range f) [hG' : IsSolvable G'] [hG'' : IsSolvable G''] :
      theorem solvable_of_solvable_injective {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {f : G →* G'} (hf : Function.Injective f) [IsSolvable G'] :
      theorem solvable_of_surjective {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {f : G →* G'} (hf : Function.Surjective f) [IsSolvable G] :
      instance solvable_prod {G : Type u_1} [Group G] {G' : Type u_3} [Group G'] [IsSolvable G] [IsSolvable G'] :
      IsSolvable (G × G')
      Equations
      theorem IsSimpleGroup.comm_iff_isSolvable {G : Type u_1} [Group G] [IsSimpleGroup G] :
      (∀ (a b : G), a * b = b * a) IsSolvable G
      theorem not_solvable_of_mem_derivedSeries {G : Type u_1} [Group G] {g : G} (h1 : g 1) (h2 : ∀ (n : ), g derivedSeries G n) :