Subgroup functors and closed classes of groups

AbbreviationClasses of finite groups (Kourovka 16.82 setting)#✓fully proved

A class \(\mathfrak{X}\) of finite groups is a predicate on finite groups \(G\) (with carrier in the lowest type universe, together with their group structure); the groups satisfying it are the members of the class, written \(G \in \mathfrak{X}\).

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

Used by 5

Used byKourovka Problem 16.82 (Skiba) · Order on subgroup functors · Closed classes of finite groups · Closed subgroup functors · Prime divisors of a class of finite groups

DefinitionClosed classes of finite groups#✓fully proved

A class \(\mathfrak{X}\) of finite groups is closed when it contains at least one group and is closed under homomorphic images, subgroups and direct products: if \(G \in \mathfrak{X}\) and \(f : G \to H\) is a surjective homomorphism onto a finite group \(H\), then \(H \in \mathfrak{X}\); every subgroup of a group in \(\mathfrak{X}\) lies in \(\mathfrak{X}\); and if \(G, H \in \mathfrak{X}\), then \(G \times H \in \mathfrak{X}\).

def IsClosedClass (X : FiniteGroupClass) : Prop :=
  (∃ (G : Type) (_ : Group G) (_ : Finite G), X G) ∧
    (∀ (G H : Type) [Group G] [Finite G] [Group H] [Finite H] (f : G →* H),
      Function.Surjective f → X G → X H) ∧
    (∀ (G : Type) [Group G] [Finite G] (H : Subgroup G), X G → X H) ∧
    ∀ (G H : Type) [Group G] [Finite G] [Group H] [Finite H], X G → X H → X (G × H)

Uses 1 · Used by 1

Statement usesClasses of finite groups (Kourovka 16.82 setting)

Used byKourovka Problem 16.82 (Skiba)

AbbreviationSubgroup assignments#✓fully proved

A subgroup assignment \(\tau\) assigns to every finite group \(G\) (with carrier in the lowest type universe) a set \(\tau(G)\) of subgroups of \(G\).

abbrev SubgroupAssignment : Type 1 :=
  ∀ (G : Type) [Group G] [Finite G], Set (Subgroup G)

Used by 3

Used byKourovka Problem 16.82 (Skiba) · Order on subgroup functors · Closed subgroup functors

DefinitionClosed subgroup functors#✓fully proved

Let \(\mathfrak{X}\) be a class of finite groups. A subgroup assignment \(\tau\) is a closed subgroup functor on \(\mathfrak{X}\) (A. N. Skiba) when the following three conditions hold. For every \(G \in \mathfrak{X}\), \(G \in \tau(G)\). For every surjective homomorphism \(\varphi : A \to B\) with \(A, B \in \mathfrak{X}\), \(\varphi(H) \in \tau(B)\) for every \(H \in \tau(A)\) and \(\varphi^{-1}(T) \in \tau(A)\) for every \(T \in \tau(B)\). For every \(G \in \mathfrak{X}\), every \(H \in \tau(G)\) and every \(K \in \tau(H)\), the subgroup \(K\), viewed as a subgroup of \(G\), lies in \(\tau(G)\); that is, \(\tau(H) \subseteq \tau(G)\).

def IsClosedSubgroupFunctor (X : FiniteGroupClass) (τ : SubgroupAssignment) : Prop :=
  (∀ (G : Type) [Group G] [Finite G], X G → ⊤ ∈ τ G) ∧
    (∀ (A B : Type) [Group A] [Finite A] [Group B] [Finite B] (φ : A →* B),
      Function.Surjective φ → X A → X B →
        (∀ H ∈ τ A, H.map φ ∈ τ B) ∧ ∀ T ∈ τ B, T.comap φ ∈ τ A) ∧
    ∀ (G : Type) [Group G] [Finite G], X G → ∀ H ∈ τ G, ∀ K ∈ τ H, K.map H.subtype ∈ τ G

Uses 2 · Used by 1

Statement usesClasses of finite groups (Kourovka 16.82 setting) · Subgroup assignments

Used byKourovka Problem 16.82 (Skiba)

DefinitionOrder on subgroup functors#✓fully proved

Let \(\mathfrak{X}\) be a class of finite groups. For subgroup assignments \(\tau_1\) and \(\tau_2\), \(\tau_1 \le \tau_2\) on \(\mathfrak{X}\) when \(\tau_1(G) \subseteq \tau_2(G)\) for every \(G \in \mathfrak{X}\). This is the order of the lattice \(F(\mathfrak{X})\) of closed subgroup functors on \(\mathfrak{X}\).

def FunctorLE (X : FiniteGroupClass) (τ₁ τ₂ : SubgroupAssignment) : Prop :=
  ∀ (G : Type) [Group G] [Finite G], X G → τ₁ G ⊆ τ₂ G

Uses 2 · Used by 1

Statement usesClasses of finite groups (Kourovka 16.82 setting) · Subgroup assignments

Used byKourovka Problem 16.82 (Skiba)

DefinitionPrime divisors of a class of finite groups#✓fully proved

For a class \(\mathfrak{X}\) of finite groups, \(\pi(\mathfrak{X})\) is the set of primes \(p\) that divide the order of some group in \(\mathfrak{X}\).

def primesOf (X : FiniteGroupClass) : Set ℕ :=
  {p | p.Prime ∧ ∃ (G : Type) (_ : Group G) (_ : Finite G), X G ∧ p ∣ Nat.card G}

Uses 1 · Used by 1

Statement usesClasses of finite groups (Kourovka 16.82 setting)

Used byKourovka Problem 16.82 (Skiba)

DefinitionKourovka Problem 16.82 (Skiba)#✓fully proved

For a class \(\mathfrak{X}\) of finite groups, let \(\pi(\mathfrak{X})\) be the set of primes dividing the order of some group in \(\mathfrak{X}\), and for subgroup assignments \(\tau_1, \tau_2\) write \(\tau_1 \le \tau_2\) on \(\mathfrak{X}\) when \(\tau_1(G) \subseteq \tau_2(G)\) for every \(G \in \mathfrak{X}\). There is a class \(\mathfrak{X}\) of finite groups that contains at least one group, is closed under homomorphic images, subgroups and direct products, and contains a non-nilpotent group, such that the lattice \(F(\mathfrak{X})\) of closed subgroup functors on \(\mathfrak{X}\) has width at most \(|\pi(\mathfrak{X})|\): every set of closed subgroup functors on \(\mathfrak{X}\) in which no two distinct members \(\tau_1, \tau_2\) satisfy \(\tau_1 \le \tau_2\) on \(\mathfrak{X}\) has cardinality at most \(|\pi(\mathfrak{X})|\).

def existsNonnilpotentClassOfSmallWidth : Prop :=
  ∃ X : FiniteGroupClass, IsClosedClass X ∧
    (∃ (G : Type) (_ : Group G) (_ : Finite G), X G ∧ ¬ Group.IsNilpotent G) ∧
    ∀ A : Set SubgroupAssignment, (∀ τ ∈ A, IsClosedSubgroupFunctor X τ) →
      (∀ τ₁ ∈ A, ∀ τ₂ ∈ A, τ₁ ≠ τ₂ → ¬ FunctorLE X τ₁ τ₂) →
      Cardinal.mk A ≤ Cardinal.lift.{1} (Cardinal.mk (primesOf X))

Uses 6 · Used by 1

Statement usesClasses of finite groups (Kourovka 16.82 setting) · Order on subgroup functors · Closed classes of finite groups · Closed subgroup functors · Subgroup assignments · Prime divisors of a class of finite groups

Used byKourovka Problem 16.82 has a negative answer

TheoremKourovka Problem 16.82 has a negative answer#●ready to prove

For a class \(\mathfrak{X}\) of finite groups, let \(\pi(\mathfrak{X})\) be the set of primes dividing the order of some group in \(\mathfrak{X}\), and for subgroup assignments \(\tau_1, \tau_2\) write \(\tau_1 \le \tau_2\) on \(\mathfrak{X}\) when \(\tau_1(G) \subseteq \tau_2(G)\) for every \(G \in \mathfrak{X}\). There is no class \(\mathfrak{X}\) of finite groups that contains at least one group, is closed under homomorphic images, subgroups and direct products, contains a non-nilpotent group, and has the following property: every set of closed subgroup functors on \(\mathfrak{X}\) in which no two distinct members \(\tau_1, \tau_2\) satisfy \(\tau_1 \le \tau_2\) on \(\mathfrak{X}\) has cardinality at most \(|\pi(\mathfrak{X})|\). In other words, for every such class the lattice \(F(\mathfrak{X})\) of closed subgroup functors on \(\mathfrak{X}\) has width greater than \(|\pi(\mathfrak{X})|\).

The Kourovka Archive answers 16.82 "No such classes exist", citing Kamornikov (2010).

public theorem_wanted existsNonnilpotentClassOfSmallWidth_refuted :
    ¬ existsNonnilpotentClassOfSmallWidth

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.82 (A. N. Skiba); resolution: S. F. Kamornikov, Siberian Math. J. 51 (2010), no. 5, 824-829, Kourovka Archive, Problem 16.82 (No such classes exist).

Uses 1

Statement usesKourovka Problem 16.82 (Skiba)

7 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.