A map given by a pair of standard dyadic partitions is a word in $A$ and $B$

Open

CannonFloydParry.mem_closure_mapA_mapB_of_standardDyadicPartition

by shivm · Sep 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsgroup-theorypiecewise-linearthompsons-group

This is the generation half of the source's Corollary 2.6, stated for a single element in terms of its tree diagram.

Suppose $f$ is an order isomorphism of $[0,1]$ realised by a pair of standard dyadic partitions with equally many intervals, that is, there are

0 = x_0 < x_1 < \cdots < x_n = 1, \qquad 0 = y_0 < y_1 < \cdots < y_n = 1,

each $[x_{i}, x_{i+1}]$ and each $[y_{i}, y_{i+1}]$ a standard dyadic interval $[a/2^{k}, (a+1)/2^{k}]$ , such that $f$ maps $[x_{i}, x_{i+1}]$ affinely onto $[y_{i}, y_{i+1}]$ :

f(z) = \frac{y_{i+1} - y_{i}}{x_{i+1} - x_{i}}\,\bigl(z - x_{i}\bigr) + y_{i} \qquad (x_{i} \le z \le x_{i+1}).

Then $f$ lies in the subgroup generated by the two maps $A$ and $B$ of Example 1.1.

The argument in the source is by induction on the number of intervals, using the fact that the subgroup $\langle A, B \rangle$ acts transitively on standard dyadic partitions with a fixed number of intervals. Writing $R_n$ for the "all-right" partition $\{0, \tfrac12, \tfrac34, \ldots, 1 - 2^{-(n-1)}, 1\}$ , one produces $g, h \in \langle A, B \rangle$ carrying $R_n$ to the $x$ -partition and to the $y$ -partition respectively, each affinely on every interval; then $f = h g^{-1}$ . The elements needed are the maps $x_m = A^{-(m-1)} B A^{m-1}$ , each of which is visibly a word in $A$ and $B$ and which halves a single interval of the right vine.

Combined with the normal-form lemma — every element of $F$ is realised by such a pair of standard dyadic partitions — this yields $F = \langle A, B \rangle$ .

Preamble

import Definitions.Def_CannonFloydParry
import Mathlib

Formal statement

namespace CannonFloydParry

theorem mem_closure_mapA_mapB_of_standardDyadicPartition {n : ℕ} {f : UI ≃o UI}
    (x y : Fin (n + 1) → UI)
    (hx : StrictMono x) (hy : StrictMono y)
    (hx0 : (x 0 : ℝ) = 0) (hxn : (x (Fin.last n) : ℝ) = 1)
    (hy0 : (y 0 : ℝ) = 0) (hyn : (y (Fin.last n) : ℝ) = 1)
    (hxs : ∀ i : Fin n, ∃ a k : ℕ,
      (x i.castSucc : ℝ) = a / 2 ^ k ∧ (x i.succ : ℝ) = (a + 1) / 2 ^ k)
    (hys : ∀ i : Fin n, ∃ a k : ℕ,
      (y i.castSucc : ℝ) = a / 2 ^ k ∧ (y i.succ : ℝ) = (a + 1) / 2 ^ k)
    (hf : ∀ (i : Fin n) (z : UI), (x i.castSucc : ℝ) ≤ (z : ℝ) → (z : ℝ) ≤ (x i.succ : ℝ) →
      (f z : ℝ) =
        ((y i.succ : ℝ) - (y i.castSucc : ℝ)) / ((x i.succ : ℝ) - (x i.castSucc : ℝ))
          * ((z : ℝ) - (x i.castSucc : ℝ)) + (y i.castSucc : ℝ)) :
    f ∈ Subgroup.closure {mapA, mapB} := by
  sorry

end CannonFloydParry

Source

Cannon, J. W., Floyd, W. J., Parry, W. R., Introductory notes on Richard Thompson's groups, L'Enseignement Mathematique (2) 42 (1996) 215-256, https://doi.org/10.5169/seals-87877, Section 2 (tree diagrams), Lemma 2.2 and Theorem 2.5, pp. 220-224 (supporting steps for Corollary 2.6, that

A

and

B

generate

F

)

View graph

A map given by a pair of standard dyadic partitions is a word in AAA and BBB

A map given by a pair of standard dyadic partitions is a word in $A$ and $B$