3-transposition groups

DefinitionSet of 3-transpositions#✓fully proved

A subset \(D\) of a group \(G\) is a set of 3-transpositions when it is closed under conjugation (\(g d g^{-1} \in D\) for all \(g \in G\) and \(d \in D\)), every \(d \in D\) is an involution (\(d \ne 1\) and \(d^2 = 1\)), and for all \(d, e \in D\) the product \(de\) has order at most \(3\), that is, \(de = 1\), \((de)^2 = 1\) or \((de)^3 = 1\).

def IsThreeTranspositionSet {G : Type*} [Group G] (D : Set G) : Prop :=
  (∀ g : G, ∀ d ∈ D, g * d * g⁻¹ ∈ D) ∧ (∀ d ∈ D, d ≠ 1 ∧ d ^ 2 = 1) ∧
    ∀ d ∈ D, ∀ e ∈ D, d * e = 1 ∨ (d * e) ^ 2 = 1 ∨ (d * e) ^ 3 = 1

Used by 1

Used bySozutov's question on 3-transposition groups (Kourovka 12.76)

DefinitionLocally finite group, via finite subsets#✓fully proved

A group \(G\) is locally finite when every finite subset \(S \subseteq G\) generates a finite subgroup; equivalently, every finitely generated subgroup of \(G\) is finite.

def IsLocallyFinite (G : Type*) [Group G] : Prop :=
  ∀ S : Set G, S.Finite → (Subgroup.closure S : Set G).Finite

Used by 1

Used bySozutov's question on 3-transposition groups (Kourovka 12.76)

DefinitionSozutov's question on 3-transposition groups (Kourovka 12.76)#✓fully proved

The statement that for every group \(G\) and every set \(D\) of 3-transpositions of \(G\) that generates \(G\), the group \(G\) is locally finite.

def threeTranspositionGroupLocallyFinite : Prop :=
  ∀ (G : Type) [Group G] (D : Set G), IsThreeTranspositionSet D → Subgroup.closure D = ⊤ →
    IsLocallyFinite G

Uses 2 · Used by 1

Statement usesLocally finite group, via finite subsets · Set of 3-transpositions

Used byGroups generated by 3-transpositions are locally finite

TheoremGroups generated by 3-transpositions are locally finite#●ready to prove

If a group \(G\) is generated by a set \(D\) of 3-transpositions (a conjugation-invariant set of involutions whose pairwise products have order at most \(3\)), then \(G\) is locally finite: every finite subset of \(G\) generates a finite subgroup of \(G\).

The Kourovka Archive answers 12.76 "Yes, it is" (H. Cuypers and J. I. Hall, 1992).

public theorem_wanted threeTranspositionGroupLocallyFinite_holds :
    threeTranspositionGroupLocallyFinite

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.76 (A. I. Sozutov); resolution: H. Cuypers and J. I. Hall, in: Groups, combinatorics and geometry (Durham, 1990), London Math. Soc. Lecture Note Ser. 165, Cambridge Univ. Press, 1992, 121-138, Kourovka Archive, Problem 12.76: Yes, it is.

Uses 1

Statement usesSozutov's question on 3-transposition groups (Kourovka 12.76)

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.