Expansion in groups without Følner sets

If a group G has no Følner sets, some finite set S ⊆ G expands every finite subset of G by a fixed factor c > 1:

c · |F| ≤ |S • F|        for every finite F ⊆ G.

Indeed, the failure of the finite-test Følner condition gives a finite K ⊆ G and ε > 0 such that every finite nonempty F has some g ∈ K with |gF △ F| ≥ ε |F|. Since |gF △ F| = 2 |gF \ F|, the set S = {1} ∪ K satisfies |S • F| ≥ |F ∪ gF| ≥ (1 + ε/2) |F|. Iterating, a pointwise power of S expands every finite set by any prescribed natural factor k, and Hall's marriage theorem turns expansion by k into an injection j : G × Fin k → G with j (x, i) = d * x for d in a fixed finite set.

By the averaging criterion TauCeti.Amenable.of_hasFoelnerSets, a nonamenable group has no Følner sets, for any group topology. For k = 2 the injection exhibits two disjoint subsets of G, each the image of G under finitely many left translations of pieces; this is the combinatorial core of the proof that a nonamenable discrete group is paradoxical (the hard direction of Tarski's alternative).

Main results

• TauCeti.exists_mul_card_le_card_smul_of_not_hasFoelnerSets: a group without Følner sets has, for each natural k, a finite set D with k · |F| ≤ |D • F| for all finite F.
• TauCeti.exists_injective_mul_of_not_hasFoelnerSets: a group without Følner sets has, for each natural k, a finite set D and an injection j : G × Fin k → G with j (x, i) = d * x for some d ∈ D.
• TauCeti.exists_injective_mul_of_not_amenable: the same for a nonamenable topological group.

References

• A. Garrido, An introduction to amenable groups, proof of Theorem 1.11 and Theorem 1.15.
• T. Ceccherini-Silberstein, R. Grigorchuk, P. de la Harpe, Amenability and paradoxical decompositions for pseudogroups and for discrete metric spaces, Theorems 7 and 35.

theorem TauCeti.exists_mul_card_le_card_smul_of_not_hasFoelnerSets {G : Type u_1} [Group G] [DecidableEq G] (h : ¬HasFoelnerSets G) (k : ℕ) : ∃ (D : Finset G), ∀ (F : Finset G), k * F.card ≤ (D • F).card

A group without Følner sets has, for every natural number k, a finite set D expanding every finite set by the factor k: k · |F| ≤ |D • F|.

theorem TauCeti.exists_injective_mul_of_not_hasFoelnerSets {G : Type u_1} [Group G] (h : ¬HasFoelnerSets G) (k : ℕ) : ∃ (D : Finset G) (j : G × Fin k → G), Function.Injective j ∧ ∀ (p : G × Fin k), ∃ d ∈ D, d * p.1 = j p

A group without Følner sets has, for every natural number k, a finite set D and an injective map j : G × Fin k → G such that each j (x, i) is d * x for some d ∈ D.

theorem TauCeti.exists_injective_mul_of_not_amenable {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (h : ¬Amenable G) (k : ℕ) : ∃ (D : Finset G) (j : G × Fin k → G), Function.Injective j ∧ ∀ (p : G × Fin k), ∃ d ∈ D, d * p.1 = j p

A nonamenable topological group has, for every natural number k, a finite set D and an injective map j : G × Fin k → G such that each j (x, i) is d * x for some d ∈ D.