Abnormal supersoluble factorizations

DefinitionSupersoluble groups via cyclic normal series#✓fully proved

A group \(G\) is supersoluble if there are a natural number \(k\) and subgroups \(1 = S_0 \le S_1 \le \cdots \le S_k = G\), each normal in \(G\), such that for every \(i < k\) we have \(S_i \le S_{i+1}\) and there is an element \(x \in S_{i+1}\) such that \(S_{i+1}\) is generated by \(x\) and \(S_i\); that is, every factor \(S_{i+1}/S_i\) is cyclic.

def IsSupersoluble (G : Type) [Group G] : Prop :=
  ∃ (k : ℕ) (s : ℕ → Subgroup G), s 0 = ⊥ ∧ s k = ⊤ ∧ ∀ i < k, s i ≤ s (i + 1) ∧ (s i).Normal ∧
    ∃ x ∈ s (i + 1), s (i + 1) = Subgroup.closure {x} ⊔ s i

Used by 1

Used byAbnormal supersoluble trifactorizations (Kourovka 19.100)

DefinitionAbnormal subgroup#✓fully proved

A subgroup \(H\) of a group \(G\) is abnormal in \(G\) if every element \(g \in G\) lies in the subgroup generated by \(H\) and its conjugate \(gHg^{-1}\).

def IsAbnormal {G : Type} [Group G] (H : Subgroup G) : Prop :=
  ∀ g : G, g ∈ H ⊔ H.map (MulAut.conj g).toMonoidHom

Used by 1

Used byAbnormal supersoluble trifactorizations (Kourovka 19.100)

DefinitionAbnormal supersoluble trifactorizations (Kourovka 19.100)#✓fully proved

The proposition that for every finite group \(G\) and all subgroups \(A\), \(B\), \(C\) of \(G\) that are abnormal in \(G\) and supersoluble, if \(G = AB = BC = CA\) as sets, then \(G\) is supersoluble.

def abnormalSupersolubleTriFactorizationSupersoluble : Prop :=
  ∀ (G : Type) [Group G] [Finite G] (A B C : Subgroup G),
    IsAbnormal A → IsAbnormal B → IsAbnormal C →
    IsSupersoluble A → IsSupersoluble B → IsSupersoluble C →
    (A : Set G) * (B : Set G) = Set.univ → (B : Set G) * (C : Set G) = Set.univ →
    (C : Set G) * (A : Set G) = Set.univ → IsSupersoluble G

def IsAbnormal {G : Type} [Group G] (H : Subgroup G) : Prop :=
  ∀ g : G, g ∈ H ⊔ H.map (MulAut.conj g).toMonoidHom

WantedExt/GroupTheory/AbnormalSupersolubleFactorizationKourovka19Problem100Wanted.lean:50

def IsSupersoluble (G : Type) [Group G] : Prop :=
  ∃ (k : ℕ) (s : ℕ → Subgroup G), s 0 = ⊥ ∧ s k = ⊤ ∧ ∀ i < k, s i ≤ s (i + 1) ∧ (s i).Normal ∧
    ∃ x ∈ s (i + 1), s (i + 1) = Subgroup.closure {x} ⊔ s i

WantedExt/GroupTheory/AbnormalSupersolubleFactorizationKourovka19Problem100Wanted.lean:45

Uses 2 · Used by 1

Statement usesAbnormal subgroup · Supersoluble groups via cyclic normal series

Used byKourovka Problem 19.100 has a positive answer

TheoremKourovka Problem 19.100 has a positive answer#●ready to prove

Let \(G\) be a finite group and let \(A\), \(B\), \(C\) be subgroups of \(G\), each abnormal in \(G\) and supersoluble, such that \(G = AB = BC = CA\) as sets. Then \(G\) is supersoluble.

The Kourovka Notebook (21st issue) answers 19.100 "Yes, it is" (L. S. Kazarin and V. N. Tyutyanov, 2023).

public theorem_wanted abnormalSupersolubleTriFactorizationSupersoluble_holds :
    abnormalSupersolubleTriFactorizationSupersoluble

def abnormalSupersolubleTriFactorizationSupersoluble : Prop :=
  ∀ (G : Type) [Group G] [Finite G] (A B C : Subgroup G),
    IsAbnormal A → IsAbnormal B → IsAbnormal C →
    IsSupersoluble A → IsSupersoluble B → IsSupersoluble C →
    (A : Set G) * (B : Set G) = Set.univ → (B : Set G) * (C : Set G) = Set.univ →
    (C : Set G) * (A : Set G) = Set.univ → IsSupersoluble G

WantedExt/GroupTheory/AbnormalSupersolubleFactorizationKourovka19Problem100Wanted.lean:55

Sources

E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 19.100 (A. F. Vasil'ev, T. I. Vasil'eva); resolution: L. S. Kazarin and V. N. Tyutyanov, preprint, 2023 (Russian), the Kourovka Notebook (21st issue) marks 19.100 solved: Yes, it is, https://kourovkanotebookorg.wordpress.com/wp-content/uploads/2025/09/d09ad0bed183d180d0bed0b2d0bad0b0-19.100-5.pdf.

Uses 1

Statement usesAbnormal supersoluble trifactorizations (Kourovka 19.100)

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.