Indecomposable formations

AbbreviationClass of finite groups (Kourovka 10.72)#✓fully proved

A class of finite groups is given by a membership predicate: a proposition \(X(G)\) for every finite group \(G\). It is not required to be closed under isomorphisms.

abbrev GroupClass : Type 1 :=
  ∀ (G : Type) [Group G] [Finite G], Prop

Used by 3

Used byFormation of finite groups (Kourovka 10.72) · Indecomposability of the formation of finite \(p\)-groups (Kourovka 10.72) · Residual of a finite group with respect to a class (Kourovka 10.72)

DefinitionFormation of finite groups (Kourovka 10.72)#✓fully proved

A class \(X\) of finite groups is a formation when it is closed under isomorphisms, contains the trivial group, contains the quotient \(G/N\) of each of its members \(G\) by every normal subgroup \(N\), and contains \(G/(N_1 \cap N_2)\) whenever \(N_1\) and \(N_2\) are normal subgroups of a finite group \(G\) with \(G/N_1\) and \(G/N_2\) in \(X\). The last condition is closure under subdirect products.

def IsFormation (X : GroupClass) : Prop :=
  (∀ (G H : Type) [Group G] [Finite G] [Group H] [Finite H], (G ≃* H) → X G → X H) ∧ X Unit ∧
  (∀ (G : Type) [Group G] [Finite G] (N : Subgroup G) [N.Normal], X G → X (G ⧸ N)) ∧
  ∀ (G : Type) [Group G] [Finite G] (N₁ N₂ : Subgroup G) [N₁.Normal] [N₂.Normal],
    X (G ⧸ N₁) → X (G ⧸ N₂) → X (G ⧸ (N₁ ⊓ N₂))

Uses 1 · Used by 1

Statement usesClass of finite groups (Kourovka 10.72)

Used byIndecomposability of the formation of finite \(p\)-groups (Kourovka 10.72)

DefinitionResidual of a finite group with respect to a class (Kourovka 10.72)#✓fully proved

For a class \(X\) of finite groups and a finite group \(G\), the \(X\)-residual of \(G\) is the intersection of all normal subgroups \(N\) of \(G\) with \(G/N \in X\). When \(X\) is a formation, it is the smallest such \(N\).

def residual (X : GroupClass) (G : Type) [Group G] [Finite G] : Subgroup G :=
  ⨅ (N : Subgroup G) (_ : ∃ _ : N.Normal, X (G ⧸ N)), N

Uses 1 · Used by 1

Statement usesClass of finite groups (Kourovka 10.72)

Used byIndecomposability of the formation of finite \(p\)-groups (Kourovka 10.72)

DefinitionIndecomposability of the formation of finite \(p\)-groups (Kourovka 10.72)#✓fully proved

The statement that for every prime \(p\), the class \(\mathfrak{N}_p\) of all finite \(p\)-groups is not the Gaschütz product \(\mathfrak{F} \circ \mathfrak{G}\) of two formations \(\mathfrak{F}\) and \(\mathfrak{G}\) that consist of \(p\)-groups, each contain a nontrivial group and each omit some finite \(p\)-group. Here a finite group \(G\) lies in \(\mathfrak{F} \circ \mathfrak{G}\) when its \(\mathfrak{G}\)-residual lies in \(\mathfrak{F}\).

Omitting some finite \(p\)-group is part of the reading of "non-trivial": for all formations \(\mathfrak{F}, \mathfrak{G}\) consisting of \(p\)-groups, \(\mathfrak{N}_p \circ \mathfrak{G} = \mathfrak{F} \circ \mathfrak{N}_p = \mathfrak{N}_p\).

def pGroupFormationIndecomposable : Prop :=
  ∀ p : ℕ, p.Prime → ∀ F H : GroupClass, IsFormation F → IsFormation H →
    (∀ (G : Type) [Group G] [Finite G], F G → IsPGroup p G) →
    (∀ (G : Type) [Group G] [Finite G], H G → IsPGroup p G) →
    (∃ (G : Type) (_ : Group G) (_ : Finite G), Nontrivial G ∧ F G) →
    (∃ (G : Type) (_ : Group G) (_ : Finite G), Nontrivial G ∧ H G) →
    (∃ (G : Type) (_ : Group G) (_ : Finite G), IsPGroup p G ∧ ¬ F G) →
    (∃ (G : Type) (_ : Group G) (_ : Finite G), IsPGroup p G ∧ ¬ H G) →
    ¬ ∀ (G : Type) [Group G] [Finite G], IsPGroup p G ↔ F (residual H G)

Uses 3 · Used by 1

Statement usesClass of finite groups (Kourovka 10.72) · Formation of finite groups (Kourovka 10.72) · Residual of a finite group with respect to a class (Kourovka 10.72)

Used byThe formation of finite \(p\)-groups is indecomposable

TheoremThe formation of finite \(p\)-groups is indecomposable#●ready to prove

For every prime \(p\), the class \(\mathfrak{N}_p\) of all finite \(p\)-groups is not the Gaschütz product \(\mathfrak{F} \circ \mathfrak{G}\) of two formations \(\mathfrak{F}\) and \(\mathfrak{G}\) that consist of \(p\)-groups, each contain a nontrivial group and each omit some finite \(p\)-group. Here a finite group \(G\) lies in \(\mathfrak{F} \circ \mathfrak{G}\) when its \(\mathfrak{G}\)-residual lies in \(\mathfrak{F}\).

public theorem_wanted pGroupFormationIndecomposable_holds : pGroupFormationIndecomposable

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 10.72 (L. A. Shemetkov); resolution: A. N. Skiba and L. A. Shemetkov, Dokl. Akad. Nauk BSSR 33 (1989), 581-582 (Russian), Kourovka Archive, Problem 10.72 ("This has been proved").

Uses 1

Statement usesIndecomposability of the formation of finite \(p\)-groups (Kourovka 10.72)

StructureIsomorphism-closed classes of groups (Kourovka 12.97)#✓fully proved

A class of groups is given by a membership predicate on groups such that every group isomorphic to a member is again a member. Only the finite members matter in the formulation of Kourovka Problem 12.97.

structure GroupClass where
  /-- Membership predicate. -/
  mem : ∀ (H : Type) [Group H], Prop
  /-- Closure under isomorphism. -/
  iso : ∀ (H K : Type) [Group H] [Group K], (H ≃* K) → mem H → mem K

Used by 5

Used byKourovka Problem 12.97 (Shemetkov) · Formations of finite groups (Kourovka 12.97) · Proper subclass of a formation · Classes containing a nontrivial finite group · The residual of a group with respect to a class (Kourovka 12.97)

DefinitionFormations of finite groups (Kourovka 12.97)#✓fully proved

A class \(X\) of groups is a formation when it contains the trivial group, the quotient \(G/N\) lies in \(X\) for every finite group \(G\) in \(X\) and every normal subgroup \(N\) of \(G\), and for every finite group \(G\) with normal subgroups \(N_1\) and \(N_2\) such that \(G/N_1\) and \(G/N_2\) lie in \(X\), the quotient \(G/(N_1 \cap N_2)\) lies in \(X\).

def IsFormation (X : GroupClass) : Prop :=
  X.mem Unit ∧
  (∀ (G : Type) [Group G] [Finite G] (N : Subgroup G) [N.Normal], X.mem G → X.mem (G ⧸ N)) ∧
  ∀ (G : Type) [Group G] [Finite G] (N₁ N₂ : Subgroup G) [N₁.Normal] [N₂.Normal],
    X.mem (G ⧸ N₁) → X.mem (G ⧸ N₂) → X.mem (G ⧸ (N₁ ⊓ N₂))

Uses 1 · Used by 1

Statement usesIsomorphism-closed classes of groups (Kourovka 12.97)

Used byKourovka Problem 12.97 (Shemetkov)

DefinitionClasses containing a nontrivial finite group#✓fully proved

A class \(X\) of groups is nontrivial when it contains a nontrivial finite group; for a formation this means that \(X\) is not the trivial formation.

def NontrivialClass (X : GroupClass) : Prop :=
  ∃ (G : Type) (_ : Group G) (_ : Finite G), Nontrivial G ∧ X.mem G

Uses 1 · Used by 1

Statement usesIsomorphism-closed classes of groups (Kourovka 12.97)

Used byKourovka Problem 12.97 (Shemetkov)

DefinitionThe residual of a group with respect to a class (Kourovka 12.97)#✓fully proved

For a class \(X\) of groups and a group \(G\), the \(X\)-residual of \(G\) is the intersection of all normal subgroups \(N\) of \(G\) such that the quotient \(G/N\) lies in \(X\).

def residual (X : GroupClass) (G : Type) [Group G] : Subgroup G :=
  ⨅ (N : Subgroup G) (_ : ∃ _ : N.Normal, X.mem (G ⧸ N)), N

Uses 1 · Used by 1

Statement usesIsomorphism-closed classes of groups (Kourovka 12.97)

Used byKourovka Problem 12.97 (Shemetkov)

DefinitionGroups with a subnormal series whose factors are all isomorphic to a given group#✓fully proved

For groups \(T\) and \(G\), the group \(G\) lies in the class \(\mathfrak{F}_T\) when it has a subnormal series \(1 = H_0 \le H_1 \le \dots \le H_n = G\), each \(H_i\) normal in \(H_{i+1}\), all of whose factors \(H_{i+1}/H_i\) are isomorphic to \(T\). For simple \(T\) these are the groups all of whose composition factors are isomorphic to \(T\).

def AllCompositionFactorsIso (T : Type) [Group T] (G : Type) [Group G] : Prop :=
  ∃ (n : ℕ) (H : Fin (n + 1) → Subgroup G), H 0 = ⊥ ∧ H (Fin.last n) = ⊤ ∧
    ∀ i : Fin n, H i.castSucc ≤ H i.succ ∧
      ∃ _ : ((H i.castSucc).subgroupOf (H i.succ)).Normal,
        Nonempty ((H i.succ ⧸ (H i.castSucc).subgroupOf (H i.succ)) ≃* T)

Used by 2

Used byKourovka Problem 12.97 (Shemetkov) · Proper subclass of a formation

DefinitionProper subclass of a formation#✓fully proved

X is a proper subclass of 𝔉_T: some finite group of 𝔉_T does not belong to X.

def IsProperIn (T : Type) [Group T] (X : GroupClass) : Prop :=
  ∃ (G : Type) (_ : Group G) (_ : Finite G), AllCompositionFactorsIso T G ∧ ¬ X.mem G

Uses 2 · Used by 1

Statement usesGroups with a subnormal series whose factors are all isomorphic to a given group · Isomorphism-closed classes of groups (Kourovka 12.97)

Used byKourovka Problem 12.97 (Shemetkov)

DefinitionKourovka Problem 12.97 (Shemetkov)#✓fully proved

For a group \(T\), write \(\mathfrak{F}_T\) for the class of groups having a subnormal series all of whose factors are isomorphic to \(T\). This is the proposition that, for every finite non-abelian simple group \(T\) and all formations \(\mathfrak{M}\) and \(\mathfrak{H}\) whose finite members lie in \(\mathfrak{F}_T\), each containing a nontrivial finite group and each missing some finite group of \(\mathfrak{F}_T\), it is not the case that every finite group \(G\) satisfies: \(G \in \mathfrak{F}_T\) if and only if the \(\mathfrak{H}\)-residual \(G^{\mathfrak{H}}\) of \(G\) lies in \(\mathfrak{M}\). In other words, \(\mathfrak{F}_T\) is not the Gaschütz product \(\mathfrak{M}\mathfrak{H} = \{G : G^{\mathfrak{H}} \in \mathfrak{M}\}\) of two nontrivial proper subformations.

def compositionFactorFormationIndecomposable : Prop :=
  ∀ (T : Type) [Group T] [Finite T], IsSimpleGroup T → (∃ a b : T, a * b ≠ b * a) →
    ∀ M H : GroupClass, IsFormation M → IsFormation H → NontrivialClass M →
      NontrivialClass H →
      (∀ (G : Type) [Group G] [Finite G], M.mem G → AllCompositionFactorsIso T G) →
      (∀ (G : Type) [Group G] [Finite G], H.mem G → AllCompositionFactorsIso T G) →
      IsProperIn T M → IsProperIn T H →
      ¬ ∀ (G : Type) [Group G] [Finite G], AllCompositionFactorsIso T G ↔ M.mem (residual H G)

Uses 6 · Used by 1

Statement usesGroups with a subnormal series whose factors are all isomorphic to a given group · Isomorphism-closed classes of groups (Kourovka 12.97) · Formations of finite groups (Kourovka 12.97) · Proper subclass of a formation · Classes containing a nontrivial finite group · The residual of a group with respect to a class (Kourovka 12.97)

Used byMel'nikov's theorem on Kourovka Problem 12.97

TheoremMel'nikov's theorem on Kourovka Problem 12.97#●ready to prove

Let \(T\) be a finite non-abelian simple group, and write \(\mathfrak{F}_T\) for the class of groups having a subnormal series all of whose factors are isomorphic to \(T\). Let \(\mathfrak{M}\) and \(\mathfrak{H}\) be formations whose finite members lie in \(\mathfrak{F}_T\), each containing a nontrivial finite group and each missing some finite group of \(\mathfrak{F}_T\). Then it is not true that, for every finite group \(G\), \(G\) lies in \(\mathfrak{F}_T\) if and only if its \(\mathfrak{H}\)-residual \(G^{\mathfrak{H}}\) lies in \(\mathfrak{M}\): the formation \(\mathfrak{F}_T\) is not the Gaschütz product \(\mathfrak{M}\mathfrak{H}\) of two nontrivial proper subformations.

public theorem_wanted compositionFactorFormationIndecomposable_holds :
    compositionFactorFormationIndecomposable

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 12.97 (L. A. Shemetkov); resolution: O. V. Mel'nikov, Problems in Algebra 9, Gomel', 1996, 42-47 (Russian), Kourovka Archive, Problem 12.97: it is proved.

Uses 1

Statement usesKourovka Problem 12.97 (Shemetkov)

11 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.