Self-extensions of groups

DefinitionHall group#✓fully proved

A group \(G\) is a Hall group (in the sense of Göbel and Shelah) when it is isomorphic to every extension of itself by itself: for every group \(H\) and every normal subgroup \(N\) of \(H\) with \(N \cong G\) and \(H/N \cong G\), also \(H \cong G\).

def IsHallGroup (G : Type) [Group G] : Prop :=
  ∀ (H : Type) [Group H] (N : Subgroup H) [N.Normal],
    Nonempty (N ≃* G) → Nonempty ((H ⧸ N) ≃* G) → Nonempty (H ≃* G)

Used by 1

Used byHall's problem on self-extensions (Kourovka Problem 12.44)

DefinitionHall's problem on self-extensions (Kourovka Problem 12.44)#✓fully proved

There is a nontrivial group \(G\) that is a Hall group, that is, isomorphic to every extension of itself by itself: every group \(H\) with a normal subgroup \(N \cong G\) such that \(H/N \cong G\) is isomorphic to \(G\).

def existsGroupIsoToSelfExtensions : Prop :=
  ∃ (G : Type) (_ : Group G), Nontrivial G ∧ IsHallGroup G

def IsHallGroup (G : Type) [Group G] : Prop :=
  ∀ (H : Type) [Group H] (N : Subgroup H) [N.Normal],
    Nonempty (N ≃* G) → Nonempty ((H ⧸ N) ≃* G) → Nonempty (H ≃* G)

WantedExt/GroupTheory/HallGroupSelfExtensionKourovka12Problem44Wanted.lean:39

Uses 1 · Used by 1

Statement usesHall group

Used byExistence of Hall groups (Göbel–Shelah; Kourovka Problem 12.44)

TheoremExistence of Hall groups (Göbel–Shelah; Kourovka Problem 12.44)#●ready to prove

There is a nontrivial group \(G\) that is isomorphic to every extension of itself by itself: every group \(H\) with a normal subgroup \(N \cong G\) such that \(H/N \cong G\) is isomorphic to \(G\).

public theorem_wanted existsGroupIsoToSelfExtensions_holds : existsGroupIsoToSelfExtensions

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.44 (P. Hall; J. C. Lennox); resolution: R. Göbel and S. Shelah, Philip Hall's problem on non-Abelian splitters, Math. Proc. Cambridge Philos. Soc. 134 (2003), no. 1, 23-31, arXiv:math/0009091, Definition 1.1 and Corollary 1.5 (L^ω is a Hall group for every rigid group L), with the existence of rigid groups (Theorem 3.1); Kourovka Archive, Problem 12.44, https://arxiv.org/abs/math/0009091.

Uses 1

Statement usesHall's problem on self-extensions (Kourovka Problem 12.44)

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.