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 β]
:
Equations
- BoundedContinuousFunction.instStarAddMonoid = StarAddMonoid.mk ⋯
@[simp]
theorem
BoundedContinuousFunction.coe_star
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[SeminormedAddCommGroup β]
[StarAddMonoid β]
[NormedStarGroup β]
(f : BoundedContinuousFunction α β)
:
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 : α)
:
instance
BoundedContinuousFunction.instNormedStarGroup
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[SeminormedAddCommGroup β]
[StarAddMonoid β]
[NormedStarGroup β]
:
Equations
- ⋯ = ⋯
instance
BoundedContinuousFunction.instStarModule
{α : Type u}
{β : Type v}
{𝕜 : Type u_2}
[NormedField 𝕜]
[StarRing 𝕜]
[TopologicalSpace α]
[SeminormedAddCommGroup β]
[StarAddMonoid β]
[NormedStarGroup β]
[NormedSpace 𝕜 β]
[StarModule 𝕜 β]
:
StarModule 𝕜 (BoundedContinuousFunction α β)
Equations
- ⋯ = ⋯
instance
BoundedContinuousFunction.instStarRing
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[NonUnitalNormedRing β]
[StarRing β]
[NormedStarGroup β]
:
Equations
- BoundedContinuousFunction.instStarRing = StarRing.mk ⋯
instance
BoundedContinuousFunction.instCStarRing
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[NonUnitalNormedRing β]
[StarRing β]
[CStarRing β]
:
Equations
- ⋯ = ⋯