Formations of p-groups and varieties

AbbreviationClasses of groups#✓fully proved

A class of groups is a predicate on groups: it assigns to every group \(G\) (in the lowest universe of types) a proposition, read as "\(G\) belongs to the class". No closure under isomorphism is required.

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

Used by 2

Used byFormations of finite groups · Kourovka Problem 11.21 (Vasil'yev's question on formations of \(p\)-groups)

StructureFormations of finite groups#✓fully proved

A class \(\mathfrak F\) of groups is a formation when every group in \(\mathfrak F\) is finite, \(\mathfrak F\) contains at least one group, \(\mathfrak F\) is closed under isomorphism, \(\mathfrak F\) is closed under quotients (if \(G \in \mathfrak F\) and \(N\) is a normal subgroup of \(G\), then \(G/N \in \mathfrak F\)), and \(\mathfrak F\) is closed under subdirect products: if \(G\) is a finite group with normal subgroups \(M\) and \(N\) such that \(G/M \in \mathfrak F\) and \(G/N \in \mathfrak F\), then \(G/(M \cap N) \in \mathfrak F\).

structure IsFormation (F : GroupClass) : Prop where
  finite : ∀ (G : Type) [Group G], F G → Finite G
  nonempty : ∃ (G : Type) (_ : Group G), F G
  of_mulEquiv : ∀ (G H : Type) [Group G] [Group H], (G ≃* H) → F G → F H
  quotient : ∀ (G : Type) [Group G] (N : Subgroup G) [N.Normal], F G → F (G ⧸ N)
  subdirect : ∀ (G : Type) [Group G] [Finite G] (M N : Subgroup G) [M.Normal] [N.Normal],
    F (G ⧸ M) → F (G ⧸ N) → F (G ⧸ (M ⊓ N))

Uses 1 · Used by 1

Statement usesClasses of groups

Used byKourovka Problem 11.21 (Vasil'yev's question on formations of \(p\)-groups)

DefinitionGroups satisfying a set of laws#✓fully proved

Let \(W\) be a set of words in the free group on countably many generators \(x_0, x_1, x_2, \dots\). A group \(G\) satisfies the laws in \(W\) when every homomorphism from this free group to \(G\) sends every \(w \in W\) to \(1\). The groups satisfying \(W\) form the variety defined by \(W\), and every variety arises this way.

def SatisfiesLaws (W : Set (FreeGroup ℕ)) (G : Type) [Group G] : Prop :=
  ∀ w ∈ W, ∀ f : FreeGroup ℕ →* G, f w = 1

Used by 3

Used byKourovka Problem 11.21 (Vasil'yev's question on formations of \(p\)-groups) · Consequence of a set of laws · Locally finite variety

DefinitionKourovka Problem 11.21 (Vasil'yev's question on formations of \(p\)-groups)#✓fully proved

The proposition that for every prime \(p\) and every formation \(\mathfrak F\) all of whose members are \(p\)-groups (a subformation of the formation \(\mathfrak N_p\) of all finite \(p\)-groups), there is a set \(W\) of laws, words in the free group on countably many generators, such that a finite \(p\)-group lies in \(\mathfrak F\) if and only if it satisfies every law in \(W\). In other words, every such \(\mathfrak F\) equals \(\mathfrak N_p \cap \mathfrak M\) for the variety \(\mathfrak M\) defined by \(W\).

def subformationOfPGroupsIsVarietal : Prop :=
  ∀ p : ℕ, p.Prime → ∀ F : GroupClass, IsFormation F →
    (∀ (G : Type) [Group G], F G → IsPGroup p G) →
    ∃ W : Set (FreeGroup ℕ), ∀ (G : Type) [Group G] [Finite G], IsPGroup p G →
      (F G ↔ SatisfiesLaws W G)

Uses 3 · Used by 1

Statement usesClasses of groups · Formations of finite groups · Groups satisfying a set of laws

Used byKourovka Problem 11.21 has a negative answer

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

There are a prime \(p\) and a formation \(\mathfrak F\) all of whose members are \(p\)-groups such that for every set \(W\) of laws, words in the free group on countably many generators, some finite \(p\)-group lies in \(\mathfrak F\) and fails a law in \(W\), or satisfies every law in \(W\) and does not lie in \(\mathfrak F\). Thus \(\mathfrak F\) is not of the form \(\mathfrak N_p \cap \mathfrak M\) for any variety \(\mathfrak M\), where \(\mathfrak N_p\) is the formation of all finite \(p\)-groups.

The Kourovka Archive answers 11.21 "No, it is not true" (A. N. Krasil'nikov): formations of finite \(p\)-groups correspond bijectively to varieties of pro-\(p\) groups, there are continuously many varieties of nilpotent pro-\(p\) groups of class at most \(6\) (Zubkov), hence continuously many formations of finite \(p\)-groups of class at most \(6\), while such a formation of the form \(\mathfrak N_p \cap \mathfrak M\) equals \(\mathfrak N_p \cap (\mathfrak M \cap \mathfrak N_6)\), where \(\mathfrak N_6\) is the variety of nilpotent groups of class at most \(6\), and there are only countably many varieties of nilpotent groups of class at most \(6\) (all finitely based).

public theorem_wanted subformationOfPGroupsIsVarietal_refuted : ¬ subformationOfPGroupsIsVarietal

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 11.21 (A. F. Vasil'yev); resolution: A. N. Krasil'nikov, letter of 17 July 1998, using A. N. Zubkov, Siberian Math. J. 29, no. 3 (1988), 491-494, Kourovka Archive, Problem 11.21: "No, it is not true"; formations of finite p-groups correspond to varieties of pro-p groups, there are continuously many varieties of nilpotent pro-p groups of class at most 6 (Zubkov) but only countably many varieties of nilpotent groups of class at most 6, https://arxiv.org/abs/1401.0300v49.

Uses 1

Statement usesKourovka Problem 11.21 (Vasil'yev's question on formations of \(p\)-groups)

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.