Motivation

This mission formalizes §4 of Cannon, Floyd and Parry's Introductory notes on Richard Thompson's groups, together with the definition of Thompson's group $F$ from their §1. The goal is their Theorem 4.5: the commutator subgroup $[F,F]$ is simple.

In the 1960s Richard Thompson defined three groups, now written $F$, $T$ and $V$, whose properties have kept them in use ever since as a source of examples at the edge of what groups can do. $F$ is the smallest of the three and the least understood. It is finitely presented (§3 of the source) and torsion-free, it has no free subgroup of rank two, and whether it is amenable — whether it carries a finitely additive left-invariant probability measure defined on all its subsets — is open. Cannon, Floyd and Parry record (§4, p. 227) that Geoghegan raised the question and conjectured in 1979 both that $F$ contains no non-Abelian free subgroup and that $F$ is not amenable.

That question is what makes $F$ worth pinning down precisely. Write $AG$ for the class of amenable discrete groups, $EG$ for the elementary amenable ones, and $NF$ for the groups with no free subgroup of rank two. That $AG \subset NF$ was noted by Day and follows from von Neumann; whether it is strict is the von Neumann–Day problem. It is: Olshanskii proved $AG \neq NF$ in a 1984 ICM address and Gromov gave an independent proof — but by examples that are not finitely presented. Brin and Squier proved in 1985 that $F \in NF$, and $F$ is not elementary amenable (Theorem 4.10 of the source, CannonFloydParry.not_elementaryAmenable_F). So $F$ is a finitely presented group in $AG \setminus EG$ if it is amenable and in $NF \setminus AG$ if it is not — a question with no other finitely presented candidate.

Setting

Call a real number dyadic if it has the form $m/2^{k}$ with $m \in \mathbb{Z}$ and $k \in \mathbb{N}$.

Thompson's group $F$, as §1 of the source defines it, is the set of piecewise linear homeomorphisms of the closed unit interval $[0,1]$ onto itself that are differentiable except at finitely many dyadic rationals, and whose derivatives, where they exist, are powers of $2$. Since those derivatives are positive, every element preserves orientation, so the elements of $F$ are increasing. Composition of two such maps is again one, and so is the inverse of one, so $F$ is a group.

The formalization calls such a map piecewise linear over the dyadics, and defines $F$ as the subgroup generated by those maps — so that closure under composition and inverses is a theorem rather than part of the construction, as the source has it. What the model fixes rather than derives is under Formalization scope below.

Two particular elements generate it. Write

$$A(x) = \begin{cases} x/2 & 0 \le x \le \tfrac12\\ x - \tfrac14 & \tfrac12 \le x \le \tfrac34\\ 2x-1 & \tfrac34 \le x \le 1\end{cases} \qquad B(x) = \begin{cases} x & 0 \le x \le \tfrac12 \\ x/2 + \tfrac14 & \tfrac12 \le x \le \tfrac34 \\ x - \tfrac18 & \tfrac34 \le x \le \tfrac78 \\ 2x-1 & \tfrac78 \le x \le 1.\end{cases}$$

An element of $F$ is trivial near $0$ if it fixes every point of some interval $[0,\varepsilon)$, and trivial near $1$ if it fixes every point of some $(1-\varepsilon, 1]$. The support of $f$ is the set of points of $[0,1]$ that $f$ moves. The commutator convention throughout is $[x,y] = xyx^{-1}y^{-1}$, and $[F,F]$ denotes the commutator subgroup.

Formalization targets

Goal

$$[F,F] \ \text{is a simple group.}$$

This is the capstone of §4: it says the commutator subgroup has no normal subgroup other than itself and the trivial one. It is the goal because the rest of the section feeds it — both halves of Theorem 4.1, Theorem 4.3, and both supporting lemmas below are consumed by its proof.

Theorem 4.1, which has two parts

$$[F,F] \;=\; \{\, f \in F : f \text{ is trivial near } 0 \text{ and near } 1 \,\}$$ $$F/[F,F] \;\cong\; \mathbb{Z} \oplus \mathbb{Z}$$

Theorem 4.3

$$N \trianglelefteq F,\ N \neq 1 \;\Longrightarrow\; F/N \text{ is Abelian}$$

So $F$ has no interesting proper quotients at all. With the first part of Theorem 4.1 this forces every nontrivial normal subgroup of $F$ to contain $[F,F]$.

Supporting results

That the piecewise-linear maps are already closed under composition and inverses, so that $F$ consists of exactly those maps; a transitivity lemma on dyadic partitions of $[0,1]$; the fact that the subgroup of elements supported in a dyadic interval $[a,b]$ of dyadic length is isomorphic to $F$ itself; triviality of the center; that $F$ contains no non-Abelian free group; and that $F$ admits a total order invariant under multiplication on both sides.

Significance

What the results give. Theorem 4.1 identifies $[F,F]$ concretely — a subgroup defined by a global algebraic condition turns out to be cut out by local behavior at the two endpoints — and computes the abelianization, making the pair of endpoint slopes a complete invariant of $F$ modulo commutators. Theorem 4.3 and the simplicity of $[F,F]$ together determine the whole normal subgroup lattice: every normal subgroup of $F$ is trivial or contains $[F,F]$. That lattice is the input to the elementary-amenability argument.

What formalizing adds. All of these are proved in the source; none is in Mathlib, which has no piecewise-linear homeomorphism API and no Thompson group. Four of the milestones are proved as part of this proposal: that the piecewise-linear maps form a subgroup, that elements of $F$ permute the dyadic rationals, that $F$ embeds in the group Brin and Squier work with, and the absence of a free subgroup of rank two, which follows from the already-formalized Brin–Squier theorem via that embedding. The rest are open. The piecewise-linear machinery built along the way — local affineness, dyadic-breakpoint bookkeeping, extension by the identity — is reusable for $T$, for $V$, and for the wider family of piecewise-linear homeomorphism groups.

Difficulty

The obvious approach to the goal is to argue that a normal subgroup of $[F,F]$ containing a nontrivial element must be everything, by conjugating that element around. It fails on its own: an element of $[F,F]$ is pinned down only by being trivial near the two endpoints, and one still has to manufacture — inside $[F,F]$, not merely inside $F$ — an element carrying a prescribed pair of neighborhoods into those. That construction is what the dyadic-partition transitivity lemma supplies, and it is where the combinatorics of dyadic subdivision enters.

The second difficulty was that the source proves §4 using the tree-diagram normal form of §2. That section is now formalized in its own mission, Cannon–Floyd–Parry §2: tree diagrams and the normal form (mission ffd1e4ea-9f9a-4cb6-8419-78e70f2545e8), all of whose milestones are proved. Corollary 2.6 — milestone 5 here, the same theorem object — is closed from there, and Theorem 2.5 (represents_word_exponents) and the normal form (existsUnique_normalForm) are available to a solver attacking Theorem 4.3, so the source's argument can now be followed. A solution file imports only definitions, so whatever it uses from §2 must be reproved inline; the §2 solutions are public and written to be reused that way. The piecewise-linear route — dyadic-partition transitivity, Lemma 4.4 and Theorem 4.1 — remains an alternative, and is what Theorem 4.5's own argument uses.

Formalization scope

The unit interval is $[0,1] \subseteq \mathbb{R}$ as a subtype, and an element of $F$ is an order isomorphism of it, so orientation preservation is built into the representation rather than derived — faithful to the source's set, but assuming one sentence CFP prove. Piecewise linearity is stated as: there is a finite set $B$ of dyadic reals such that the map is affine, with slope a power of two, on every closed interval whose interior misses $B$. Intercepts are not required to be dyadic — that is derived by induction along the breakpoints, not part of the definition.

The definition is not vacuous: $A$ and $B$ of Example 1.1 are constructed explicitly, and that $F$ is not the trivial group is one of the milestones below — so no statement here is satisfied by the trivial group. In particular the goal, which asserts simplicity and therefore nontriviality, is not trivially false.

A companion definition places the same data on the real line, each element extended by the identity outside $[0,1]$; that line realisation is what the bridge statement connects to Brin and Squier's group.

Selected references

• J. W. Cannon, W. J. Floyd, W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Mathématique (2) 42 (1996), 215–256. doi:10.5169/seals-87877
• M. G. Brin, C. C. Squier, Groups of piecewise linear homeomorphisms of the real line, Inventiones Mathematicae 79 (1985), 485–498. doi:10.1007/BF01388519
• C. Chou, Elementary amenable groups, Illinois Journal of Mathematics 24 (1980), 396–407. doi:10.1215/ijm/1256047608
• M. M. Day, Amenable semigroups, Illinois Journal of Mathematics 1 (1957), 509–544. doi:10.1215/ijm/1255380675
• J. von Neumann, Zur allgemeinen Theorie des Maßes, Fundamenta Mathematicae 13 (1929), 73–116. doi:10.4064/fm-13-1-73-116
• A. Yu. Olshanskii, On a geometric method in the combinatorial group theory, Proceedings of the International Congress of Mathematicians (Warsaw, 1983), vol. 1, 1984, pp. 415–424. IMU archive
• M. Gromov, Hyperbolic groups, in Essays in Group Theory (S. M. Gersten, ed.), MSRI Publications 8, Springer, 1987, pp. 75–263. doi:10.1007/978-1-4613-9586-7_3