Injectors of Fitting classes

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

A class of groups is a property of groups that is closed under isomorphism: if a group \(H\) has the property and \(K\) is a group isomorphic to \(H\), then \(K\) has it too.

Only finite members matter for Fitting classes and for injectors of finite groups.

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 4

Used byKourovka Problem 12.96: a Fitting class without injectors · Fitting classes of finite groups · Injectors · Maximal subgroups within a class of groups

DefinitionFitting classes of finite groups#✓fully proved

A class \(\mathfrak{X}\) of groups is a Fitting class of finite groups if, for every finite group \(G\), every normal subgroup of \(G\) lies in \(\mathfrak{X}\) whenever \(G\) does, and the product \(N_1 N_2\) of two normal subgroups \(N_1\) and \(N_2\) of \(G\) lies in \(\mathfrak{X}\) whenever \(N_1\) and \(N_2\) do.

def IsFitting (X : GroupClass) : Prop :=
  (∀ (G : Type) [Group G] [Finite G] (N : Subgroup G), N.Normal → X.mem G → X.mem N) ∧
  ∀ (G : Type) [Group G] [Finite G] (N₁ N₂ : Subgroup G), N₁.Normal → N₂.Normal →
    X.mem N₁ → X.mem N₂ → X.mem ↥(N₁ ⊔ N₂)

Uses 1 · Used by 1

Statement usesIsomorphism-closed classes of groups (Kourovka 12.96)

Used byKourovka Problem 12.96: a Fitting class without injectors

DefinitionMaximal subgroups within a class of groups#✓fully proved

Let \(\mathfrak{X}\) be a class of groups and let \(V\) and \(K\) be subgroups of a group \(G\). Then \(V\) is \(\mathfrak{X}\)-maximal in \(K\) if \(V \le K\), \(V\) lies in \(\mathfrak{X}\), and no subgroup \(W\) of \(G\) with \(V < W \le K\) lies in \(\mathfrak{X}\).

def IsXMaximalIn (X : GroupClass) {G : Type} [Group G] (V K : Subgroup G) : Prop :=
  V ≤ K ∧ X.mem V ∧ ∀ W : Subgroup G, V < W → W ≤ K → ¬ X.mem W

Uses 1 · Used by 1

Statement usesIsomorphism-closed classes of groups (Kourovka 12.96)

Used byInjectors

DefinitionInjectors#✓fully proved

Let \(\mathfrak{X}\) be a class of groups and \(G\) a group. A subgroup \(V\) of \(G\) is an \(\mathfrak{X}\)-injector of \(G\) if, for every subnormal subgroup \(N\) of \(G\), the intersection \(V \cap N\) is \(\mathfrak{X}\)-maximal in \(N\).

def IsInjector (X : GroupClass) {G : Type} [Group G] (V : Subgroup G) : Prop :=
  ∀ N : Subgroup G, N.IsSubnormal → IsXMaximalIn X (V ⊓ N) N

Uses 2 · Used by 1

Statement usesIsomorphism-closed classes of groups (Kourovka 12.96) · Maximal subgroups within a class of groups

Used byKourovka Problem 12.96: a Fitting class without injectors

DefinitionKourovka Problem 12.96: a Fitting class without injectors#✓fully proved

The statement that there are a Fitting class \(\mathfrak{X}\) of finite groups that contains at least one finite group and a finite non-soluble group \(G\) such that no subgroup of \(G\) is an \(\mathfrak{X}\)-injector of \(G\).

The problem was posed by L. A. Shemetkov.

def fittingClassWithoutInjectors : Prop :=
  ∃ X : GroupClass, IsFitting X ∧ (∃ (H : Type) (_ : Group H) (_ : Finite H), X.mem H) ∧
    ∃ (G : Type) (_ : Group G) (_ : Finite G), ¬ Group.IsSolvable G ∧
      ∀ V : Subgroup G, ¬ IsInjector X V

Uses 3 · Used by 1

Statement usesIsomorphism-closed classes of groups (Kourovka 12.96) · Fitting classes of finite groups · Injectors

Used byA Fitting class with no injectors in a non-soluble group

TheoremA Fitting class with no injectors in a non-soluble group#●ready to prove

There are a Fitting class \(\mathfrak{X}\) of finite groups that contains at least one finite group and a finite non-soluble group \(G\) such that no subgroup of \(G\) is an \(\mathfrak{X}\)-injector of \(G\).

This answers Kourovka Problem 12.96 (L. A. Shemetkov) affirmatively: the Kourovka Archive records that E. Salomon found such a Fitting class and group; the example is presented in Section 7.1 of Ballester-Bolinches and Ezquerro, Classes of finite groups (2006).

public theorem_wanted fittingClassWithoutInjectors_holds : fittingClassWithoutInjectors

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.96 (L. A. Shemetkov); resolution: E. Salomon (unpublished), presented in A. Ballester-Bolinches and L. M. Ezquerro, Classes of finite groups, Springer, 2006, Section 7.1, Kourovka Archive, Problem 12.96: found by E. Salomon.

Uses 1

Statement usesKourovka Problem 12.96: a Fitting class without injectors

5 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.