Subformations of the formation generated by a group

AbbreviationClasses of finite groups#✓fully proved

A class of finite groups is a predicate on finite groups: it assigns to every finite group \(G\) a proposition, read as "\(G\) belongs to the class". The class need not be closed under isomorphism.

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

Used by 3

Used byKourovka Problem 16.31 for finite groups · Formation generated by a finite group · Formations of finite groups, possibly empty

DefinitionFormations of finite groups, possibly empty#✓fully proved

A class \(\mathfrak{F}\) of finite groups is a formation if it is closed under homomorphic images (whenever \(f \colon G \to H\) is a surjective homomorphism of finite groups and \(G \in \mathfrak{F}\), then \(H \in \mathfrak{F}\)) and under finite subdirect products (whenever \(N_1\) and \(N_2\) are normal subgroups of a finite group \(G\) with \(G / N_1 \in \mathfrak{F}\) and \(G / N_2 \in \mathfrak{F}\), then \(G / (N_1 \cap N_2) \in \mathfrak{F}\)). In particular the empty class is a formation.

def IsFormation (F : FiniteGroupClass) : Prop :=
  (∀ (G H : Type) [Group G] [Finite G] [Group H] [Finite H] (f : G →* H),
      Function.Surjective f → F G → F H) ∧
    ∀ (G : Type) [Group G] [Finite G] (N₁ N₂ : Subgroup G) [N₁.Normal] [N₂.Normal],
      F (G ⧸ N₁) → F (G ⧸ N₂) → F (G ⧸ (N₁ ⊓ N₂))

Uses 1 · Used by 2

Statement usesClasses of finite groups

Used byKourovka Problem 16.31 for finite groups · Formation generated by a finite group

DefinitionFormation generated by a finite group#✓fully proved

For a finite group \(G\), the formation generated by \(G\) is the class of finite groups \(H\) such that \(H\) belongs to every formation that contains \(G\); that is, it is the intersection of all formations containing \(G\).

def formationGeneratedBy (G : Type) [Group G] [Finite G] : FiniteGroupClass :=
  fun (H : Type) [Group H] [Finite H] => ∀ F : FiniteGroupClass, IsFormation F → F G → F H

Uses 2 · Used by 1

Statement usesClasses of finite groups · Formations of finite groups, possibly empty

Used byKourovka Problem 16.31 for finite groups

DefinitionKourovka Problem 16.31 for finite groups#✓fully proved

The statement (V. A. Vedernikov) that for every finite group \(G\) only finitely many formations of finite groups are contained in the formation generated by \(G\). Here formations may be empty, and a formation \(\mathfrak{F}\) is contained in the formation generated by \(G\) when every finite group in \(\mathfrak{F}\) belongs to the formation generated by \(G\).

def finitelyManySubformations : Prop :=
  ∀ (G : Type) [Group G] [Finite G],
    {F : FiniteGroupClass | IsFormation F ∧
      ∀ (H : Type) [Group H] [Finite H], F H → formationGeneratedBy G H}.Finite

Uses 3 · Used by 1

Statement usesClasses of finite groups · Formations of finite groups, possibly empty · Formation generated by a finite group

Used byThe formation generated by a finite group can have infinitely many subformations

TheoremThe formation generated by a finite group can have infinitely many subformations#●ready to prove

There is a finite group \(G\) such that infinitely many formations are contained in the formation generated by \(G\). That is, the answer to Kourovka Problem 16.31 is negative, even for finite \(G\).

public theorem_wanted finitelyManySubformations_refuted : ¬ finitelyManySubformations

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 16.31 (V. A. Vedernikov); resolution: V. P. Burichenko, J. Algebra 372 (2012), 428-458, Kourovka Archive, Problem 16.31 (No, not always, even for G finite).

Uses 1

Statement usesKourovka Problem 16.31 for finite groups

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.