Supersolubility criteria

DefinitionSupersoluble group (Kourovka 15.81)#✓fully proved

A group \(G\) is supersoluble when it has a series \(1 = H_0 \le H_1 \le \cdots \le H_n = G\) of subgroups, each normal in \(G\), such that every factor \(H_{i+1}/H_i\) is cyclic.

def IsSupersoluble (G : Type*) [Group G] : Prop :=
  ∃ (n : ℕ) (H : Fin (n + 1) → Subgroup G), H 0 = ⊥ ∧ H (Fin.last n) = ⊤ ∧ (∀ i, (H i).Normal) ∧
    ∀ i : Fin n, H i.castSucc ≤ H i.succ ∧
      ∃ g ∈ H i.succ, ∀ x ∈ H i.succ, ∃ k : ℤ, x * (g ^ k)⁻¹ ∈ H i.castSucc

Used by 1

Used byUncomplemented maximal subgroups of Sylow subgroups (Kourovka 15.81, Skiba)

DefinitionUncomplemented maximal subgroups of Sylow subgroups (Kourovka 15.81, Skiba)#✓fully proved

The statement that every finite group \(G\) that is not supersoluble has, for some prime \(p\), a non-cyclic Sylow \(p\)-subgroup \(P\) with a maximal subgroup \(M\) of \(P\) that has no proper complement in \(G\), that is, there is no subgroup \(K \ne G\) with \(MK = G\) and \(M \cap K = 1\).

def nonSupersolubleHasUncomplementedSylowMaximal : Prop :=
  ∀ (G : Type) [Group G] [Finite G], ¬ IsSupersoluble G →
    ∃ p : ℕ, p.Prime ∧ ∃ P : Sylow p G, ¬ IsCyclic (P : Subgroup G) ∧
      ∃ M : Subgroup G, M < P ∧ (∀ L : Subgroup G, M < L → L ≤ P → L = P) ∧
        ¬ ∃ K : Subgroup G, K ≠ ⊤ ∧ (M : Set G) * (K : Set G) = Set.univ ∧ M ⊓ K = ⊥

def IsSupersoluble (G : Type*) [Group G] : Prop :=
  ∃ (n : ℕ) (H : Fin (n + 1) → Subgroup G), H 0 = ⊥ ∧ H (Fin.last n) = ⊤ ∧ (∀ i, (H i).Normal) ∧
    ∀ i : Fin n, H i.castSucc ≤ H i.succ ∧
      ∃ g ∈ H i.succ, ∀ x ∈ H i.succ, ∃ k : ℤ, x * (g ^ k)⁻¹ ∈ H i.castSucc

WantedExt/GroupTheory/NonSupersolubleUncomplementedMaximalKourovka15Problem81Wanted.lean:41

Uses 1 · Used by 1

Statement usesSupersoluble group (Kourovka 15.81)

Used byFinite non-supersoluble groups have uncomplemented maximal subgroups of Sylow subgroups

TheoremFinite non-supersoluble groups have uncomplemented maximal subgroups of Sylow subgroups#●ready to prove

For every finite group \(G\) that is not supersoluble, there are a prime \(p\) and a non-cyclic Sylow \(p\)-subgroup \(P\) of \(G\) with a maximal subgroup \(M\) of \(P\) that has no proper complement in \(G\): there is no subgroup \(K \ne G\) with \(MK = G\) and \(M \cap K = 1\). This answers Kourovka Problem 15.81 in the affirmative.

The Kourovka Archive answers 15.81 "Yes, it is" (Wang and Wei).

public theorem_wanted nonSupersolubleHasUncomplementedSylowMaximal_holds :
    nonSupersolubleHasUncomplementedSylowMaximal

def nonSupersolubleHasUncomplementedSylowMaximal : Prop :=
  ∀ (G : Type) [Group G] [Finite G], ¬ IsSupersoluble G →
    ∃ p : ℕ, p.Prime ∧ ∃ P : Sylow p G, ¬ IsCyclic (P : Subgroup G) ∧
      ∃ M : Subgroup G, M < P ∧ (∀ L : Subgroup G, M < L → L ≤ P → L = P) ∧
        ¬ ∃ K : Subgroup G, K ≠ ⊤ ∧ (M : Set G) * (K : Set G) = Set.univ ∧ M ⊓ K = ⊥

WantedExt/GroupTheory/NonSupersolubleUncomplementedMaximalKourovka15Problem81Wanted.lean:49

Sources

E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Archive of Solved Problems, Problem 15.81 (A. N. Skiba); resolution: Wang Yanming and Wei Huaquan, Sci. China Ser. A 47 (2004), no. 1, 96-103, Kourovka Archive, Problem 15.81 (answer: Yes, it is).

Uses 1

Statement usesUncomplemented maximal subgroups of Sylow subgroups (Kourovka 15.81, Skiba)

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.