Φ-extensions of p-groups

Definition\(\Phi\)-extension (Berkovich)#✓fully proved

For a natural number \(p\) and groups \(H\) and \(G\), \(H\) is a \(\Phi\)-extension of \(G\) when \(H\) is a finite \(p\)-group with a normal subgroup \(N\) of order \(p\) such that \(N \le \Phi(H)\), where \(\Phi(H)\) is the Frattini subgroup of \(H\), and \(H/N \cong G\).

def IsPhiExtension (p : ℕ) (H G : Type) [Group H] [Group G] : Prop :=
  Finite H ∧ IsPGroup p H ∧ ∃ N : Subgroup H, ∃ _ : N.Normal,
    Nat.card N = p ∧ N ≤ frattini H ∧ Nonempty (H ⧸ N ≃* G)

Used by 1

Used byKourovka Problem 16.12 (infinite chains of \(\Phi\)-extensions)

DefinitionKourovka Problem 16.12 (infinite chains of \(\Phi\)-extensions)#✓fully proved

The statement, a question of Ya. G. Berkovich, that for every prime \(p\) and every nontrivial finite \(p\)-group \(G\) there are groups \(G_0, G_1, G_2, \dots\) with \(G_0 \cong G\) such that, for every \(i \ge 0\), \(G_{i+1}\) is a \(\Phi\)-extension of \(G_i\) for the prime \(p\).

def phiExtensionSequence : Prop :=
  ∀ p : ℕ, p.Prime → ∀ (G : Type) [Group G] [Finite G], IsPGroup p G → Nontrivial G →
    ∃ (S : ℕ → Type) (_ : ∀ i, Group (S i)), Nonempty (S 0 ≃* G) ∧
      ∀ i, IsPhiExtension p (S (i + 1)) (S i)

Uses 1 · Used by 1

Statement uses\(\Phi\)-extension (Berkovich)

Used byInfinite chains of \(\Phi\)-extensions (Kourovka 16.12)

TheoremInfinite chains of \(\Phi\)-extensions (Kourovka 16.12)#●ready to prove

For every prime \(p\) and every nontrivial finite \(p\)-group \(G\) there are groups \(G_0, G_1, G_2, \dots\) with \(G_0 \cong G\) such that, for every \(i \ge 0\), \(G_{i+1}\) is a \(\Phi\)-extension of \(G_i\) for the prime \(p\). This answers Kourovka Problem 16.12 in the affirmative: the Kourovka Archive answers "Yes, it is", citing Kamornikov (2008).

The trivial group is excluded: it has no \(\Phi\)-extension, since a group of order \(p\) has trivial Frattini subgroup.

public theorem_wanted phiExtensionSequence_holds : phiExtensionSequence

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.12 (Ya. G. Berkovich); resolution: S. F. Kamornikov, Izv. Gomel' Univ. 5 (2008), 200-201 (Russian), Kourovka Archive, Problem 16.12 (Yes, it is).

Uses 1

Statement usesKourovka Problem 16.12 (infinite chains of \(\Phi\)-extensions)

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.