This mission formalizes §6 of J. W. Cannon, W. J. Floyd and W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Mathématique (2) 42 (1996) 215–256, doi:10.5169/seals-87877: the definition of Thompson's group $V$ and Thompson's proof that $V$ is simple.

Motivation

Thompson's groups $T$ and $V$, introduced in unpublished notes of Richard Thompson in 1965, were the first known examples of infinite, finitely presented, simple groups. The notes of Cannon, Floyd and Parry were written in part "to make available Thompson's unpublished proofs … of the simplicity of $T$ and $V$" (p. 216); §6 is the proof for $V$.

$V$ contains $T$, which contains $F$. Earlier missions on this platform formalize $F$ and its commutator subgroup (§1 and §4), its tree-diagram normal form (§2), its presentations (§3), and the simplicity of $T$ (§5). Unlike $T$, the elements of $V$ need not be continuous: they cut the circle into pieces and rearrange them in any order, so $V$ contains every finite symmetric group.

Setting

The circle $S^1$ is $[0,1]$ with its endpoints identified, in Lean UnitAddCircle ($\mathbb{R}/\mathbb{Z}$); $[x]$ denotes the image of $x \in \mathbb{R}$. Maps compose right to left, $(fg)(t) = f(g(t))$, and $[x, y] = xyx^{-1}y^{-1}$.

The group $V$ (p. 240) consists of the right-continuous bijections of $S^1$ that map images of dyadic rationals to images of dyadic rationals, are differentiable except at finitely many images of dyadic rationals, and are linear with slope a power of $2$ on each maximal interval of differentiability. In Lean a permutation $f$ of the circle satisfies IsThompsonV f when it maps dyadic points to dyadic points and, for a finite set of dyadic breakpoints, is $[z] \mapsto [2^n z + c]$ on each half-open piece between consecutive breakpoints modulo $1$. V is the subgroup generated by these maps; that they already form a group is the first milestone.

The elements. $A$, $B$, $C$ are $T$'s generators, and $\pi_0$ (mapPi0) exchanges $[0, \tfrac12)$ and $[\tfrac12, \tfrac34)$ by $x \mapsto x/2 + \tfrac12$ and $x \mapsto 2x - 1$. The words $X_0 = A$, $X_n = A^{-(n-1)}BA^{n-1}$, $C_n = A^{-(n-1)}CB^{n-1}$, $\pi_1 = C_2^{-1}\pi_0C_2$ and $\pi_n = A^{-(n-1)}\pi_1A^{n-1}$ (p. 241) are defined once, as words in four symbols, and read both as maps of the circle and in $V_1$.

The presented group $V_1$ (p. 242) is the free group on $A$, $B$, $C$, $\pi_0$ modulo fourteen relators: the six relators of $T_1$ (§5), and eight more involving the $\pi_n$, such as $\pi_1^2$, $(\pi_2\pi_1)^3$ and $(\pi_1C_2)^3$. In $V_1$, $\Pi(n)$ is the subgroup generated by $\pi_0, \dots, \pi_{n-1}$, $\Pi = \bigcup_n \Pi(n)$, and an element is positive when it is a product of nonnegative powers of the $X_i$.

Target

The goal is the sentence in which the notes state what §6 does, "In §6 we define $V$ and give Thompson's proof that $V$ is simple" (p. 216):

$$V \text{ is simple.}$$

The route is the section's own. Lemma 6.1 shows that $A$, $B$, $C$, $\pi_0$ generate $V$ and satisfy the fourteen relations, so $V_1$ maps onto $V$. Lemmas 6.2–6.8 establish how the $\pi_i$ move past the $X_j$ and $C_n$, leading to Theorem 6.9, $V_1$ is simple, and hence $V_1 \cong V$. The goal follows.

Significance

The result. $V$ is the third of Thompson's groups and the one whose elements rearrange pieces of the circle: it is infinite, finitely presented and simple, and it contains every finite group (through the finite symmetric groups). Together with $T$ it gave the first examples of infinite finitely presented simple groups.

Formalizing it. No machine-checked proof that $V$ is simple exists on this platform, and Mathlib has nothing on Thompson's groups. This mission reuses the formalization of $F$ and $T$: $V_1$'s first six relators are $T_1$'s, and the proof of Theorem 6.9 applies Theorem 5.7 and Theorem 5.8 inside $V_1$.

Difficulty

The central difficulty is the generation half of Lemma 6.1. The notes' proof uses tree diagrams with labelled leaves: every element of $V$ permutes the intervals of one standard dyadic partition onto those of another, $F$ moves any partition to a standard comb, and the subgroup generated by $\pi_0$ and $C_{n-2}$ acts as the full symmetric group on the comb's intervals. Each step is stated in one sentence; the milestones make each a separate statement.

The algebra of $V_1$ (Lemmas 6.2–6.6) is a chain of inductions. The proofs lean on two facts the notes use without isolating them: that $T_1$ maps to $V_1$ (so §5's lemmas hold in $V_1$), and the normal form $g = p\pi C_n^m q^{-1}$ in $V_1$, stated inside the proof of Theorem 6.9. Both are milestones here. The notes also cite two facts about the finitary symmetric group $\Sigma$ without proof, its presentation and the behaviour of its proper quotients, and deduce $\Pi \cong \Sigma$; the proof of Theorem 6.9 uses all three, and each is a milestone.

What is left out

• Figures 16–19, tree-diagram computations for relations 11) and 12); the relations are stated directly in Lemma 6.1.

Formalization scope

• $V$ is a Subgroup (Equiv.Perm UnitAddCircle) generated by IsThompsonV. Half-open pieces make every element right-continuous; "linear" is read modulo $1$, so a piece may wrap past $[0]$, as a rotation does. Unlike $T$, no lift to the line is available, since elements of $V$ need not be monotone.
• $V_1$ is Mathlib's PresentedGroup on the four-element type FormalV. Relators are written out as $xyx^{-1}y^{-1}$.
• $\Sigma$ is SigmaPerm, the subgroup of Equiv.Perm ℕ of permutations moving finitely many points, and $s_i$ is the transposition of $i$ and $i + 1$; its presentation is a PresentedGroup on ℕ. $\Pi$ is taken as the subgroup of $V_1$ generated by all the $\pi_i$, which is the union of the $\Pi(n)$.
• Lemma 6.1's surjection and the isomorphism $V_1 \cong V$ pin the images of the four symbols, so no isomorphism ignoring the generators satisfies them.
• Reused platform theorems, which solutions may import: Theorem 3.4, Corollary 2.6, Lemma 4.2, Theorem 4.11, and from §5 Lemma 5.2, Lemmas 5.5 and 5.6, Theorem 5.7 and Theorem 5.8. The standard dyadic partitions of the tree-diagram milestone are the §2 bundle's IsStandardDyadicPartition.

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, §6 pp. 240–248. doi:10.5169/seals-87877