Tarski's alternative for the left regular action

A discrete group G is amenable exactly when it is not paradoxical for its left regular action: exactly one of a left-invariant finitely additive probability on all subsets of G and a finite paradoxical decomposition of G exists.

If G has Følner sets, it is amenable for the discrete topology, so it carries a left-invariant finitely additive probability on all of its subsets (TauCeti.Amenable.exists_invariantContent), and such a probability rules out a paradoxical decomposition (TauCeti.not_paradoxical_univ_of_addContent).

Conversely, if G has no Følner sets, expansion and Hall's marriage theorem give a finite set D ⊆ G and an injection j : G × Fin 2 → G with j (x, i) = d * x for some d ∈ D (TauCeti.exists_injective_mul_of_not_hasFoelnerSets). For each i, the injective map x ↦ j (x, i) moves every point by one of the finitely many elements of D, so G is equidecomposable with its range. The two ranges are disjoint since j is injective, so they are two disjoint copies of G inside G, and the subcopy criterion TauCeti.paradoxical_iff_exists_subset gives a paradoxical decomposition of G.

Neither direction needs a countability assumption on G. The statements in terms of Følner sets involve no topology; by the Følner characterization TauCeti.amenable_iff_hasFoelnerSets they become statements about amenability of discrete groups.

Main results

• TauCeti.paradoxical_univ_of_not_hasFoelnerSets: a group without Følner sets is paradoxical for its left regular action.
• TauCeti.hasFoelnerSets_iff_not_paradoxical_univ: a group has Følner sets exactly when it is not paradoxical for its left regular action.
• TauCeti.paradoxical_univ_of_not_amenable: a nonamenable topological group is paradoxical for its left regular action.
• TauCeti.amenable_iff_not_paradoxical_univ: Tarski's alternative, a discrete group is amenable exactly when it is not paradoxical for its left regular action.

References

• A. Garrido, An introduction to amenable groups, Theorem 1.11 (for X = E = G) and Theorem 1.15.
• T. Ceccherini-Silberstein, R. Grigorchuk, P. de la Harpe, Amenability and paradoxical decompositions for pseudogroups and for discrete metric spaces, Theorem 7.

theorem TauCeti.paradoxical_univ_of_not_hasFoelnerSets {G : Type u_1} [Group G] (h : ¬HasFoelnerSets G) : Paradoxical G Set.univ

A group without Følner sets is paradoxical for its left regular action.

theorem TauCeti.hasFoelnerSets_iff_not_paradoxical_univ {G : Type u_1} [Group G] : HasFoelnerSets G ↔ ¬Paradoxical G Set.univ

Tarski's alternative, topology-free form: a group has Følner sets exactly when it is not paradoxical for its left regular action.

theorem TauCeti.paradoxical_univ_of_not_amenable {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (h : ¬Amenable G) : Paradoxical G Set.univ

A nonamenable topological group is paradoxical for its left regular action.

theorem TauCeti.amenable_iff_not_paradoxical_univ {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] : Amenable G ↔ ¬Paradoxical G Set.univ

Tarski's alternative: a discrete group is amenable exactly when it is not paradoxical for its left regular action.