Mission

Brin–Squier: the group of piecewise-linear homeomorphisms of the line with finitely many breakpoints has no free subgroup of rank greater than oneResearch Paper

Dynamical Systems Group Theory Topology·Captain: dbenbenn

Motivation

Von Neumann introduced amenability in 1929 in response to the Banach–Tarski paradox: a group is amenable when it carries a finitely additive, translation-invariant probability measure on its subsets, and no amenable group contains a free subgroup of rank $2$ — which is exactly what the paradox needs. The converse is the von Neumann conjecture, and it is false: Ol'shanskii in 1980 and Adyan in 1982 produced finitely generated counterexamples. A finitely presented counterexample was harder, and one candidate stood out — Richard Thompson's group $F$ , finitely presented, with nobody able to decide whether it was amenable.

Brin and Squier attacked it and in 1985 got what they called "half a success": they proved that $F$ , and more generally the group $\mathrm{PLF}(\mathbb{R})$ of piecewise-linear homeomorphisms of the line with finitely many breakpoints, contains no free subgroup of rank greater than $1$ . Whether $F$ is amenable they could not determine, and it is still open today; claimed proofs have appeared in both directions and none has been accepted. Finitely presented counterexamples were eventually found by other routes (Ol'shanskii–Sapir 2002; Lodha–Moore 2016), so $F$ is no longer needed as a candidate. This mission formalizes the half that was settled.

Setting

Let $\mathrm{Homeo}_+(\mathbb{R})$ be the group of orientation-preserving homeomorphisms of the line: the strictly increasing bijections $\mathbb{R}\to\mathbb{R}$ under composition. The support of $f$ is the set of points it moves, $\operatorname{supp} f = \{\,t : f(t)\neq t\,\}$ , an open subset of $\mathbb{R}$ .

A continuous $f$ is piecewise linear when there is a discrete set $B$ of breakpoints with $f$ differentiable off $B$ and $f'$ constant on each component of $\mathbb{R}\setminus B$ ; for finite $B$ this is the same as $f$ being affine on a neighbourhood of every point outside $B$ . Nothing is required at the points of $B$ , so the two affine pieces meeting at a breakpoint may disagree — that is what makes such an $f$ more than an affine map. Write $\mathrm{PL}(\mathbb{R})$ for the piecewise-linear elements of $\mathrm{Homeo}_+(\mathbb{R})$ and

\mathrm{PLF}(\mathbb{R}) = \{\, f \in \mathrm{PL}(\mathbb{R}) : f \text{ has a finite breakpoint set} \,\}

for the subgroup this mission is about. The distinction matters: the goal below holds in $\mathrm{PLF}(\mathbb{R})$ and fails in $\mathrm{PL}(\mathbb{R})$ , where Brin and Squier build free subgroups of rank $2$ by lifting them from the circle. Write $\mathrm{PLF}'(\mathbb{R})$ for the commutator subgroup, which Brin and Squier identify as the elements whose slope at each end is $1$ — an element has slope $a$ at an end when it agrees with a single affine map of slope $a$ on a ray out to that end. Thompson's group $F$ — the piecewise-linear homeomorphisms of $[0,1]$ with dyadic breakpoints and power-of-two slopes — is realized inside $\mathrm{PLF}(\mathbb{R})$ .

Formalization targets

Goal — no two elements generate freely

\text{for } f,g \in \mathrm{PLF}(\mathbb{R}), \quad F_2 \to \mathrm{PLF}(\mathbb{R}),\ a \mapsto f,\ b \mapsto g \quad\text{is never injective.}

Since a free group of rank greater than $1$ contains one of rank $2$ , this is Brin and Squier's Theorem (3.1).

The dichotomy it rests on

G \le \mathrm{PLF}'(\mathbb{R}) \implies G \text{ abelian, or } G \text{ contains a free abelian subgroup of rank } 2.

Their Theorem (3.2), with the conclusion weakened to what the goal consumes. What they prove is infinite rank, which needs the general form of their Lemma (1.2); that general Lemma and the full-strength (3.2) are milestones of their own here. The goal itself only ever uses the rank-two form.

The twenty-four milestones

Thirteen are numbered results of theirs: the support observations (1.1a), (1.1b); Lemma (1.2) in its rank-two case and in its general form; Lemmas (3.4) and (3.5), already formalized and published, entering as references; the commutator facts (2.14a), (2.14b), (2.14c); Theorem (3.2) both as the rank-two dichotomy the goal consumes and at full strength; and Corollary (3.3), likewise in both strengths. Five are piecewise-linear infrastructure the source treats as routine: closure of $\mathrm{PLF}(\mathbb{R})$ under composition and under inverse, the same two for slope $1$ at each end, and finiteness of the number of components of a support. Five more are steps the source asserts without proof — that the line carries no non-fixed periodic points, that a map fixing a set's complement preserves its components, that the iterated images of a pushed-forward interval are pairwise disjoint, that the closure of a commutator's moved set stays inside the union of the two supports (p. 495), and that the derived subgroup of a free group of rank two is non-abelian (p. 494). The last is not from the source at all — that an abelian subgroup of a free group is cyclic, which is what lets the goal finish through Nielsen–Schreier.

Significance

The theorem closes the standard route to proving a group non-amenable. To show a group amenable the classical routes are elementary amenability and subexponential growth, and $F$ is neither elementary amenable (Cannon–Floyd–Parry, Theorem 4.10) nor of subexponential growth, having exponential growth (their Corollary 4.7). To show a group non-amenable the standard route is to exhibit a free subgroup of rank $2$ — the route this theorem closes. $F$ sits in the gap, which is why its status has survived sustained attention.

The result reaches past $F$ . Monod's groups of piecewise projective homeomorphisms are counterexamples to von Neumann's conjecture, and Monod's theorem that they contain no non-abelian free subgroup is, in Monod's words, "a sequacious generalization of the corresponding theorem of Brin–Squier about piecewise affine transformations"; of its own proof that paper says it will "largely follow [Brin–Squier, § 3]".

What formalizing it adds. Mathlib has no piecewise-linear maps and no amenability predicate for groups. This mission builds the piecewise-linear layer: a workable $\mathrm{PLF}(\mathbb{R})$ , its closure properties, and the structure of supports.

Difficulty

The obstruction is bookkeeping across two finiteness facts of different kinds. Finiteness of the breakpoint set is what gives an element slopes at $\pm\infty$ at all, and what makes two elements affine on each side of a common fixed point. Compactness is the other — throughout, $[f,g] = fgf^{-1}g^{-1}$ — and it splits: that the closure of $\operatorname{supp}[f,g]$ is compact needs only slope $1$ at each end, with no piecewise linearity at all, which is why (2.14b) is formalized under a weaker hypothesis than the source's; that the closure stays inside $\operatorname{supp} f \cup \operatorname{supp} g$ is what reaches back to finiteness. Keeping straight which fact does which job is most of the work.

The first idea a newcomer has about (3.2) is the wrong one. Its proof produces a family of commuting elements, and it is not disjointness of supports that makes them commute: only their intersections with one chosen component are disjoint, and commutation is deduced instead from a minimality argument. A proof routed through disjoint supports will not close.

Formalization scope

What the Lean fixes. Elements are order isomorphisms of $\mathbb{R}$ — strictly increasing bijections, automatically homeomorphisms — rather than a homeomorphism type. Composition follows Mathlib's convention $(f\cdot g)(x) = f(g(x))$ , the opposite of the source's right action, so the conjugation identity reads $\operatorname{supp}(fgf^{-1}) = f(\operatorname{supp} g)$ here; getting this backwards states a different theorem that still compiles. A support is the bare moved set, with no closure taken. Piecewise linearity is a finite breakpoint set together with local affineness off it — the set need not be minimal and may be empty. A copy of $\mathbb{Z}^2$ is an injectivity statement about $(m,n)\mapsto u^m v^n$ , not a subgroup isomorphism, and the goal is about a single pair $f,g$ rather than a subgroup. The dichotomy hypothesises slope $1$ at both ends directly, not membership in a derived subgroup — that these coincide is the source's result, and both inclusions are formalized here: (2.14a) gives one, and the identification asserted on p. 493 gives the other. Beyond a workable $\mathrm{PLF}(\mathbb{R})$ , the development needs Nielsen–Schreier, already in Mathlib as subgroupIsFreeOfIsFree: it is what lets an abelian subgroup of a free group be cyclic, and so lets the goal finish without the source's metabelian ending. That ending is formalized too, as Corollary (3.3) together with the p. 494 remark that the derived subgroup of a free group of rank two is non-abelian; the goal simply does not route through it.

One trivializing reading is ruled out. Slope $1$ at both ends is not a compact-support condition — every translation satisfies it — so (3.2) is not secretly a statement about compactly supported maps.

Nothing is built for $F$ specifically, and amenability is not touched. That is the one piece deliberately omitted, and contributions are welcome on it: modelling $F$ and embedding it in $\mathrm{PLF}(\mathbb{R})$ . The piecewise-linear layer is reusable beyond this theorem — Thompson's groups $T$ and $V$ , and piecewise-linear topology generally, need exactly it.

Selected references

M. G. Brin and C. C. Squier, Groups of piecewise linear homeomorphisms of the real line, Invent. math. 79 (1985), 485–498, doi:10.1007/BF01388519. Theorem (3.1) is the goal.
J. W. Cannon, W. J. Floyd and W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Mathématique 42 (1996), 215–256. Theorem 4.10 and Corollary 4.7.
N. Monod, Groups of piecewise projective homeomorphisms, Proc. Natl. Acad. Sci. USA 110 (2013), 4524–4527, arXiv:1209.5229.
A. Yu. Ol'shanskii and M. V. Sapir, Non-amenable finitely presented torsion-by-cyclic groups, Publ. Math. IHÉS 96 (2002), 43–169, doi:10.1007/s10240-002-0006-7.
Y. Lodha and J. T. Moore, A nonamenable finitely presented group of piecewise projective homeomorphisms, Groups Geom. Dyn. 10 (2016), 177–200, doi:10.4171/ggd/347.
V. Guba, Amenability problem for Thompson's group $F$ : state of the art, J. Groups Complex. Cryptol. 15 (2023), arXiv:2305.07113.

Goal · No two piecewise-linear homeomorphisms with finitely many breakpoints form a free basis (Theorem 3.1: PLF(ℝ) has no free subgroup of rank greater than one)

PROVED

namespace BrinSquier

theorem no_free_subgroup_of_rank_two (f g : ℝ ≃o ℝ) (hf : IsPLF f) (hg : IsPLF g) :
    ¬ Function.Injective (FreeGroup.lift ![f, g]) := by
  sorry

end BrinSquier

For any two piecewise-linear homeomorphisms $f,g$ of $\mathbb{R}$ with finitely many breakpoints, the homomorphism from the free group of rank two sending its generators to $f$ and $g$ is never injective.

F_2 \longrightarrow \mathrm{PLF}(\mathbb{R}), \qquad a \mapsto f, \quad b \mapsto g\qquad\text{is never injective.}

Equivalently — and this is how Brin and Squier open their Section 3 — any two elements of $\mathrm{PLF}(\mathbb{R})$ satisfy a nontrivial relation: some nonempty reduced word in $f$ , $g$ and their inverses is the identity.

Since a free group of rank greater than one contains one of rank two, and since $\mathrm{PLF}(\mathbb{R})$ is closed under products and inverses, this is exactly their Theorem (3.1): $\mathrm{PLF}(\mathbb{R})$ contains no free subgroup of rank greater than $1$ .

Why it matters. Thompson's group $F$ sits inside $\mathrm{PLF}(\mathbb{R})$ , so $F$ too has no non-abelian free subgroup. Brin and Squier set out to decide whether $F$ is a finitely presented counterexample to von Neumann's conjecture, and called this result half a success: it settles that $F$ cannot be shown non-amenable by exhibiting a free subgroup. Whether $F$ is amenable remains open.

Frontier · Open leaf nodes

Recent activity

Mission

Brin–Squier: the group of piecewise-linear homeomorphisms of the line with finitely many breakpoints has no free subgroup of rank greater than one

Goal