Maximal soluble subgroups

DefinitionKourovka 14.62: a maximal soluble subgroup whose normalizer supplements#✓fully proved

The proposition that for every finite group \(G\) and every non-soluble normal subgroup \(H\) of \(G\) there is a maximal soluble subgroup \(S\) of \(H\) (a soluble subgroup \(S \le H\) contained in no strictly larger soluble subgroup of \(H\)) such that \(G = H\,N_G(S)\), where \(N_G(S)\) is the normalizer of \(S\) in \(G\); since \(H\) is normal, this says that \(H\) and \(N_G(S)\) generate \(G\).

def maximalSolubleSubgroupNormalizerSupplement : Prop :=
  ∀ (G : Type) [Group G] [Finite G] (H : Subgroup G), H.Normal → ¬ Group.IsSolvable H →
    ∃ S : Subgroup G, S ≤ H ∧ Group.IsSolvable S ∧
      (∀ T : Subgroup G, S ≤ T → T ≤ H → Group.IsSolvable T → T = S) ∧
      H ⊔ Subgroup.normalizer (S : Set G) = ⊤

Used by 1

Used byZenkov–Monakhov–Revin theorem (Kourovka 14.62)

TheoremZenkov–Monakhov–Revin theorem (Kourovka 14.62)#●ready to prove

For every finite group \(G\) and every non-soluble normal subgroup \(H\) of \(G\) there is a maximal soluble subgroup \(S\) of \(H\) (a soluble subgroup \(S \le H\) contained in no strictly larger soluble subgroup of \(H\)) such that \(G = H\,N_G(S)\), where \(N_G(S)\) is the normalizer of \(S\) in \(G\); since \(H\) is normal, this says that \(H\) and \(N_G(S)\) generate \(G\).

Zenkov, Monakhov and Revin proved this using the classification of finite simple groups, so the Kourovka Archive answers 14.62 "Yes, it always exists".

public theorem_wanted maximalSolubleSubgroupNormalizerSupplement_holds :
    maximalSolubleSubgroupNormalizerSupplement

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 14.62 (V. S. Monakhov); resolution: V. I. Zenkov, V. S. Monakhov and D. O. Revin, Algebra and Logic 43 (2004), no. 2, 102-108 (using the classification of finite simple groups), Kourovka Archive, Problem 14.62 (answer: Yes, it always exists mod CFSG).

Uses 1

Statement usesKourovka 14.62: a maximal soluble subgroup whose normalizer supplements

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.