σ-solubility, σ-nilpotency and σ-subnormality

DefinitionChief factors#✓fully proved

For subgroups \(A\) and \(B\) of a group \(G\), \(A / B\) is a chief factor of \(G\) if \(A\) and \(B\) are normal in \(G\), \(B < A\), and every normal subgroup \(N\) of \(G\) with \(B \le N \le A\) equals \(B\) or \(A\).

def IsChiefFactor {G : Type*} [Group G] (A B : Subgroup G) : Prop :=
  A.Normal ∧ B.Normal ∧ B < A ∧ ∀ N : Subgroup G, N.Normal → B ≤ N → N ≤ A → N = B ∨ N = A

Used by 4

Used byComplemented chief factor · Frattini chief factor · \(\sigma\)-soluble groups · Chief factor of rank above a bound

DefinitionGroups of Fitting height at most \(h\)#✓fully proved

For a natural number \(h\), a group \(G\) has Fitting height (nilpotent length) at most \(h\) if there are normal subgroups \(1 = G_0 \le G_1 \le \cdots \le G_h = G\) of \(G\) such that for every \(i < h\) some term of the lower central series of \(G_{i+1}\) lies in \(G_i\), that is, \(G_{i+1} / G_i\) is nilpotent.

def FittingHeightLE (G : Type*) [Group G] (h : ℕ) : Prop :=
  ∃ s : ℕ → Subgroup G, s 0 = ⊥ ∧ s h = ⊤ ∧ ∀ i < h, (s i).Normal ∧ s i ≤ s (i + 1) ∧
    ∃ c : ℕ, (s (i + 1)).lowerCentralSeries c ≤ s i

Used by 2

Used byKourovka Problem 19.43: Fitting height, automorphism order and centralizer size · Kourovka 19.55(b) (Monakhov): unbounded Fitting height

DefinitionComposition factors via subnormal subgroups#✓fully proved

A group \(S\) is a composition factor of a group \(K\) if \(S\) is simple and some subnormal subgroup \(H\) of \(K\) has a surjective homomorphism onto \(S\).

For finite \(K\) this is the same as \(S\) occurring as a factor of a composition series of \(K\) (refine the subnormal chain through the kernel).

def IsCompositionFactor (S K : Type*) [Group S] [Group K] : Prop :=
  IsSimpleGroup S ∧ ∃ H : Subgroup K, H.IsSubnormal ∧ ∃ f : H →* S, Function.Surjective f

Used by 2

Used byKourovka Problem 19.67 · Kourovka 19.55(a) (Monakhov): every non-abelian simple group occurs

DefinitionConjugacy separable groups#✓fully proved

A group \(G\) is conjugacy separable if any two elements \(x, y \in G\) whose images are conjugate in every quotient \(G / N\) by a normal subgroup \(N\) of finite index (that is, \(g x g^{-1} y^{-1} \in N\) for some \(g \in G\)) are conjugate in \(G\).

def IsConjugacySeparable (G : Type*) [Group G] : Prop :=
  ∀ x y : G, (∀ N : Subgroup G, N.Normal → N.FiniteIndex → ∃ g : G, g * x * g⁻¹ * y⁻¹ ∈ N) →
    IsConj x y

Used by 1

Used byKapovich's conjugacy separability question (Kourovka 19.41)

DefinitionResidually finite \(p\)-groups#✓fully proved

For a natural number \(p\), a group \(G\) is residually a finite \(p\)-group if every element \(g \ne 1\) of \(G\) lies outside some normal subgroup of \(G\) whose index is \(p^k\) for some \(k \ge 0\), where an infinite index counts as \(0\).

This notion appears in Kourovka Notebook problems 1.84, 4.52 and 10.30.

def IsResiduallyFiniteP (p : ℕ) (G : Type*) [Group G] : Prop :=
  ∀ g : G, g ≠ 1 → ∃ N : Subgroup G, N.Normal ∧ (∃ k : ℕ, N.index = p ^ k) ∧ g ∉ N

Used by 1

Used byMedvedev's question on right-orderability (Kourovka 10.30)

DefinitionRestricted wreath product#✓fully proved

For groups \(A\) and \(B\), let \(A \wr_r B = A^B \rtimes B\) be the regular (unrestricted) wreath product, where \(A^B\) is the group of all functions \(f : B \to A\) and \(b \in B\) acts on it by \((b \cdot f)(x) = f(b^{-1} x)\). The restricted wreath product \(A \wr B\) is the subgroup of \(A \wr_r B\) generated by the elements \((f, b)\) whose function part \(f\) has finite support, that is, \(f(x) \ne 1\) for only finitely many \(x \in B\).

These elements already form a subgroup, and for finite \(B\) it is all of \(A \wr_r B\).

def restrictedWreath (A B : Type*) [Group A] [Group B] : Subgroup (A ≀ᵣ B) :=
  Subgroup.closure {x | {b : B | x.left b ≠ 1}.Finite}

DefinitionPartitions of the primes#✓fully proved

A family \(\sigma = (\sigma_i)_{i \in I}\) of sets of natural numbers is a partition of the primes if every \(\sigma_i\) is a nonempty set of primes, \(\sigma_i\) and \(\sigma_j\) are disjoint whenever \(i \ne j\), and every prime lies in some \(\sigma_i\).

def IsPrimePartition {I : Type} (σ : I → Set ℕ) : Prop :=
  (∀ i, (σ i).Nonempty ∧ ∀ p ∈ σ i, p.Prime) ∧ (∀ i j, i ≠ j → Disjoint (σ i) (σ j)) ∧
    ∀ p : ℕ, p.Prime → ∃ i, p ∈ σ i

Used by 4

Used byClaim of Kourovka Problem 19.85 · Skiba's \(\sigma\)-subnormality question (Kourovka 19.84) · Kourovka Problem 19.88 (statement) · Kourovka Problem 19.87 (statement)

Definition\(\sigma\)-primary numbers#✓fully proved

For a family \(\sigma = (\sigma_i)_{i \in I}\) of sets of natural numbers, a natural number \(n\) is \(\sigma\)-primary if there is an index \(i\) such that every prime divisor of \(n\) lies in \(\sigma_i\). For \(n = 0\) this means that some \(\sigma_i\) contains every prime.

A finite group is called \(\sigma\)-primary when its order is.

def IsSigmaPrimary {I : Type} (σ : I → Set ℕ) (n : ℕ) : Prop :=
  ∃ i, ∀ p : ℕ, p.Prime → p ∣ n → p ∈ σ i

Used by 3

Used by\(\sigma\)-nilpotent groups · \(\sigma\)-soluble groups · \(\sigma\)-subnormal subgroups

Definition\(\sigma\)-subnormal subgroups#✓fully proved

For a family \(\sigma = (\sigma_i)_{i \in I}\) of sets of natural numbers, a subgroup \(A\) of a group \(G\) is \(\sigma\)-subnormal in \(G\) if there is a chain of subgroups \(A = A_0 \le A_1 \le \cdots \le A_n = G\) such that for every \(i < n\) either \(A_i\) is normal in \(A_{i+1}\), or the index in \(A_{i+1}\) of the normal core of \(A_i\) in \(A_{i+1}\) is \(\sigma\)-primary (an infinite index counts as \(0\)).

def IsSigmaSubnormal {I : Type} (σ : I → Set ℕ) {G : Type*} [Group G] (A : Subgroup G) : Prop :=
  ∃ (n : ℕ) (K : ℕ → Subgroup G), K 0 = A ∧ K n = ⊤ ∧ ∀ i < n, K i ≤ K (i + 1) ∧
    (((K i).subgroupOf (K (i + 1))).Normal ∨
      IsSigmaPrimary σ ((K i).subgroupOf (K (i + 1))).normalCore.index)

Uses 1 · Used by 2

Statement uses\(\sigma\)-primary numbers

Used byClaim of Kourovka Problem 19.85 · Skiba's \(\sigma\)-subnormality question (Kourovka 19.84)

Definition\(\sigma\)-nilpotent groups#✓fully proved

For a family \(\sigma = (\sigma_i)_{i \in I}\) of sets of natural numbers, a group \(G\) is \(\sigma\)-nilpotent if it is the internal direct product of finitely many normal subgroups \(H_1, \dots, H_t\) whose orders are \(\sigma\)-primary (the order of an infinite subgroup counts as \(0\)): the \(H_k\) generate \(G\), and each \(H_k\) meets the subgroup generated by the others trivially.

def IsSigmaNilpotent {I : Type} (σ : I → Set ℕ) (G : Type*) [Group G] : Prop :=
  ∃ (t : ℕ) (H : Fin t → Subgroup G), (∀ k, (H k).Normal ∧ IsSigmaPrimary σ (Nat.card (H k))) ∧
    (⨆ k, H k) = ⊤ ∧ ∀ k, H k ⊓ (⨆ j ∈ ({k}ᶜ : Set (Fin t)), H j) = ⊥

Uses 1 · Used by 2

Statement uses\(\sigma\)-primary numbers

Used byClaim of Kourovka Problem 19.85 · Kourovka Problem 19.88 (statement)

Definition\(\sigma\)-soluble groups#✓fully proved

For a family \(\sigma = (\sigma_i)_{i \in I}\) of sets of natural numbers, a group \(G\) is \(\sigma\)-soluble if for every chief factor \(A / B\) of \(G\) the index \(|A : B|\) is \(\sigma\)-primary (an infinite index counts as \(0\)).

def IsSigmaSoluble {I : Type} (σ : I → Set ℕ) (G : Type*) [Group G] : Prop :=
  ∀ A B : Subgroup G, IsChiefFactor A B → IsSigmaPrimary σ (B.relIndex A)

Uses 2 · Used by 1

Statement usesChief factors · \(\sigma\)-primary numbers

Used byKourovka Problem 19.87 (statement)

DefinitionSkiba's \(\sigma\)-subnormality question (Kourovka 19.84)#✓fully proved

The statement that for every partition \(\sigma\) of the set of primes, every finite group \(G\) and every subgroup \(A\) of \(G\), if \(A\) is \(\sigma\)-subnormal in the subgroup \(\langle A, A^x \rangle\) generated by \(A\) and \(A^x = xAx^{-1}\) for every \(x \in G\), then \(A\) is \(\sigma\)-subnormal in \(G\).

def sigmaSubnormalFromJoinsWithConjugates : Prop :=
  ∀ (I : Type) (σ : I → Set ℕ), IsPrimePartition σ → ∀ (G : Type) [Group G] [Finite G]
    (A : Subgroup G),
    (∀ x : G, IsSigmaSubnormal σ (A.subgroupOf (A ⊔ A.map (MulAut.conj x).toMonoidHom))) →
    IsSigmaSubnormal σ A

Uses 2 · Used by 1

Statement usesPartitions of the primes · \(\sigma\)-subnormal subgroups

Used byA counterexample to Skiba's \(\sigma\)-subnormality question

TheoremA counterexample to Skiba's \(\sigma\)-subnormality question#●ready to prove

The statement of Kourovka Problem 19.84 is false: there are a partition \(\sigma\) of the set of primes, a finite group \(G\) and a subgroup \(A\) of \(G\) such that \(A\) is \(\sigma\)-subnormal in the subgroup \(\langle A, A^x \rangle\) generated by \(A\) and \(A^x = xAx^{-1}\) for every \(x \in G\), but \(A\) is not \(\sigma\)-subnormal in \(G\).

Tyutyanov's example is \(G = S_5\), a partition with blocks \(\{2, 3\}\) and \(\{5\}\), and \(A = \langle (1\,2) \rangle\). Wielandt's theorem gives the affirmative answer for the partition into single primes.

public theorem_wanted sigmaSubnormalFromJoinsWithConjugates_refuted :
    ¬ sigmaSubnormalFromJoinsWithConjugates

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 19.84 (A. N. Skiba); resolution: V. N. Tyutyanov, letter of 28 August 2019, Kourovka Archive, Problem 19.84: No, not always; in G = S₅ with σ = {2, 3} ∪ {5} the subgroup A = ⟨(12)⟩ is σ-subnormal in ⟨A, A^x⟩ for every x but not σ-subnormal in G, https://arxiv.org/abs/1401.0300v49.

Uses 1

Statement usesSkiba's \(\sigma\)-subnormality question (Kourovka 19.84)

12 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.