Amenable topological groups

A mean m on TauCeti.UCB G is left invariant when m (L_g f) = m f for every g : G and every f, where (L_g f)(x) = f (g⁻¹ * x) is the left translation. A topological group is amenable when UCB G carries a left-invariant mean. No separation, local compactness, countability or generation hypothesis is part of the definition.

A mean m on UCB G pushes forward along a continuous homomorphism φ : G →ₜ* H to the mean f ↦ m (f ∘ φ) on UCB H. Since (L_(φ g) f) ∘ φ = L_g (f ∘ φ), the pushforward of a left-invariant mean is invariant under translation by the range of φ, and, by continuity of k ↦ m ((L_k f) ∘ φ), by its closure. So the pushforward along a homomorphism with dense range is left invariant. Hence amenability passes to the target of a continuous homomorphism with dense range, in particular to images under surjective continuous homomorphisms, and is invariant under isomorphisms of topological groups.

Main definitions

• TauCeti.Mean.IsLeftInvariant: m (L_g f) = m f for all g and f.
• TauCeti.Mean.map φ: the pushforward of means along a continuous homomorphism φ.
• TauCeti.Amenable G: UCB G carries a left-invariant mean.

Main results

• TauCeti.Mean.convex_toContinuousLinearMap_image_setOf_isLeftInvariant: the left-invariant means form a convex set.
• TauCeti.Mean.IsLeftInvariant.map: pushforward along a continuous homomorphism with dense range preserves left invariance.
• TauCeti.Amenable.of_denseRange: amenability passes to the target of a continuous homomorphism with dense range, in particular to images under surjective continuous homomorphisms.
• ContinuousMulEquiv.amenable_iff: amenability is invariant under isomorphisms of topological groups.

References

• B. Bekka, P. de la Harpe, A. Valette, Kazhdan's Property (T), Appendix G.1, and Proposition G.2.2 for quotients.

def TauCeti.Mean.IsLeftInvariant {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (m : Mean G) : Prop

A mean m on UCB G is left invariant when m (L_g f) = m f for every g and f, where (L_g f)(x) = f (g⁻¹ * x).

theorem TauCeti.Mean.isLeftInvariant_iff {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {m : Mean G} : m.IsLeftInvariant ↔ ∀ (g : G) (f : UCB G), m ((UCB.leftTranslation g) f) = m f

The defining property of a left-invariant mean.

@[simp]

theorem TauCeti.Mean.IsLeftInvariant.apply_leftTranslation {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {m : Mean G} (hm : m.IsLeftInvariant) (g : G) (f : UCB G) : m ((UCB.leftTranslation g) f) = m f

A left-invariant mean takes the same value at a function and at its left translates.

theorem TauCeti.Mean.convex_toContinuousLinearMap_image_setOf_isLeftInvariant {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Convex ℝ (toContinuousLinearMap '' {m : Mean G | m.IsLeftInvariant})

The left-invariant means on UCB G form a convex set of continuous linear functionals.

noncomputable def TauCeti.Mean.map {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : G →ₜ* H) (m : Mean G) : Mean H

The pushforward f ↦ m (f ∘ φ) of a mean m on UCB G along a continuous homomorphism φ : G →ₜ* H, as a mean on UCB H.

@[simp]

theorem TauCeti.Mean.map_apply {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : G →ₜ* H) (m : Mean G) (f : UCB H) : (map φ m) f = m ((UCB.compRightAlgHom φ) f)

@[simp]

theorem TauCeti.Mean.map_id {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (m : Mean G) : map (ContinuousMonoidHom.id G) m = m

The pushforward along the identity is the identity.

@[simp]

theorem TauCeti.Mean.map_map {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [Group K] [TopologicalSpace K] [IsTopologicalGroup K] (ψ : H →ₜ* K) (φ : G →ₜ* H) (m : Mean G) : map ψ (map φ m) = map (ψ.comp φ) m

Pushing forward along φ and then along ψ is pushing forward along ψ ∘ φ.

theorem TauCeti.Mean.IsLeftInvariant.map_apply_leftTranslation {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {m : Mean G} (hm : m.IsLeftInvariant) (φ : G →ₜ* H) (g : G) (f : UCB H) : (Mean.map φ m) ((UCB.leftTranslation (φ g)) f) = (Mean.map φ m) f

The pushforward of a left-invariant mean along a continuous homomorphism φ is invariant under left translation by the elements φ g of the range of φ.

theorem TauCeti.Mean.IsLeftInvariant.map {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {m : Mean G} (hm : m.IsLeftInvariant) {φ : G →ₜ* H} (hφ : DenseRange ⇑φ) : (Mean.map φ m).IsLeftInvariant

The pushforward of a left-invariant mean along a continuous homomorphism with dense range is left invariant.

class TauCeti.Amenable (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Prop

A topological group G is amenable when UCB G carries a left-invariant mean.

• exists_isLeftInvariant : ∃ (m : Mean G), m.IsLeftInvariant

  An amenable group has a left-invariant mean on UCB G.

theorem TauCeti.amenable_iff (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Amenable G ↔ ∃ (m : Mean G), m.IsLeftInvariant

A topological group is amenable exactly when UCB G carries a left-invariant mean.

theorem TauCeti.Amenable.of_denseRange {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [Amenable G] (φ : G →ₜ* H) (hφ : DenseRange ⇑φ) : Amenable H

The target of a continuous homomorphism with dense range from an amenable topological group is amenable; in particular, so is the image under a surjective continuous homomorphism.

theorem TauCeti.Amenable.of_le {G : Type u_1} [Group G] {t₁ t₂ : TopologicalSpace G} [IsTopologicalGroup G] [IsTopologicalGroup G] (h : t₁ ≤ t₂) (ha : Amenable G) : Amenable G

Amenability passes from a finer group topology to a coarser group topology.

theorem ContinuousMulEquiv.amenable_iff {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : G ≃ₜ* H) : TauCeti.Amenable G ↔ TauCeti.Amenable H

Amenability is invariant under isomorphisms of topological groups.