This mission formalizes N. Monod, Groups of piecewise projective homeomorphisms, Proceedings of the National Academy of Sciences 110 (2013) 4524–4527, doi:10.1073/pnas.1218426110: the groups $H(A)$ of piecewise projective homeomorphisms of the line are non-amenable and have no free subgroups whenever $A \neq \mathbf{Z}$.

Motivation

The paper opens with the Banach–Tarski paradox and von Neumann's notion of amenability: "Tarski readily proved that amenability is the only obstruction to paradoxical decompositions. However, the known paradoxes relied more prosaically on the existence of non-abelian free subgroups. Therefore, the main open problem in the subject remained for half a century to find non-amenable groups without free subgroups" (p. 1). That problem, the so-called von Neumann conjecture, was answered by Ol'shanskii around 1980, with Tarski monsters. Monod's groups give "straightforward torsion-free counter-examples", "so simple that many additional properties can be established" (p. 1).

Monod's groups are close relatives of Thompson's groups: Thurston's model identifies Thompson's group $F$ with piecewise $\mathrm{PSL}_2(\mathbf{Z})$ maps of the line with rational breakpoints (p. 2). Whether $F$ is amenable is a notorious open problem, and whether $H(\mathbf{Z})$ is amenable is Monod's Problem 12 (p. 2).

Timeline

• 1914–1929. Hausdorff's paradox (1914); Banach–Tarski (1924); von Neumann introduces amenable groups (1929); Tarski characterizes amenability by the absence of paradoxical decompositions.
• 1950s. Day's classes; the question whether every non-amenable group contains a free subgroup of rank two becomes attached to von Neumann's name.
• c. 1965–1975. Thompson's groups $F$, $T$, $V$; Thurston's piecewise projective models of $F$ and $T$.
• 1979–1982. Ol'shanskii proves Tarski monsters non-amenable; Adyan does the same for free Burnside groups.
• 1985. Brin–Squier: groups of piecewise linear homeomorphisms of the line have no free subgroups.
• 2003. Ol'shanskii–Sapir: finitely presented non-amenable groups without free subgroups.
• 2013. Monod: the piecewise projective groups $H(A)$ (this paper).
• 2016. Lodha–Moore: a finitely presented subgroup of Monod's group, non-amenable and without free subgroups.

Setting

The projective line $\mathbf{P}^1$ is OnePoint ℝ, on which $\mathrm{SL}_2(A)$ acts through $\mathrm{GL}_2(\mathbf{R})$ by Möbius transformations (mob, using Mathlib's action on OnePoint). For a subring $A$ of $\mathbf{R}$ (A : Subring ℝ; $\mathbf{Z}$ is ⊥, $\mathbf{R}$ is ⊤), P A is $P_A$, the set of fixed points of hyperbolic elements (trace of absolute value greater than $2$).

A homeomorphism of $\mathbf{P}^1$ is piecewise in $\mathrm{PSL}_2(A)$ with breakpoints in $E$ (IsPiecewiseProjOn A E f) when, off some finite subset of $E$, it agrees near every point with a Möbius transformation from $\mathrm{SL}_2(A)$. Monod's $G$ (Gpp) is the group generated by the homeomorphisms piecewise in $\mathrm{PSL}_2(\mathbf{R})$, with breakpoints anywhere, and $H$ (Hpp) is its stabilizer of $\infty$ (fixInf). For a subring $A$, $G(A)$ (G A) is the subgroup of $G$ generated by its elements that are piecewise in $\mathrm{PSL}_2(A)$ with breakpoints in $P_A$ (IsPiecewiseProj A), and $H(A)$ (H A) is its stabilizer of $\infty$; $H(\mathbf{Z})$ is H ⊥. GRat is the subgroup of $G$ generated by its elements piecewise in $\mathrm{PSL}_2(\mathbf{Z})$ with breakpoints in $\mathbf{Q} \cup \{\infty\}$, and HRat its stabilizer of $\infty$: the rational-breakpoint variants of $G(\mathbf{Z})$ and $H(\mathbf{Z})$ (p. 2).

Amenability is Garrido.IsAmenable (a finitely additive left-invariant probability measure on all subsets), and "no non-abelian free subgroup" is Chou.NoFreeSubgroupOfRankTwo; both are published definitions, in the bundles Garrido_Amenability and Chou_Classes. Co-amenable subgroups (IsCoamenable), inner amenability (IsInnerAmenable) and pointwise stabilizers (fixSubgroup), all on p. 3, are defined in the bundle in the same style.

A relation $R \subseteq X \times X$ is amenable for a measure $\mu$ (IsAmenableRel μ R, p. 2) when it has a left invariant mean in the sense of Connes–Feldman–Weiss: a positive, unital map from bounded measurable functions on $R$ to functions on $X$, linear up to $\mu$-null sets and invariant under the partial transformations of $R$. volP1 is the Lebesgue measure class on $\mathbf{P}^1$.

Target

The goal is Theorem 1, "The group $H(A)$ is non-amenable if $A \neq \mathbf{Z}$" (p. 1), introduced as "the main result of this article". The proof (p. 2) passes to a countable dense subring $A'$ of $A$, compares the orbits of $H(A')$ and $\mathrm{PSL}_2(A')$ on $\mathbf{P}^1 \setminus \{\infty\}$ (Proposition 9), and concludes from two facts about measured equivalence relations: the orbit relation of an amenable group's action is amenable, and, by a theorem of Carrière and Ghys, the orbit relation of $\mathrm{PSL}_2(A')$ on $\mathbf{P}^1$ is not.

The milestones are, in the paper's order: $G(A)$ consists exactly of the elements of $G$ piecewise in $\mathrm{PSL}_2(A)$ with breakpoints in $P_A$; $H = H(\mathbf{R})$; $H$ preserves orientation, is left-orderable and torsion-free; Proposition 9; the countable dense subring; the orbit relation of a measurable action of an amenable group is amenable; the orbit relation of $\mathrm{PSL}_2(A)$ on $\mathbf{P}^1$ is not amenable (Carrière–Ghys, external); Lemma 13 and Theorem 14 leading to Theorem 2 ($H$ has no free subgroups); Corollary 3; Proposition 6 (bi-orderability); Lemma 16, Proposition 7 (co-amenability of pointwise stabilizers), Proposition 15 and Proposition 5 (inner amenability); and Thurston's identification of the rational-breakpoint variants of $H(\mathbf{Z})$ and $G(\mathbf{Z})$ with $F$ and $T$.

Significance

The result. Theorem 1 and Theorem 2 together make $H(A)$, for instance $A = \mathbf{Z}[\sqrt 2]$, a torsion-free counterexample to the von Neumann conjecture, with finitely generated examples (Corollary 3). The groups are concrete enough to carry many further properties (Propositions 5–7).

Formalizing it. Nothing on amenability of groups of homeomorphisms of the line, or on measured equivalence relations, is in Mathlib. Amenability and Følner's theorem are on this platform from Garrido I, the Banach–Tarski paradox from Garrido II, Brin–Squier's theorem from its own mission, and Thompson's $F$ and $T$ (CannonFloydParry, CannonFloydParry_T) from the Cannon–Floyd–Parry missions.

Difficulty

The algebraic half, Theorem 2 and Propositions 5–9, follows Brin–Squier and elementary dynamics on the circle. The analytic half is the passage through measured equivalence relations in the proof of Theorem 1. The mission defines amenability of a relation as Connes–Feldman–Weiss do, by an invariant mean valued in $L^\infty$, which is the form under which an amenable group's orbit relation is amenable without extra set-theoretic hypotheses. The step taken from the literature, that the orbit relation of $\mathrm{PSL}_2(A)$ on $\mathbf{P}^1$ is not amenable for $A$ countable and dense, rests on Carrière–Ghys's theorem and on Zimmer's theory of amenable actions (Adams–Elliott–Giordano). The milestone is proved (Monod.not_isAmenableRel_mob) by an elementary route that needs neither: a ping-pong argument in $\mathrm{SL}_2(A)$ that contradicts an invariant mean directly.

What is left out

• The second sentence of Proposition 6 (no non-trivial homomorphism from a Kazhdan group) and Proposition 8 (actions on CAT(0) spaces): property (T) and CAT(0) spaces are not in Mathlib.
• Proposition 4 ($L^2$-Betti numbers), the remarks on group laws, on the Dixmier problem and on bounded cohomology.
• Remarks 10 and 11, which discuss alternative proofs of the step taken from Carrière–Ghys.

Formalization scope

• $\mathbf{P}^1$ is OnePoint ℝ and $\mathrm{PSL}_2(A)$ acts through Matrix.SpecialLinearGroup (Fin 2) A; since $-1$ acts trivially the orbits are those of $\mathrm{PSL}_2(A)$.
• "Piecewise with finitely many pieces, each an interval" is stated locally: off a finite set of breakpoints, $f$ agrees near each point with one Möbius transformation. Pieces then extend over arcs because two Möbius maps agreeing near a point agree everywhere.
• The groups are subgroups of the homeomorphism group of OnePoint ℝ, each defined as the subgroup generated by the maps the paper describes; the milestones state that $G(A)$ is exactly its set of such maps and that $G = G(\mathbf{R})$.
• An amenable measured equivalence relation (p. 2) is one with a left invariant mean in the sense of Connes–Feldman–Weiss (an operator from $L^\infty$ of the relation to $L^\infty(X, \mu)$, their Definition 6), as in Schmidt, whom the paper cites. The paper describes it as a measurable assignment of means on the orbits, the motivating form in Connes–Feldman–Weiss; for that form, "an amenable group's action produces an amenable relation" is known only assuming CH. $\mathbf{P}^1$ carries its Borel σ-algebra and the Lebesgue measure class (volP1).
• "Metabelian" is the vanishing of the second derived subgroup, and "contains a free abelian group of rank two" is an injective homomorphism from $\mathbf{Z}^2$.
• Reused platform items, which solutions may import: the amenability and free-subgroup definitions (Garrido, Chou), Brin–Squier's Theorem 3.1, and Thompson's $F$ and $T$ (Cannon–Floyd–Parry).

Selected references

• N. Monod, Groups of piecewise projective homeomorphisms, Proc. Natl. Acad. Sci. USA 110 (2013) 4524–4527. doi:10.1073/pnas.1218426110
• Y. Carrière, É. Ghys, Relations d'équivalence moyennables sur les groupes de Lie, C. R. Acad. Sci. Paris Sér. I Math. 300 (1985) 677–680 (no DOI).
• A. Connes, J. Feldman, B. Weiss, An amenable equivalence relation is generated by a single transformation, Ergodic Theory Dynam. Systems 1 (1981) 431–450. doi:10.1017/S014338570000136X
• K. Schmidt, Algebraic ideas in ergodic theory, CBMS Regional Conference Series in Mathematics 76, AMS (1990) (a book; no DOI).
• M. G. Brin, C. C. Squier, Groups of piecewise linear homeomorphisms of the real line, Invent. Math. 79 (1985) 485–498. doi:10.1007/BF01388519