Concrete von Neumann algebras as C⋆-algebras

A concrete von Neumann algebra is norm closed, since it is a double commutant. Its elements therefore form a C⋆-algebra with the inherited operator norm and adjoint. This allows the abstract continuous functional calculus and positive-functional APIs to be applied directly to concrete algebras, including those acting on the zero Hilbert space.

The instances use Mathlib's generic subobject constructions, in particular StarSubalgebra.cstarAlgebra. The underlying star subalgebra has the same instances; no new norm, completion, or algebra carrier is introduced.

instance VonNeumannAlgebra.instSMulMemClass {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : SMulMemClass (VonNeumannAlgebra H) ℂ (H →L[ℂ] H)

Concrete von Neumann algebras are closed under complex scalar multiplication.

instance VonNeumannAlgebra.isClosed {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) : IsClosed ↑M

A concrete von Neumann algebra is closed in the operator norm topology.

instance VonNeumannAlgebra.instIsClosedToStarSubalgebra {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) : IsClosed ↑M.toStarSubalgebra

The underlying star subalgebra is closed in the same operator norm topology.