Bounded functions on a discrete group

On a discrete group every bounded continuous function is uniformly continuous for the right uniformity. Thus TauCeti.UCB G is the entire algebra G →ᵇ ℝ. The identification preserves the supremum norm, pointwise order, constants, and left and right translations. Since every function on a discrete space is continuous, this is the bounded-function space used for finitely additive probabilities and discrete invariant means.

For the same reason, precomposition f ↦ f ∘ r with an arbitrary map r : G → H into a topological group sends UCB H to UCB G; this is TauCeti.UCB.compRightAlgHomOfDiscrete r. When r is equivariant along a homomorphism φ : H →* G, in the sense that r (φ h * x) = h * r x, the pullback intertwines L_h with L_(φ h). Such maps arise as the retractions of a discrete group onto a subgroup along a choice of right coset representatives.

References

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

@[simp]

theorem TauCeti.ucb_eq_top {G : Type u_1} [Group G] [TopologicalSpace G] [DiscreteTopology G] : ucb G = ⊤

On a discrete group the UCB subalgebra is the entire bounded-function algebra.

noncomputable def TauCeti.UCB.discreteAlgEquiv (G : Type u_1) [Group G] [TopologicalSpace G] [DiscreteTopology G] : UCB G ≃ₐ[ℝ] BoundedContinuousFunction G ℝ

The canonical algebra equivalence from UCB to all bounded functions on a discrete group.

@[simp]

theorem TauCeti.UCB.discreteAlgEquiv_apply {G : Type u_1} [Group G] [TopologicalSpace G] [DiscreteTopology G] (f : UCB G) : (discreteAlgEquiv G) f = ↑f

@[simp]

theorem TauCeti.UCB.coe_discreteAlgEquiv_symm {G : Type u_1} [Group G] [TopologicalSpace G] [DiscreteTopology G] (f : BoundedContinuousFunction G ℝ) : ↑((discreteAlgEquiv G).symm f) = f

@[simp]

theorem TauCeti.UCB.discreteAlgEquiv_symm_compContinuous_mulLeft {G : Type u_1} [Group G] [TopologicalSpace G] [DiscreteTopology G] (g : G) (f : BoundedContinuousFunction G ℝ) : (discreteAlgEquiv G).symm (f.compContinuous (ContinuousMap.mulLeft g⁻¹)) = (leftTranslation g) ((discreteAlgEquiv G).symm f)

The inverse discrete identification intertwines left translation.

@[simp]

theorem TauCeti.UCB.discreteAlgEquiv_symm_compContinuous_mulRight {G : Type u_1} [Group G] [TopologicalSpace G] [DiscreteTopology G] (g : G) (f : BoundedContinuousFunction G ℝ) : (discreteAlgEquiv G).symm (f.compContinuous (ContinuousMap.mulRight g)) = (rightTranslation g) ((discreteAlgEquiv G).symm f)

The inverse discrete identification intertwines right translation.

@[simp]

theorem TauCeti.UCB.discreteAlgEquiv_symm_le_discreteAlgEquiv_symm_iff {G : Type u_1} [Group G] [TopologicalSpace G] [DiscreteTopology G] {f h : BoundedContinuousFunction G ℝ} : (discreteAlgEquiv G).symm f ≤ (discreteAlgEquiv G).symm h ↔ f ≤ h

The inverse discrete identification preserves and reflects the pointwise order.

noncomputable def TauCeti.UCB.discreteLinearIsometryEquiv (G : Type u_1) [Group G] [TopologicalSpace G] [DiscreteTopology G] : UCB G ≃ₗᵢ[ℝ] BoundedContinuousFunction G ℝ

The discrete identification as a linear isometry equivalence for the supremum norm.

@[simp]

theorem TauCeti.UCB.discreteLinearIsometryEquiv_apply {G : Type u_1} [Group G] [TopologicalSpace G] [DiscreteTopology G] (f : UCB G) : (discreteLinearIsometryEquiv G) f = ↑f

@[simp]

theorem TauCeti.UCB.discreteLinearIsometryEquiv_symm_apply {G : Type u_1} [Group G] [TopologicalSpace G] [DiscreteTopology G] (f : BoundedContinuousFunction G ℝ) : (discreteLinearIsometryEquiv G).symm f = (discreteAlgEquiv G).symm f

noncomputable def TauCeti.UCB.compRightAlgHomOfDiscrete {G : Type u_1} [Group G] [TopologicalSpace G] [DiscreteTopology G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (r : G → H) : UCB H →ₐ[ℝ] UCB G

On a discrete group G, the pullback f ↦ f ∘ r along an arbitrary map r : G → H, as a unital algebra homomorphism from UCB H to UCB G.

theorem TauCeti.UCB.coe_compRightAlgHomOfDiscrete {G : Type u_1} [Group G] [TopologicalSpace G] [DiscreteTopology G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (r : G → H) (f : UCB H) : ↑((compRightAlgHomOfDiscrete r) f) = (↑f).compContinuous { toFun := r, continuous_toFun := ⋯ }

The pullback f ∘ r is the precomposition of f with r.

@[simp]

theorem TauCeti.UCB.compRightAlgHomOfDiscrete_apply {G : Type u_1} [Group G] [TopologicalSpace G] [DiscreteTopology G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (r : G → H) (f : UCB H) (x : G) : ↑((compRightAlgHomOfDiscrete r) f) x = ↑f (r x)

theorem TauCeti.UCB.compRightAlgHomOfDiscrete_coe {G : Type u_1} [Group G] [TopologicalSpace G] [DiscreteTopology G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : G →ₜ* H) : compRightAlgHomOfDiscrete ⇑φ = compRightAlgHom φ

Along a continuous homomorphism, the pullback out of a discrete group is the pullback TauCeti.UCB.compRightAlgHom.

theorem TauCeti.UCB.monotone_compRightAlgHomOfDiscrete {G : Type u_1} [Group G] [TopologicalSpace G] [DiscreteTopology G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (r : G → H) : Monotone ⇑(compRightAlgHomOfDiscrete r)

The pullback preserves the pointwise order.

theorem TauCeti.UCB.norm_compRightAlgHomOfDiscrete_apply_le {G : Type u_1} [Group G] [TopologicalSpace G] [DiscreteTopology G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (r : G → H) (f : UCB H) : ‖(compRightAlgHomOfDiscrete r) f‖ ≤ ‖f‖

The pullback does not increase the supremum norm.

theorem TauCeti.UCB.compRightAlgHomOfDiscrete_leftTranslation {G : Type u_1} [Group G] [TopologicalSpace G] [DiscreteTopology G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : H →* G) {r : G → H} (hr : ∀ (h : H) (x : G), r (φ h * x) = h * r x) (h : H) (f : UCB H) : (compRightAlgHomOfDiscrete r) ((leftTranslation h) f) = (leftTranslation (φ h)) ((compRightAlgHomOfDiscrete r) f)

If r (φ h * x) = h * r x for a homomorphism φ : H →* G, then the pullback along r intertwines left translation by h with left translation by φ h.