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 = StarAddMonoid.mk ⋯

@[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 = StarRing.mk ⋯

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