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 : ) :
    theorem derivedSeries_normal (G : Type u_1) [Group G] (n : ) :
    (derivedSeries G n).Normal
    @[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] :
    IsSolvable G ∃ (n : ), derivedSeries G n =
    class IsSolvable (G : Type u_1) [Group G] :

    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.

    • solvable : ∃ (n : ), derivedSeries G n =

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

    Instances
      theorem IsSolvable.solvable {G : Type u_1} :
      ∀ {inst : Group G} [self : IsSolvable G], ∃ (n : ), derivedSeries G n =

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

      @[instance 100]
      instance CommGroup.isSolvable {G : Type u_3} [CommGroup G] :
      Equations
      • =
      theorem isSolvable_of_comm {G : Type u_3} [hG : Group G] (h : ∀ (a b : G), a * b = b * a) :
      @[instance 100]
      Equations
      • =
      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 : g.ker f.range) [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'] :
      instance subgroup_solvable_of_solvable {G : Type u_1} [Group G] (H : Subgroup G) [IsSolvable G] :
      Equations
      • =
      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_quotient_of_solvable {G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] [IsSolvable G] :
      Equations
      • =
      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) :