This mission formalizes §5 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 $T$ and Thompson's proof that $T$ 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. Every finitely presented simple group known before them was finite. 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), and §5 is that proof for $T$.

$T$ is the circle's counterpart of Thompson's group $F$. Earlier missions on this platform formalize $F$ and its commutator subgroup (§1 and §4 of the same notes), its tree-diagram normal form (§2), and its two presentations (§3). $F$ is not simple: its abelianization is $\mathbb{Z}^2$. $T$ is simple, it has elements of finite order (the generator $C$ below has order $3$), and it contains $F$ as the stabilizer of a point.

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] = x y x^{-1} y^{-1}$, the convention of the notes.

The group $T$ (pp. 233–234) consists of the piecewise linear homeomorphisms 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 have slopes that are powers of $2$. In Lean a permutation $f$ of the circle satisfies IsThompsonCircle f when it has a lift to the line: an order isomorphism $L$ of $\mathbb{R}$ with $L(x+1) = L(x) + 1$ and $f[x] = [L(x)]$, mapping dyadic rationals to dyadic rationals, and affine with slope a power of $2$ between consecutive integer translates of finitely many dyadic breakpoints. T is the subgroup generated by these maps. That they already form a group is the first milestone.

The elements $A$, $B$, $C$ (Example 5.1). $A$ and $B$ are the generators of $F$ from the §1 mission (mapA, mapB), carried to the circle by toCircle, which sends an order isomorphism $g$ of $[0,1]$ to $[x] \mapsto [g(x)]$. $C$ (mapC) is given on $[0,1]$ by $x/2 + 3/4$, $2x - 1$ and $x - 1/4$ on $[0, \tfrac12]$, $[\tfrac12, \tfrac34]$ and $[\tfrac34, 1]$. symT sends the formal symbols $A$, $B$, $C$ to these three maps.

The presented group $T_1$ (p. 236) is the free group on formal symbols $A$, $B$, $C$ modulo six relators:

$$[AB^{-1}, A^{-1}BA],\quad [AB^{-1}, A^{-2}BA^2],\quad C^{-1}B(A^{-1}CB),$$ $$((A^{-1}CB)(A^{-1}BA))^{-1}B(A^{-2}CB^2),\quad (CA)^{-1}(A^{-1}CB)^2,\quad C^3.$$

In $T_1$, $X_0 = A$ and $X_n = A^{-(n-1)}BA^{n-1}$ (XT1); $C_0 = 1$ and $C_n = A^{-(n-1)}CB^{n-1}$ (CT1) for $n \ge 1$. An element is positive (IsPositiveT1) when it is a product of nonnegative powers of the $X_i$.

Target

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

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

The route is the section's own. Lemma 5.2 shows that $A$, $B$, $C$ generate $T$ and satisfy the six relations, so $T_1$ maps onto $T$ (Lemma 5.3). Lemmas 5.4–5.6 and a normal form (Theorem 5.7, every $g \in T_1$ is $p\,C_n^m q^{-1}$ with $p$, $q$ positive and $m < n + 2$) lead to Theorem 5.8, $T_1$ is simple, and hence to Corollary 5.9, $T_1 \cong T$. The goal follows.

Significance

The result. The simplicity of $T$ is one of the two facts that made Thompson's groups famous: $T$ is an infinite, finitely presented, simple group. Corollary 5.9 gives more, an explicit presentation of $T$ on three generators and six relators.

Formalizing it. No machine-checked proof that $T$ is simple exists on this platform, and Mathlib has nothing on Thompson's groups. The proof in the notes is short and complete. This mission connects the analytic definition of $T$ with the combinatorial group $T_1$, reusing the platform's formalization of $F$: the presentation of $F$ (Theorem 3.4), its normal form (Corollary 2.7), and the fact that its proper quotients are Abelian (Theorem 4.3).

Difficulty

The algebra of $T_1$ (Lemmas 5.5 and 5.6) is a chain of explicit inductions. The substance lies at two points.

The first is Theorem 5.7. The notes' proof that the set of elements $p\,C_n^m q^{-1}$ is closed under multiplication moves $q_1^{-1}p_2$ past $C_j^i$ and $C_l^k$ using the normal form of $F$, transported into $T_1$ through Lemma 5.4, and then re-indexes, all inside the abstract group $T_1$ with no geometry to lean on.

The second is the analytic side of Lemma 5.2. Generation reduces an arbitrary $f \in T$ to an element of $F$ by composing with $C$ and with an element of $F$ that moves $f([0])$ to $[\tfrac34]$. That needs the fact that an element of $T$ fixing $[0]$ comes from $F$, which the notes state in one line. The relations are identities between explicit piecewise linear maps of the circle.

What is left out

• The remark that $T$ is conjugate to a group of $C^\infty$ diffeomorphisms (Ghys–Sergiescu, p. 234). It is not used.
• Tree diagrams for $T$ and Figures 11–15. The notes use them only to verify relations 3)–6), and those relations are stated directly in Lemma 5.2.
• The observation on p. 237 that $C_n$ permutes $n + 2$ intervals cyclically, given "to gain some insight" and not used afterwards.

Formalization scope

• $T$ is a Subgroup (Equiv.Perm UnitAddCircle) generated by IsThompsonCircle. The lift makes every element an orientation-preserving homeomorphism, so continuity is not stated separately. Unlike for $F$, the condition that dyadics map to dyadics cannot be dropped: an irrational rotation satisfies every other clause.
• $T_1$ is Mathlib's PresentedGroup on the three-element type FormalABC. Relators are written out as $xyx^{-1}y^{-1}$, not with commutator notation.
• Lemma 5.3 and Corollary 5.9 pin the images of the three symbols, so no isomorphism that ignores the generators can satisfy them. Lemma 5.4 pins the images of $A$ and $B$.
• Reused platform theorems, which solutions may import: Theorem 3.4 ($F_1 \cong F$), Corollary 2.6 ($A$, $B$ generate $F$), Lemma 4.2, Corollary 2.7, Lemma 2.8, Theorem 4.3, line (3.2), and Theorem 4.11 ($F$ is totally ordered, hence torsion-free).
• Welcome beyond the milestones: §6's group $V$, whose presentation extends $T_1$.

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, §5 pp. 233–240. doi:10.5169/seals-87877
• É. Ghys, V. Sergiescu, Sur un groupe remarquable de difféomorphismes du cercle, Comment. Math. Helv. 62 (1987) 185–239. doi:10.1007/BF02564445