Lattices of formations

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

A class of groups \(\mathfrak{X}\) is given by a membership predicate on groups whose underlying type lies in the lowest universe, such that whenever a group \(H\) belongs to \(\mathfrak{X}\) and \(K\) is a group isomorphic to \(H\), the group \(K\) also belongs to \(\mathfrak{X}\).

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 9
Used byInclusion of group classes · Algebraic sets of group classes · Compact elements of a set of group classes · Complete lattices of formations · Formations of finite groups (Kourovka 18.92) · Joins in a set of group classes · Modular sets of group classes · Kourovka Problem 18.92(a) (A. N. Skiba) · The non-modular formation lattice problem (Kourovka 18.92(b), A. N. Skiba)

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

A class \(\mathfrak{X}\) of groups is a formation if every group in \(\mathfrak{X}\) is finite, \(\mathfrak{X}\) contains the trivial group, for every finite group \(G\) in \(\mathfrak{X}\) and every normal subgroup \(N\) of \(G\) the quotient \(G/N\) lies in \(\mathfrak{X}\), 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 \(\mathfrak{X}\), the quotient \(G/(N_1 \cap N_2)\) lies in \(\mathfrak{X}\).

def IsFormation (X : GroupClass) : Prop :=
  (∀ (H : Type) [Group H], X.mem H → Finite H) ∧ 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 18.92)
Used byComplete lattices of formations

DefinitionInclusion of group classes#✓fully proved

For classes of groups \(\mathfrak{X}\) and \(\mathfrak{Y}\), the class \(\mathfrak{X}\) is included in \(\mathfrak{Y}\), written \(\mathfrak{X} \subseteq \mathfrak{Y}\), if every group that belongs to \(\mathfrak{X}\) also belongs to \(\mathfrak{Y}\).

def Incl (X Y : GroupClass) : Prop :=
  ∀ (H : Type) [Group H], X.mem H → Y.mem H
Uses 1 · Used by 4
Statement usesIsomorphism-closed classes of groups (Kourovka 18.92)
Used byCompact elements of a set of group classes · Complete lattices of formations · Joins in a set of group classes · Modular sets of group classes

DefinitionComplete lattices of formations#✓fully proved

A set \(\Theta\) of classes of groups is a complete lattice of formations if it is nonempty, every member of \(\Theta\) is a formation, for every nonempty subset \(S \subseteq \Theta\) the intersection of the classes in \(S\) (the class of groups belonging to every member of \(S\)) belongs to \(\Theta\), and \(\Theta\) has a member that contains every member of \(\Theta\).

def IsCompleteLatticeOfFormations (Θ : Set GroupClass) : Prop :=
  Θ.Nonempty ∧ (∀ X ∈ Θ, IsFormation X) ∧
  (∀ S ⊆ Θ, S.Nonempty → ∃ Y ∈ Θ, ∀ (H : Type) [Group H], Y.mem H ↔ ∀ X ∈ S, X.mem H) ∧
  ∃ T ∈ Θ, ∀ X ∈ Θ, Incl X T
Uses 3 · Used by 2
Statement usesIsomorphism-closed classes of groups (Kourovka 18.92) · Inclusion of group classes · Formations of finite groups (Kourovka 18.92)
Used byKourovka Problem 18.92(a) (A. N. Skiba) · The non-modular formation lattice problem (Kourovka 18.92(b), A. N. Skiba)

DefinitionJoins in a set of group classes#✓fully proved

Let \(\Theta\) and \(S\) be sets of classes of groups. A class \(\mathfrak{J}\) is the join of \(S\) in \(\Theta\) if \(\mathfrak{J} \in \Theta\), every member of \(S\) is contained in \(\mathfrak{J}\), and \(\mathfrak{J}\) is contained in every member of \(\Theta\) that contains every member of \(S\).

def IsJoinIn (Θ S : Set GroupClass) (J : GroupClass) : Prop :=
  J ∈ Θ ∧ (∀ X ∈ S, Incl X J) ∧ ∀ U ∈ Θ, (∀ X ∈ S, Incl X U) → Incl J U
Uses 2 · Used by 3
Statement usesIsomorphism-closed classes of groups (Kourovka 18.92) · Inclusion of group classes
Used byAlgebraic sets of group classes · Compact elements of a set of group classes · Modular sets of group classes

DefinitionCompact elements of a set of group classes#✓fully proved

Let \(\Theta\) be a set of classes of groups and \(\mathfrak{A}\) a class of groups. Then \(\mathfrak{A}\) is compact in \(\Theta\) if, for every subset \(S \subseteq \Theta\) and every join \(\mathfrak{J}\) of \(S\) in \(\Theta\) with \(\mathfrak{A} \subseteq \mathfrak{J}\), there are a finite subset \(S_1 \subseteq S\) and a join \(\mathfrak{J}_1\) of \(S_1\) in \(\Theta\) with \(\mathfrak{A} \subseteq \mathfrak{J}_1\).

def IsCompactIn (Θ : Set GroupClass) (A : GroupClass) : Prop :=
  ∀ S ⊆ Θ, ∀ J, IsJoinIn Θ S J → Incl A J →
    ∃ S₁ ⊆ S, S₁.Finite ∧ ∃ J₁, IsJoinIn Θ S₁ J₁ ∧ Incl A J₁
Uses 3 · Used by 1
Statement usesIsomorphism-closed classes of groups (Kourovka 18.92) · Inclusion of group classes · Joins in a set of group classes
Used byAlgebraic sets of group classes

DefinitionAlgebraic sets of group classes#✓fully proved

A set \(\Theta\) of classes of groups is algebraic if every member \(\mathfrak{A}\) of \(\Theta\) is the join in \(\Theta\) of some subset \(S \subseteq \Theta\) all of whose members are compact in \(\Theta\).

def IsAlgebraicIn (Θ : Set GroupClass) : Prop :=
  ∀ A ∈ Θ, ∃ S ⊆ Θ, (∀ C ∈ S, IsCompactIn Θ C) ∧ IsJoinIn Θ S A
Uses 3 · Used by 1
Statement usesIsomorphism-closed classes of groups (Kourovka 18.92) · Compact elements of a set of group classes · Joins in a set of group classes
Used byKourovka Problem 18.92(a) (A. N. Skiba)

DefinitionModular sets of group classes#✓fully proved

A set \(\Theta\) of classes of groups is modular if for all \(\mathfrak{A}, \mathfrak{B}, \mathfrak{C} \in \Theta\) with \(\mathfrak{A} \subseteq \mathfrak{C}\) the following holds: whenever \(\mathfrak{J}_1\) is the join in \(\Theta\) of the set \(\{\mathfrak{A}, \mathfrak{B} \cap \mathfrak{C}\}\) and \(\mathfrak{D}\) is the join in \(\Theta\) of the set \(\{\mathfrak{A}, \mathfrak{B}\}\), the classes \(\mathfrak{J}_1\) and \(\mathfrak{D} \cap \mathfrak{C}\) contain the same groups. This is the modular law \(\mathfrak{A} \vee (\mathfrak{B} \wedge \mathfrak{C}) = (\mathfrak{A} \vee \mathfrak{B}) \wedge \mathfrak{C}\), with joins taken in \(\Theta\) and meets the intersections.

def IsModularIn (Θ : Set GroupClass) : Prop :=
  ∀ A ∈ Θ, ∀ B ∈ Θ, ∀ C ∈ Θ, Incl A C → ∀ BC J₁ AB J₂ : GroupClass,
    (∀ (H : Type) [Group H], BC.mem H ↔ B.mem H ∧ C.mem H) → IsJoinIn Θ {A, BC} J₁ →
    IsJoinIn Θ {A, B} AB → (∀ (H : Type) [Group H], J₂.mem H ↔ AB.mem H ∧ C.mem H) →
    Incl J₁ J₂ ∧ Incl J₂ J₁
Uses 3 · Used by 1
Statement usesIsomorphism-closed classes of groups (Kourovka 18.92) · Inclusion of group classes · Joins in a set of group classes
Used byThe non-modular formation lattice problem (Kourovka 18.92(b), A. N. Skiba)

DefinitionKourovka Problem 18.92(a) (A. N. Skiba)#✓fully proved

The proposition that some set \(\Theta\) of classes of groups is a complete lattice of formations of finite groups and is not algebraic.

def nonAlgebraicCompleteLatticeOfFormations : Prop :=
  ∃ Θ : Set GroupClass, IsCompleteLatticeOfFormations Θ ∧ ¬ IsAlgebraicIn Θ
Uses 3 · Used by 1
Statement usesIsomorphism-closed classes of groups (Kourovka 18.92) · Algebraic sets of group classes · Complete lattices of formations
Used byNon-algebraic complete lattices of formations exist

DefinitionThe non-modular formation lattice problem (Kourovka 18.92(b), A. N. Skiba)#✓fully proved

The proposition that there is a complete lattice of formations of finite groups that is not modular, joins being least upper bounds in the lattice and meets being intersections.

def nonModularCompleteLatticeOfFormations : Prop :=
  ∃ Θ : Set GroupClass, IsCompleteLatticeOfFormations Θ ∧ ¬ IsModularIn Θ
Uses 3 · Used by 1
Statement usesIsomorphism-closed classes of groups (Kourovka 18.92) · Complete lattices of formations · Modular sets of group classes
Used byA non-modular complete lattice of formations exists (Kourovka 18.92(b))

TheoremNon-algebraic complete lattices of formations exist#●ready to prove

There is a set \(\Theta\) of classes of groups that is a complete lattice of formations of finite groups and is not algebraic; that is, Kourovka Problem 18.92(a) has a positive answer.

The Kourovka Notebook (21st issue) answers 18.92(a) "Yes", by an AI-generated solution confirmed by A. N. Skiba (Kinyon–Urban, 2026): for a set \(S\) of primes let \(\mathfrak{F}_S\) be the class of finite groups whose order has all its prime divisors in \(S\); the classes \(\mathfrak{F}_S\) with \(S\) finite, together with the class of all finite groups, form a complete lattice of formations whose only compact element is the bottom.

public theorem_wanted nonAlgebraicCompleteLatticeOfFormations_holds :
    nonAlgebraicCompleteLatticeOfFormations
Sources
  • E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 18.92 (A. N. Skiba); resolution: M. Kinyon and J. Urban, Results on problems from the Kourovka Notebook, preprint, version 4, 19 September 2026, Section 3.29 (Problem 18.92): with F_S the finite groups whose order has all prime divisors in S, {F_S : S finite} ∪ {F_P} is not algebraic and the formations with prime sets ∅, {2}, {2, 3}, {5}, P form a pentagon N_5; an AI solution confirmed by A. N. Skiba, accepted in the Kourovka Notebook (21st issue), https://kourovkanotebookorg.wordpress.com/wp-content/uploads/2026/09/kourovka-mathematics.pdf.
Uses 1
Statement usesKourovka Problem 18.92(a) (A. N. Skiba)

TheoremA non-modular complete lattice of formations exists (Kourovka 18.92(b))#●ready to prove

There is a complete lattice of formations of finite groups that is not modular: a nonempty set \(\Theta\) of formations of finite groups, ordered by inclusion, that contains the intersection of each of its nonempty subsets and has a largest element, in which the modular law \(A \vee (B \wedge C) = (A \vee B) \wedge C\) for \(A \le C\) fails, joins being least upper bounds in \(\Theta\) and meets intersections.

The Kourovka Notebook (21st issue) answers 18.92(b) "Yes" (Kinyon-Urban, 2026, confirmed by A. N. Skiba): writing \(\mathfrak{F}_S\) for the finite groups whose order has all prime divisors in \(S\), the formations \(\mathfrak{F}_S\) with \(S = \emptyset, \{2\}, \{2, 3\}, \{5\}\) and \(S\) the set of all primes are closed under intersections and form the pentagon \(N_5\).

public theorem_wanted nonModularCompleteLatticeOfFormations_holds :
    nonModularCompleteLatticeOfFormations
Sources
  • E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 18.92 (A. N. Skiba); resolution: M. Kinyon and J. Urban, Results on problems from the Kourovka Notebook, preprint, version 4, 19 September 2026, Section 3.29 (Problem 18.92): with F_S the finite groups whose order has all prime divisors in S, {F_S : S finite} ∪ {F_P} is not algebraic and the formations with prime sets ∅, {2}, {2, 3}, {5}, P form a pentagon N_5; an AI solution confirmed by A. N. Skiba, accepted in the Kourovka Notebook (21st issue), https://kourovkanotebookorg.wordpress.com/wp-content/uploads/2026/09/kourovka-mathematics.pdf.
Uses 1
Statement usesThe non-modular formation lattice problem (Kourovka 18.92(b), A. N. Skiba)

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

A class of finite groups is a property of finite groups: for each finite group \(G\) it states whether \(G\) belongs to the class.

Closure under isomorphism is not part of the definition.

abbrev FiniteGroupClass : Type 1 := ∀ (G : Type) [Group G] [Finite G], Prop
Used by 7
Used byInclusion of classes of finite groups · Intersection of classes of finite groups · Kourovka Problem 13.51 (Skiba): finite modular lattices embed in the lattice of formations · Join of formations (Kourovka 13.51) · Formation of finite groups (Kourovka 13.51) · Local formation of finite groups · Residual of a finite group with respect to a class

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

A class \(\mathfrak F\) of finite groups is a formation when it is closed under homomorphic images (if \(G \in \mathfrak F\) and \(\varphi : G \to H\) is a surjective homomorphism of finite groups, then \(H \in \mathfrak F\)) and, for every finite group \(G\) and normal subgroups \(N_1\) and \(N_2\) of \(G\), \(G/N_1 \in \mathfrak F\) and \(G/N_2 \in \mathfrak F\) imply \(G/(N_1 \cap N_2) \in \mathfrak F\) (closure under finite subdirect products).

The empty class is a formation.

def IsFormation (𝔉 : FiniteGroupClass) : Prop :=
  (∀ (G H : Type) [Group G] [Finite G] [Group H] [Finite H] (φ : G →* H),
      Function.Surjective φ → 𝔉 G → 𝔉 H) ∧
    ∀ (G : Type) [Group G] [Finite G] (N₁ N₂ : Subgroup G) [N₁.Normal] [N₂.Normal],
      𝔉 (G ⧸ N₁) → 𝔉 (G ⧸ N₂) → 𝔉 (G ⧸ (N₁ ⊓ N₂))
Uses 1 · Used by 3
Statement usesClass of finite groups (Kourovka 13.51)
Used byKourovka Problem 13.51 (Skiba): finite modular lattices embed in the lattice of formations · Join of formations (Kourovka 13.51) · Local formation of finite groups

DefinitionIntersection of classes of finite groups#✓fully proved

For classes \(\mathfrak F_1\) and \(\mathfrak F_2\) of finite groups, their intersection \(\mathfrak F_1 \cap \mathfrak F_2\) is the class of finite groups \(G\) with \(G \in \mathfrak F_1\) and \(G \in \mathfrak F_2\). For formations \(\mathfrak F_1\) and \(\mathfrak F_2\) it is their meet in the lattice of formations.

def classMeet (𝔉₁ 𝔉₂ : FiniteGroupClass) : FiniteGroupClass :=
  fun G _ _ => 𝔉₁ G ∧ 𝔉₂ G
Uses 1 · Used by 1
Statement usesClass of finite groups (Kourovka 13.51)
Used byKourovka Problem 13.51 (Skiba): finite modular lattices embed in the lattice of formations

DefinitionJoin of formations (Kourovka 13.51)#✓fully proved

For classes \(\mathfrak F_1\) and \(\mathfrak F_2\) of finite groups, their formation join is the class of finite groups \(G\) that belong to every formation containing all groups of \(\mathfrak F_1\) and of \(\mathfrak F_2\): the intersection of all formations containing \(\mathfrak F_1 \cup \mathfrak F_2\), which is the smallest such formation. For formations \(\mathfrak F_1\) and \(\mathfrak F_2\) it is their join in the lattice of formations.

def formationJoin (𝔉₁ 𝔉₂ : FiniteGroupClass) : FiniteGroupClass :=
  fun G _ _ => ∀ 𝔉 : FiniteGroupClass, IsFormation 𝔉 →
    (∀ (H : Type) [Group H] [Finite H], 𝔉₁ H ∨ 𝔉₂ H → 𝔉 H) → 𝔉 G
Uses 2 · Used by 1
Statement usesClass of finite groups (Kourovka 13.51) · Formation of finite groups (Kourovka 13.51)
Used byKourovka Problem 13.51 (Skiba): finite modular lattices embed in the lattice of formations

DefinitionKourovka Problem 13.51 (Skiba): finite modular lattices embed in the lattice of formations#✓fully proved

For every finite modular lattice \(L\) there is an injective map \(f\) from \(L\) to the formations of finite groups such that, for all \(a, b \in L\), \(f(a \wedge b) = f(a) \cap f(b)\) and \(f(a \vee b)\) is the smallest formation containing \(f(a) \cup f(b)\).

The map is not required to preserve the least or the greatest element.

def finiteModularLatticeEmbedsInFormations : Prop :=
  ∀ (L : Type) [Lattice L] [IsModularLattice L] [Finite L],
    ∃ f : L → FiniteGroupClass, (∀ a, IsFormation (f a)) ∧ Function.Injective f ∧
      (∀ a b, f (a ⊓ b) = classMeet (f a) (f b)) ∧ ∀ a b, f (a ⊔ b) = formationJoin (f a) (f b)
Uses 4 · Used by 1
Statement usesClass of finite groups (Kourovka 13.51) · Formation of finite groups (Kourovka 13.51) · Intersection of classes of finite groups · Join of formations (Kourovka 13.51)
Used byNot every finite modular lattice embeds in the lattice of formations

TheoremNot every finite modular lattice embeds in the lattice of formations#●ready to prove

There is a finite modular lattice \(L\) that admits no injective map \(f\) from \(L\) to the formations of finite groups such that, for all \(a, b \in L\), \(f(a \wedge b) = f(a) \cap f(b)\) and \(f(a \vee b)\) is the smallest formation containing \(f(a) \cup f(b)\). This answers Kourovka Problem 13.51 (Skiba) in the negative.

Jayadevan constructs a modular lattice with 184 elements that admits no such map (a six-variable Desargues implication holds for formations and fails in the lattice); the Kourovka Notebook (21st issue) answers 13.51 "No, not every" (AI solution confirmed by A. N. Skiba).

public theorem_wanted finiteModularLatticeEmbedsInFormations_refuted :
    ¬ finiteModularLatticeEmbedsInFormations
Sources
  • E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 13.51 (A. N. Skiba); resolution: A. Jayadevan, A finite modular lattice not embeddable in the lattice of formations of finite groups, preprint, Zenodo record 22863019 (2026), main theorem: a modular lattice with 184 elements (the dual of an incidence lattice with 91 points and 91 lines) admits no injective map preserving binary meets and joins into the lattice of formations; the Kourovka Notebook (21st issue) marks 13.51 solved (AI solution confirmed by A. N. Skiba), https://zenodo.org/records/22863019.
Uses 1
Statement usesKourovka Problem 13.51 (Skiba): finite modular lattices embed in the lattice of formations

DefinitionInclusion of classes of finite groups#✓fully proved

For classes \(\mathfrak{F}\) and \(\mathfrak{G}\) of finite groups, \(\mathfrak{F} \subseteq \mathfrak{G}\) means that every finite group in \(\mathfrak{F}\) belongs to \(\mathfrak{G}\).

def ClassLE (𝔉 𝔊 : FiniteGroupClass) : Prop :=
  ∀ (G : Type) [Group G] [Finite G], 𝔉 G → 𝔊 G
Uses 1
Statement usesClass of finite groups (Kourovka 13.51)

DefinitionLocal formation of finite groups#✓fully proved

A class \(\mathfrak{F}\) of finite groups is a local formation when it is a formation, contains the trivial group, and is saturated: a finite group \(G\) belongs to \(\mathfrak{F}\) whenever \(G/\Phi(G)\) does, where \(\Phi(G)\) is the Frattini subgroup of \(G\).

By the Gaschütz-Lubeseder-Schmid theorem a nonempty formation of finite groups is local (defined by a formation function) iff it is saturated.

def IsLocalFormation (𝔉 : FiniteGroupClass) : Prop :=
  IsFormation 𝔉 ∧ 𝔉 Unit ∧ ∀ (G : Type) [Group G] [Finite G], 𝔉 (G ⧸ frattini G) → 𝔉 G
Uses 2
Statement usesClass of finite groups (Kourovka 13.51) · Formation of finite groups (Kourovka 13.51)

DefinitionResidual of a finite group with respect to a class#✓fully proved

For a class \(\mathfrak{F}\) of finite groups and a finite group \(G\), the \(\mathfrak{F}\)-residual \(G^{\mathfrak{F}}\) is the intersection of all normal subgroups \(N\) of \(G\) with \(G/N \in \mathfrak{F}\).

For a formation containing the trivial group it is the smallest such \(N\).

def residual (𝔉 : FiniteGroupClass) (G : Type) [Group G] [Finite G] : Subgroup G :=
  ⨅ (N : Subgroup G) (_ : N.Normal) (_ : 𝔉 (G ⧸ N)), N
Uses 1
Statement usesClass of finite groups (Kourovka 13.51)

AbbreviationClasses of finite groups (Kourovka 10.56)#✓fully proved

A class of finite groups is given by its membership predicate: a proposition about each finite group, true exactly for the members of the class.

abbrev GroupClass : Type 1 :=
  ∀ (G : Type) [Group G] [Finite G], Prop
Used by 5
Used byFormation generated by two classes (Kourovka 10.56) · Formations of finite groups (Kourovka 10.56) · Formations of nilpotent groups of class at most 4 · Intersection of classes of finite groups (Kourovka 10.56) · The distributivity question for nilpotent class-4 formations (Kourovka 10.56)

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

A class \(X\) of finite groups is a formation if it is closed under isomorphism, contains the trivial group, contains \(G/N\) whenever it contains \(G\) and \(N\) is a normal subgroup of \(G\), and is closed under subdirect products: if \(N_1\) and \(N_2\) are normal subgroups of a finite group \(G\) with \(G/N_1 \in X\) and \(G/N_2 \in X\), then \(G/(N_1 \cap N_2) \in X\).

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 2
Statement usesClasses of finite groups (Kourovka 10.56)
Used byFormation generated by two classes (Kourovka 10.56) · Formations of nilpotent groups of class at most 4

DefinitionFormations of nilpotent groups of class at most 4#✓fully proved

A class \(X\) of finite groups is a formation of nilpotent groups of class at most \(4\) if \(X\) is a formation and every group \(G\) in \(X\) is nilpotent of class at most \(4\), that is, the fourth term \(\zeta_4(G)\) of the upper central series of \(G\) is all of \(G\).

def IsNilpotentClassFourFormation (X : GroupClass) : Prop :=
  IsFormation X ∧ ∀ (G : Type) [Group G] [Finite G], X G → Subgroup.upperCentralSeries G 4 = ⊤
Uses 2 · Used by 1
Statement usesClasses of finite groups (Kourovka 10.56) · Formations of finite groups (Kourovka 10.56)
Used byThe distributivity question for nilpotent class-4 formations (Kourovka 10.56)

DefinitionIntersection of classes of finite groups (Kourovka 10.56)#✓fully proved

The meet of two classes \(X\) and \(Y\) of finite groups is their intersection \(X \cap Y\): the class of finite groups that belong to both \(X\) and \(Y\).

def meet (X Y : GroupClass) : GroupClass :=
  fun G _ _ => X G ∧ Y G
Uses 1 · Used by 1
Statement usesClasses of finite groups (Kourovka 10.56)
Used byThe distributivity question for nilpotent class-4 formations (Kourovka 10.56)

DefinitionFormation generated by two classes (Kourovka 10.56)#✓fully proved

For classes \(X\) and \(Y\) of finite groups, the formation generated by \(X \cup Y\) is the class of finite groups that belong to every formation containing both \(X\) and \(Y\). For formations \(X\) and \(Y\) it is their join in the lattice of formations.

def formationJoin (X Y : GroupClass) : GroupClass :=
  fun G _ _ => ∀ Z : GroupClass, IsFormation Z → (∀ (H : Type) [Group H] [Finite H], X H → Z H) →
    (∀ (H : Type) [Group H] [Finite H], Y H → Z H) → Z G
Uses 2 · Used by 1
Statement usesClasses of finite groups (Kourovka 10.56) · Formations of finite groups (Kourovka 10.56)
Used byThe distributivity question for nilpotent class-4 formations (Kourovka 10.56)

DefinitionThe distributivity question for nilpotent class-4 formations (Kourovka 10.56)#✓fully proved

For all formations \(A\), \(B\), \(C\) of finite nilpotent groups of class at most \(4\), a finite group lies in \(A \cap (B \vee C)\) if and only if it lies in \((A \cap B) \vee (A \cap C)\), where \(X \vee Y\) denotes the formation generated by \(X \cup Y\). That is, the lattice of formations of finite nilpotent groups of class at most \(4\) is distributive (A. N. Skiba).

def nilpotentClassFourFormationsDistributive : Prop :=
  ∀ A B C : GroupClass, IsNilpotentClassFourFormation A → IsNilpotentClassFourFormation B →
    IsNilpotentClassFourFormation C → ∀ (G : Type) [Group G] [Finite G],
      (A G ∧ formationJoin B C G) ↔ formationJoin (meet A B) (meet A C) G
Uses 4 · Used by 1
Statement usesClasses of finite groups (Kourovka 10.56) · Formations of nilpotent groups of class at most 4 · Formation generated by two classes (Kourovka 10.56) · Intersection of classes of finite groups (Kourovka 10.56)
Used byThe lattice of nilpotent class-4 formations is not distributive (Kourovka 10.56)

TheoremThe lattice of nilpotent class-4 formations is not distributive (Kourovka 10.56)#●ready to prove

There exist formations \(A\), \(B\), \(C\) of finite nilpotent groups of class at most \(4\) such that the classes \(A \cap (B \vee C)\) and \((A \cap B) \vee (A \cap C)\) differ, that is, some finite group lies in exactly one of them; here \(X \vee Y\) denotes the formation generated by \(X \cup Y\), the intersection of all formations containing \(X\) and \(Y\).

The Kourovka Archive answers Problem 10.56 "No": the lattice of varieties of nilpotent \(2\)-groups of class at most \(4\) is not distributive (Belov; Bryce), and \(\mathfrak{V} \mapsto \mathfrak{V} \cap \mathfrak{F}\), where \(\mathfrak{F}\) is the class of finite groups, embeds it in the lattice of formations (Kovács), with image among the formations of finite nilpotent groups of class at most \(4\).

public theorem_wanted nilpotentClassFourFormationsDistributive_refuted :
    ¬ nilpotentClassFourFormationsDistributive
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.56 (A. N. Skiba); resolution: Yu. A. Belov, Algebra and Logic 9, no. 6 (1970), 371-374; R. A. Bryce, Philos. Trans. Roy. Soc. London (A) 266 (1970), 281-355, footnote on p. 335; L. Kovács, letter of 12 May 1988, Kourovka Archive, Problem 10.56 ("No"): the lattice of varieties of nilpotent 2-groups of class ≤ 4 is non-distributive, and V ↦ V ∩ F embeds it in the lattice of formations.
Uses 1
Statement usesThe distributivity question for nilpotent class-4 formations (Kourovka 10.56)
24 fully proved4 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.