Documentation

TauCeti.Topology.Algebra.Group.UCB.CompRight

Pullback of bounded uniformly continuous functions along continuous homomorphisms #

For a continuous homomorphism φ : G →ₜ* H of topological groups, precomposition f ↦ f ∘ φ maps TauCeti.UCB H to TauCeti.UCB G: if f (u * y) is uniformly close to f y for all u near 1 in H, then f (φ u * φ x) is uniformly close to f (φ x) for all u near 1 in G, by continuity of φ at 1. This file bundles the pullback as a unital algebra homomorphism

TauCeti.UCB.compRightAlgHom φ : UCB H →ₐ[ℝ] UCB G,

which preserves the pointwise order, does not increase the supremum norm and intertwines the left translation L_(φ g) of UCB H with the left translation L_g of UCB G. It is an isometry when φ is surjective. Dually, a mean on UCB G pushes forward to a mean on UCB H, which is how amenability is transported along surjective continuous homomorphisms.

Main definitions #

Main results #

References #

source
theorem TauCeti.compContinuous_mem_ucb {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {f : BoundedContinuousFunction H ℝ} (hf : f ∈ ucb H) (φ : G →ₜ* H) :
f.compContinuous ↑φ ∈ ucb G

The pullback x ↦ f (φ x) of a function in ucb H along a continuous homomorphism φ : G →ₜ* H lies in ucb G.

source
def TauCeti.UCB.compRightAlgHom {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : G →ₜ* H) :
UCB H →ₐ[ℝ] UCB G

The pullback f ↦ f ∘ φ along a continuous homomorphism φ : G →ₜ* H, as a unital algebra homomorphism from UCB H to UCB G.

Instances For
    source
    theorem TauCeti.UCB.coe_compRightAlgHom {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : G →ₜ* H) (f : UCB H) :
    ↑((compRightAlgHom φ) f) = (↑f).compContinuous ↑φ

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

    source
    @[simp]
    theorem TauCeti.UCB.compRightAlgHom_apply {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : G →ₜ* H) (f : UCB H) (x : G) :
    ↑((compRightAlgHom φ) f) x = ↑f (φ x)
    source
    @[simp]
    theorem TauCeti.UCB.compRightAlgHom_id {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    compRightAlgHom (ContinuousMonoidHom.id G) = AlgHom.id ℝ (UCB G)

    The pullback along the identity is the identity.

    source
    theorem TauCeti.UCB.compRightAlgHom_comp {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) :
    compRightAlgHom (ψ.comp φ) = (compRightAlgHom φ).comp (compRightAlgHom ψ)

    Pulling back along ψ ∘ φ is pulling back along ψ and then along φ.

    source
    theorem TauCeti.UCB.monotone_compRightAlgHom {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : G →ₜ* H) :
    Monotone ⇑(compRightAlgHom φ)

    The pullback preserves the pointwise order.

    source
    @[simp]
    theorem TauCeti.UCB.compRightAlgHom_le_compRightAlgHom_iff {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {φ : G →ₜ* H} (hφ : Function.Surjective ⇑φ) {f f' : UCB H} :
    (compRightAlgHom φ) f ≤ (compRightAlgHom φ) f' ↔ f ≤ f'

    Along a surjective homomorphism, the pullback preserves and reflects the pointwise order.

    source
    theorem TauCeti.UCB.norm_compRightAlgHom_apply_le {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : G →ₜ* H) (f : UCB H) :
    ‖(compRightAlgHom φ) f‖ ≤ ‖f‖

    The pullback does not increase the supremum norm.

    source
    theorem TauCeti.UCB.norm_compRightAlgHom_apply {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {φ : G →ₜ* H} (hφ : Function.Surjective ⇑φ) (f : UCB H) :
    ‖(compRightAlgHom φ) f‖ = ‖f‖

    Along a surjective homomorphism, the pullback preserves the supremum norm.

    source
    theorem TauCeti.UCB.compRightAlgHom_leftTranslation {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : G →ₜ* H) (g : G) (f : UCB H) :
    (compRightAlgHom φ) ((leftTranslation (φ g)) f) = (leftTranslation g) ((compRightAlgHom φ) f)

    The pullback intertwines left translation by φ g with left translation by g.

    source
    theorem TauCeti.UCB.compRightAlgHom_rightTranslation {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : G →ₜ* H) (g : G) (f : UCB H) :
    (compRightAlgHom φ) ((rightTranslation (φ g)) f) = (rightTranslation g) ((compRightAlgHom φ) f)

    The pullback intertwines right translation by φ g with right translation by g.