Star structures on bounded continuous functions

Star structures

In this section, if β is a normed ⋆-group, then so is the space of bounded continuous functions from α to β, by using the star operation pointwise.

If 𝕜 is normed field and a ⋆-ring over which β is a normed algebra and a star module, then the space of bounded continuous functions from α to β is a star module.

If β is a ⋆-ring in addition to being a normed ⋆-group, then α →ᵇ β inherits a ⋆-ring structure.

In summary, if β is a C⋆-algebra over 𝕜, then so is α →ᵇ β; note that completeness is guaranteed when β is complete (see BoundedContinuousFunction.complete).

instance BoundedContinuousFunction.instStarAddMonoid {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] [StarAddMonoid β] [NormedStarGroup β] : StarAddMonoid (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instStarAddMonoid = { star := fun (f : BoundedContinuousFunction α β) => BoundedContinuousFunction.comp star ⋯ f, star_involutive := ⋯, star_add := ⋯ }

@[simp]

theorem BoundedContinuousFunction.coe_star {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] [StarAddMonoid β] [NormedStarGroup β] (f : BoundedContinuousFunction α β) : ⇑(star f) = star ⇑f

The right-hand side of this equality can be parsed star ∘ ⇑f because of the instance Pi.instStarForAll. Upon inspecting the goal, one sees ⊢ ↑(star f) = star ↑f.

@[simp]

theorem BoundedContinuousFunction.star_apply {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] [StarAddMonoid β] [NormedStarGroup β] (f : BoundedContinuousFunction α β) (x : α) : (star f) x = star (f x)

instance BoundedContinuousFunction.instNormedStarGroup {α : Type u} {β : Type v} [TopologicalSpace α] [SeminormedAddCommGroup β] [StarAddMonoid β] [NormedStarGroup β] : NormedStarGroup (BoundedContinuousFunction α β)

instance BoundedContinuousFunction.instStarModule {α : Type u} {β : Type v} {𝕜 : Type u_2} [NormedField 𝕜] [StarRing 𝕜] [TopologicalSpace α] [SeminormedAddCommGroup β] [StarAddMonoid β] [NormedStarGroup β] [NormedSpace 𝕜 β] [StarModule 𝕜 β] : StarModule 𝕜 (BoundedContinuousFunction α β)

instance BoundedContinuousFunction.instStarRing {α : Type u} {β : Type v} [TopologicalSpace α] [NonUnitalNormedRing β] [StarRing β] [NormedStarGroup β] : StarRing (BoundedContinuousFunction α β)

Equations

• BoundedContinuousFunction.instStarRing = { toInvolutiveStar := BoundedContinuousFunction.instStarAddMonoid.toInvolutiveStar, star_mul := ⋯, star_add := ⋯ }

instance BoundedContinuousFunction.instCStarRing {α : Type u} {β : Type v} [TopologicalSpace α] [NonUnitalNormedRing β] [StarRing β] [CStarRing β] : CStarRing (BoundedContinuousFunction α β)

def BoundedContinuousFunction.toContinuousMapStarₐ {α : Type u} {β : Type v} (𝕜 : Type u_2) [NormedField 𝕜] [TopologicalSpace α] [NormedRing β] [NormedAlgebra 𝕜 β] [StarAddMonoid β] [NormedStarGroup β] : BoundedContinuousFunction α β →⋆ₐ[𝕜] C(α, β)

The ⋆-algebra-homomorphism forgetting that a bounded continuous function is bounded.

Equations

• BoundedContinuousFunction.toContinuousMapStarₐ 𝕜 = { toAlgHom := BoundedContinuousFunction.toContinuousMapₐ 𝕜, map_star' := ⋯ }

@[simp]

theorem BoundedContinuousFunction.toContinuousMapStarₐ_apply_apply {α : Type u} {β : Type v} (𝕜 : Type u_2) [NormedField 𝕜] [TopologicalSpace α] [NormedRing β] [NormedAlgebra 𝕜 β] [StarAddMonoid β] [NormedStarGroup β] (f : BoundedContinuousFunction α β) (a : α) : ((toContinuousMapStarₐ 𝕜) f) a = f a

@[simp]

theorem BoundedContinuousFunction.coe_toContinuousMapStarₐ {α : Type u} {β : Type v} (𝕜 : Type u_2) [NormedField 𝕜] [TopologicalSpace α] [NormedRing β] [NormedAlgebra 𝕜 β] [StarAddMonoid β] [NormedStarGroup β] (f : BoundedContinuousFunction α β) : ⇑((toContinuousMapStarₐ 𝕜) f) = ⇑f