Every nontrivial normal subgroup of $F$ contains a copy of $F$

Proved

CannonFloydParry.exists_subgroup_le_mulEquiv_of_normal_ne_bot

by dbenbenn · Sep 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

group-theorypiecewise-linearthompsons-group

Let $N$ be a normal subgroup of Thompson's group $F$ with $N \ne \{1\}$ . Then there is a subgroup $H \le F$ with $H \subseteq N$ and $H$ isomorphic to $F$ as a group.

This is the sentence in the source's proof of Theorem 4.10, "Theorem 4.1 and Lemma 4.4 easily imply that $N$ contains a subgroup isomorphic with $F$ ", stated on its own. The isomorphism is only asserted to exist; no particular one is named.

Preamble

import Definitions.Def_CannonFloydParry
import Mathlib

Formal statement

namespace CannonFloydParry

/-- Theorem 4.10, the step the source states in words: every nontrivial normal subgroup of `F`
contains a subgroup isomorphic to `F`. -/
theorem exists_subgroup_le_mulEquiv_of_normal_ne_bot (N : Subgroup F) [N.Normal] (hN : N ≠ ⊥) :
    ∃ H : Subgroup F, H ≤ N ∧ Nonempty (H ≃* F) := by
  sorry

end CannonFloydParry

Source

Cannon, J. W., Floyd, W. J., Parry, W. R., Introductory notes on Richard Thompson's groups, L'Enseignement Mathématique (2) 42 (1996) 215–256, https://doi.org/10.5169/seals-87877, Theorem 4.10 (proof), p. 233.

View graph

Every nontrivial normal subgroup of FFF contains a copy of FFF

Every nontrivial normal subgroup of $F$ contains a copy of $F$