Directed unions of amenable subgroups

A topological group is amenable when it is exhausted, finite set by finite set, by images of amenable topological groups. Given continuous homomorphisms φ i : K i →ₜ* G from amenable groups, push a left-invariant mean m on UCB (K i) forward to the mean f ↦ m (f ∘ φ i) on UCB G; since (L_(φ i k) f) ∘ φ i = L_k (f ∘ φ i), this mean satisfies every invariance equation m (L_g f) = m f with g in the range of φ i. If every finite subset of G lies in the range of some φ i, then every finite family of invariance equations has a solution, and the finite-intersection criterion TauCeti.amenable_iff_forall_finset_exists, which rests on the weak-* compactness of the space of means, produces a left-invariant mean on UCB G.

Specializing to inclusions of subgroups, with their subspace topologies, gives the closure of amenability under directed unions: if H i is a nonempty directed family of amenable subgroups of G, then the subgroup ⨆ i, H i = ⋃ i, H i is amenable, and G is amenable when this union is all of G. Since every finite subset of G lies in a finitely generated subgroup, a topological group whose finitely generated subgroups are all amenable is amenable.

No discreteness is needed: the subgroups carry the subspace topology, and a function in UCB G restricts to a function in the UCB space of each of them.

Main results

• TauCeti.Amenable.of_forall_finset_subset_range: a topological group is amenable if each of its finite subsets lies in the range of a continuous homomorphism from an amenable topological group, drawn from a fixed family.
• TauCeti.amenable_iSup_of_directed: the union of a nonempty directed family of amenable subgroups is an amenable subgroup.
• TauCeti.Amenable.of_directed_of_iSup_eq_top: a topological group which is the union of a nonempty directed family of amenable subgroups is amenable.
• TauCeti.Amenable.of_forall_fg: a topological group whose finitely generated subgroups are amenable is amenable.

References

• B. Bekka, P. de la Harpe, A. Valette, Kazhdan's Property (T), Proposition G.2.2.
• A. Garrido, An introduction to amenable groups, Proposition 2.2.

theorem TauCeti.Amenable.of_forall_finset_subset_range {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {ι : Type u_2} {K : ι → Type u_3} [(i : ι) → Group (K i)] [(i : ι) → TopologicalSpace (K i)] [∀ (i : ι), IsTopologicalGroup (K i)] [∀ (i : ι), Amenable (K i)] (φ : (i : ι) → K i →ₜ* G) (h : ∀ (s : Finset G), ∃ (i : ι), ↑s ⊆ Set.range ⇑(φ i)) : Amenable G

A topological group G is amenable if, for a family of continuous homomorphisms φ i : K i →ₜ* G from amenable topological groups, every finite subset of G lies in the range of some φ i.

theorem TauCeti.amenable_iSup_of_directed {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {ι : Type u_2} [Nonempty ι] {H : ι → Subgroup G} (hH : Directed (fun (x1 x2 : Subgroup G) => x1 ≤ x2) H) [∀ (i : ι), Amenable ↥(H i)] : Amenable ↥(⨆ (i : ι), H i)

The union ⨆ i, H i of a nonempty directed family of amenable subgroups H i of a topological group is an amenable subgroup.

theorem TauCeti.Amenable.of_directed_of_iSup_eq_top {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {ι : Type u_2} [Nonempty ι] {H : ι → Subgroup G} (hH : Directed (fun (x1 x2 : Subgroup G) => x1 ≤ x2) H) (htop : ⨆ (i : ι), H i = ⊤) [∀ (i : ι), Amenable ↥(H i)] : Amenable G

A topological group which is the union of a nonempty directed family of amenable subgroups is amenable.

theorem TauCeti.Amenable.of_forall_fg {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (h : ∀ (K : Subgroup G), K.FG → Amenable ↥K) : Amenable G

A topological group all of whose finitely generated subgroups are amenable is amenable.