Maps supported strictly inside a dyadic interval are products of commutators supported in it

Open

CannonFloydParry.mem_closure_commutator_supp_Icc

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

dynamical-systemsgroup-theorypiecewise-linearthompsons-group

Fix dyadic rationals $a, b$ with $0 < a < b < 1$ , and reals $c, d$ with $a < c < d < b$ . Write

F_{[a,b]} = \{\, g \in F : \operatorname{supp} g \subseteq [a,b] \,\}

for the subgroup of elements of $F$ supported in $[a,b]$ ; restriction to $[a,b]$ identifies it with a copy of $F$ acting on the dyadic interval $[a,b]$ .

The assertion is that every $u \in F$ whose support is contained in $[c,d]$ lies in the commutator subgroup of $F_{[a,b]}$ : $u$ is a product of commutators $g h g^{-1} h^{-1}$ with $g, h \in F$ supported in $[a,b]$ . Formally, $u$ belongs to the subgroup generated by

\{\, g h g^{-1} h^{-1} \;:\; g,h \in F,\ \operatorname{supp} g \subseteq [a,b],\ \operatorname{supp} h \subseteq [a,b] \,\}.

This is Theorem 4.1 transported to the copy of $F$ living on $[a,b]$ . Since $\operatorname{supp} u \subseteq [c,d]$ with $a < c$ and $d < b$ , the map $u$ is the identity on $[a,c]$ and on $[d,b]$ , hence trivial in neighbourhoods of the two endpoints of $[a,b]$ — exactly the condition that Theorem 4.1 characterises as membership in the commutator subgroup. The strict inequalities $a < c$ and $d < b$ are essential: an element merely supported in the open interval $(a,b)$ need not be trivial near $a$ , since it may fix $a$ while having a nontrivial slope immediately to its right.

Preamble

import Definitions.Def_CannonFloydParry
import Mathlib

Formal statement

namespace CannonFloydParry

theorem mem_closure_commutator_supp_Icc {a b c d : ℝ}
    (ha : 0 < a) (hac : a < c) (hcd : c < d) (hdb : d < b) (hb : b < 1)
    (hda : IsDyadic a) (hdb' : IsDyadic b)
    {u : UI ≃o UI} (hu : u ∈ F) (hsupp : supp u ⊆ Set.Icc c d) :
    u ∈ Subgroup.closure {x : UI ≃o UI | ∃ g h : UI ≃o UI,
      g ∈ F ∧ h ∈ F ∧ supp g ⊆ Set.Icc a b ∧ supp h ⊆ Set.Icc a b ∧ x = g * h * g⁻¹ * h⁻¹} := 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, Theorem 4.5, p. 230 (supporting step in the proof that the commutator subgroup of

F

is simple)

View graph