Products of abelian and locally quaternion groups

DefinitionLocally quaternion subgroup#✓fully proved

A subgroup \(B\) of a group \(G\) is locally quaternion if there is a strictly increasing sequence \(C_0 < C_1 < C_2 < \cdots\) of subgroups of \(G\), each isomorphic to a generalized quaternion group \(Q_{2^{k+2}}\) of order \(2^{k+2}\) for some \(k \ge 1\), whose supremum (for a chain, the union) is \(B\). In particular \(B\) is infinite.

def IsLocallyQuaternion {G : Type} [Group G] (B : Subgroup G) : Prop :=
  ∃ Q : ℕ → Subgroup G, StrictMono Q ∧
    (∀ i, ∃ k : ℕ, 1 ≤ k ∧ Nonempty (Q i ≃* QuaternionGroup (2 ^ k))) ∧ B = ⨆ i, Q i

Used by 1

Used byKourovka Problem 18.95 (Sozutov)

DefinitionKourovka Problem 18.95 (Sozutov)#✓fully proved

The proposition that every group \(G\) with subgroups \(A\) and \(B\) such that \(A\) is abelian, \(B\) is locally quaternion, and \(G = AB\) (every element of \(G\) is a product \(ab\) with \(a \in A\) and \(b \in B\)) is soluble.

def abelianLocallyQuaternionProductSoluble : Prop :=
  ∀ (G : Type) [Group G] (A B : Subgroup G), (∀ x ∈ A, ∀ y ∈ A, x * y = y * x) →
    IsLocallyQuaternion B → (A : Set G) * (B : Set G) = Set.univ → Group.IsSolvable G

Uses 1 · Used by 1

Statement usesLocally quaternion subgroup

Used byProducts of abelian and locally quaternion groups are soluble

TheoremProducts of abelian and locally quaternion groups are soluble#●ready to prove

Let \(G\) be a group with subgroups \(A\) and \(B\) such that \(A\) is abelian, \(B\) is locally quaternion, and \(G = AB\), that is, every element of \(G\) is a product \(ab\) with \(a \in A\) and \(b \in B\). Then \(G\) is soluble.

public theorem_wanted abelianLocallyQuaternionProductSoluble_holds :
    abelianLocallyQuaternionProductSoluble

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 18.95 (A. I. Sozutov); resolution: B. Amberg and Ya. Sysak, On products of groups with abelian subgroups of small index, J. Group Theory 20 (2017), no. 6, 1061-1072, Kourovka Archive, Problem 18.95: Yes, it is; Corollary 1.2 (arXiv:1611.10093): if a group G = AB is the product of an abelian subgroup A and a locally quaternion subgroup B, then G is soluble (Theorem 1.1: derived length at most 3), https://arxiv.org/abs/1611.10093.

Uses 1

Statement usesKourovka Problem 18.95 (Sozutov)

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.