Thompson's group F

DefinitionRelators of Thompson's group \(F\)#✓fully proved

In the free group on two generators \(x_0\) and \(x_1\), this is the set of the two elements \([x_0 x_1^{-1}, x_0^{-1} x_1 x_0]\) and \([x_0 x_1^{-1}, x_0^{-2} x_1 x_0^2]\), where \([a, b] = a b a^{-1} b^{-1}\). They are the relators of the standard presentation of Thompson's group \(F\).

def thompsonRelators : Set (FreeGroup (Fin 2)) :=
  let x₀ := FreeGroup.of (0 : Fin 2)
  let x₁ := FreeGroup.of (1 : Fin 2)
  let a := x₀ * x₁⁻¹
  let b := x₀⁻¹ * x₁ * x₀
  let c := x₀⁻¹ ^ 2 * x₁ * x₀ ^ 2
  {a * b * a⁻¹ * b⁻¹, a * c * a⁻¹ * c⁻¹}

Used by 2

Used byThompson's group \(F\) by its standard presentation · Howson property for Thompson's group \(F\)

AbbreviationThompson's group \(F\) by its standard presentation#✓fully proved

Thompson's group \(F\) is the group with generators \(x_0, x_1\) and relations \([x_0 x_1^{-1}, x_0^{-1} x_1 x_0] = 1\) and \([x_0 x_1^{-1}, x_0^{-2} x_1 x_0^2] = 1\), where \([a, b] = a b a^{-1} b^{-1}\); that is, the quotient of the free group on \(x_0, x_1\) by the normal subgroup generated by these two relators.

abbrev ThompsonF := PresentedGroup thompsonRelators

def thompsonRelators : Set (FreeGroup (Fin 2)) :=
  let x₀ := FreeGroup.of (0 : Fin 2)
  let x₁ := FreeGroup.of (1 : Fin 2)
  let a := x₀ * x₁⁻¹
  let b := x₀⁻¹ * x₁ * x₀
  let c := x₀⁻¹ ^ 2 * x₁ * x₀ ^ 2
  {a * b * a⁻¹ * b⁻¹, a * c * a⁻¹ * c⁻¹}

WantedExt/GroupTheory/ThompsonGroupHowsonKourovka19Problem40Wanted.lean:39

Uses 1 · Used by 1

Statement usesRelators of Thompson's group \(F\)

Used byHowson property for Thompson's group \(F\)

DefinitionHowson property for Thompson's group \(F\)#✓fully proved

The statement that Thompson's group \(F\) has the Howson property: for all finitely generated subgroups \(H\) and \(K\) of \(F\), the intersection \(H \cap K\) is finitely generated.

This is Kourovka Notebook Problem 19.40 (I. Kapovich).

def thompsonFHowson : Prop :=
  ∀ H K : Subgroup ThompsonF, H.FG → K.FG → (H ⊓ K).FG

Uses 2 · Used by 1

Statement usesThompson's group \(F\) by its standard presentation · Relators of Thompson's group \(F\)

Used byThompson's group \(F\) does not have the Howson property

TheoremThompson's group \(F\) does not have the Howson property#●ready to prove

It is not the case that the intersection of any two finitely generated subgroups of Thompson's group \(F\) is finitely generated: there are finitely generated subgroups \(H\) and \(K\) of \(F\) such that \(H \cap K\) is not finitely generated.

Resolved false: the Kourovka Archive answers 19.40 "No": \(\mathbb{Z} \wr \mathbb{Z}\) fails the Howson property (Kirkinskiĭ) and embeds in \(F\) (Cleary), and the property is inherited by subgroups.

public theorem_wanted thompsonFHowson_refuted : ¬ thompsonFHowson

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 19.40 (I. Kapovich); resolution: A. S. Kirkinskiĭ, Algebra Logic 20 (1981), no. 1, 24-36; S. Cleary, Pacific J. Math. 228 (2006), no. 1, 53-61; D. Robertson, letter of 24 April 2018, Kourovka Archive, Problem 19.40: No; ℤ ≀ ℤ does not have the Howson property (Kirkinskiĭ) and embeds in F (Cleary), and the Howson property passes to subgroups, https://arxiv.org/abs/1401.0300v49.

Uses 1

Statement usesHowson property for Thompson's group \(F\)

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.