Monsters of the first kind

DefinitionMonster of the first kind#✓fully proved

A group \(G\) is a monster of the first kind (V. P. Shunkov) when \(G\) is infinite, \(G\) has an element of order greater than \(2\), and for every element \(a\) of order greater than \(2\) and every proper subgroup \(H\) of \(G\) there is \(g \in G \setminus H\) such that \(a\) and \(g^{-1} a g\) generate \(G\). Here an element of infinite order counts as having order greater than \(2\).

def IsMonsterFirstKind (G : Type*) [Group G] : Prop :=
  Infinite G ∧ (∃ a : G, orderOf a ∉ ({1, 2} : Set ℕ)) ∧
    ∀ a : G, orderOf a ∉ ({1, 2} : Set ℕ) → ∀ H : Subgroup G, H ≠ ⊤ →
      ∃ g ∉ H, Subgroup.closure {a, g⁻¹ * a * g} = ⊤

Used by 1

Used byShunkov's question on central extensions of monsters

DefinitionShunkov's question on central extensions of monsters#✓fully proved

Kourovka Problem 14.104 (V. P. Shunkov) asks whether this proposition holds: for every monster of the first kind \(M\) there are a torsion-free group \(E\) and a cyclic subgroup \(C\) contained in the center of \(E\) such that \(E / C \cong M\).

def monsterHasTorsionFreeCyclicCentralExtension : Prop :=
  ∀ (M : Type) [Group M], IsMonsterFirstKind M →
    ∃ (E : Type) (_ : Group E) (C : Subgroup E), (∀ x : E, x ≠ 1 → ¬ IsOfFinOrder x) ∧
      C ≤ Subgroup.center E ∧ IsCyclic C ∧ ∃ _ : C.Normal, Nonempty (E ⧸ C ≃* M)

def IsMonsterFirstKind (G : Type*) [Group G] : Prop :=
  Infinite G ∧ (∃ a : G, orderOf a ∉ ({1, 2} : Set ℕ)) ∧
    ∀ a : G, orderOf a ∉ ({1, 2} : Set ℕ) → ∀ H : Subgroup G, H ≠ ⊤ →
      ∃ g ∉ H, Subgroup.closure {a, g⁻¹ * a * g} = ⊤

WantedExt/GroupTheory/MonsterTorsionFreeCentralExtensionKourovka14Problem104Wanted.lean:42

Uses 1 · Used by 1

Statement usesMonster of the first kind

Used byNot every monster of the first kind is a torsion-free group modulo a central cyclic subgroup

TheoremNot every monster of the first kind is a torsion-free group modulo a central cyclic subgroup#●ready to prove

It is not the case that for every monster of the first kind \(M\) there are a torsion-free group \(E\) and a cyclic subgroup \(C\) contained in the center of \(E\) with \(E / C \cong M\). So Kourovka Problem 14.104 has a negative answer.

The Kourovka Archive answers 14.104 "No, not always" (A. I. Sozutov): if a torsion-free group \(E\) has a central cyclic subgroup \(C\) with \(E / C \cong M\), then every finite subgroup of \(M\) is cyclic, and some monsters of the first kind have non-cyclic finite subgroups.

public theorem_wanted monsterHasTorsionFreeCyclicCentralExtension_refuted :
    ¬ monsterHasTorsionFreeCyclicCentralExtension

def monsterHasTorsionFreeCyclicCentralExtension : Prop :=
  ∀ (M : Type) [Group M], IsMonsterFirstKind M →
    ∃ (E : Type) (_ : Group E) (C : Subgroup E), (∀ x : E, x ≠ 1 → ¬ IsOfFinOrder x) ∧
      C ≤ Subgroup.center E ∧ IsCyclic C ∧ ∃ _ : C.Normal, Nonempty (E ⧸ C ≃* M)

WantedExt/GroupTheory/MonsterTorsionFreeCentralExtensionKourovka14Problem104Wanted.lean:49

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 14.104 (V. P. Shunkov); resolution: A. I. Sozutov, letter of 20 November 2001, Kourovka Archive, Problem 14.104: such an extension forces every finite subgroup of the monster to be cyclic, which fails for some monsters (answer: No, not always).

Uses 1

Statement usesShunkov's question on central extensions of monsters

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.