The bicommutant theorem

For a unital star subalgebra of bounded operators on a complete real or complex Hilbert space, both its strong operator closure and its weak operator closure are its double commutant. In particular, equality with the double commutant is equivalent to closedness in either operator topology.

The closures are taken on Mathlib's separate topology copies, not in the operator norm. For a concrete complex von Neumann algebra this gives strong and weak operator closedness; for a generated algebra it identifies the closure of the star algebra generated by the original set (VonNeumannAlgebra.image_ofCLM_adjoin_eq_closure). Taking the star algebra first is essential for a set not closed under adjoints.

Since operator balls are weak operator compact, weak operator closedness makes every closed norm ball of a concrete von Neumann algebra weak operator compact.

The approximation input is the finite-vector density theorem in TauCeti.Analysis.VonNeumannAlgebra.Density.

The same holds for self-adjoint parts: the strong and weak operator closures of the self-adjoint elements of the algebra are the self-adjoint elements of the double commutant. The weak form applies the weak-operator continuous map A ↦ 2⁻¹ • (A + A⋆) to the bicommutant theorem; the strong form follows because the self-adjoint part is convex, so its two closures agree. This is the density statement used in the proof of the Kaplansky density theorem.

References

Kadison–Ringrose, Fundamentals of the Theory of Operator Algebras I, Theorem 5.3.1, and the proof of Theorem 5.3.5 for the self-adjoint parts.

theorem StarSubalgebra.closure_image_toPointwiseConvergenceCLM {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (S : StarSubalgebra 𝕜 (H →L[𝕜] H)) : closure (⇑(ContinuousLinearMap.toPointwiseConvergenceCLM 𝕜 (RingHom.id 𝕜) H H) '' ↑S) = ⇑(ContinuousLinearMap.toPointwiseConvergenceCLM 𝕜 (RingHom.id 𝕜) H H) '' (↑S).centralizer.centralizer

The strong operator closure of a unital star subalgebra is its double commutant.

theorem StarSubalgebra.closure_image_ofCLM {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (S : StarSubalgebra 𝕜 (H →L[𝕜] H)) : closure (ContinuousLinearMapWOT.ofCLM '' ↑S) = ContinuousLinearMapWOT.ofCLM '' (↑S).centralizer.centralizer

The weak operator closure of a unital star subalgebra is its double commutant.

theorem StarSubalgebra.closure_image_ofCLM_inter_selfAdjoint {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (S : StarSubalgebra 𝕜 (H →L[𝕜] H)) : closure (ContinuousLinearMapWOT.ofCLM '' (↑S ∩ ↑(selfAdjoint (H →L[𝕜] H)))) = ContinuousLinearMapWOT.ofCLM '' ((↑S).centralizer.centralizer ∩ ↑(selfAdjoint (H →L[𝕜] H)))

The weak operator closure of the self-adjoint part of a unital star subalgebra is the self-adjoint part of its double commutant.

theorem StarSubalgebra.closure_image_toPointwiseConvergenceCLM_inter_selfAdjoint {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] [NormedSpace ℝ H] [IsScalarTower ℝ 𝕜 H] (S : StarSubalgebra 𝕜 (H →L[𝕜] H)) : closure (⇑(ContinuousLinearMap.toPointwiseConvergenceCLM 𝕜 (RingHom.id 𝕜) H H) '' (↑S ∩ ↑(selfAdjoint (H →L[𝕜] H)))) = ⇑(ContinuousLinearMap.toPointwiseConvergenceCLM 𝕜 (RingHom.id 𝕜) H H) '' ((↑S).centralizer.centralizer ∩ ↑(selfAdjoint (H →L[𝕜] H)))

The strong operator closure of the self-adjoint part of a unital star subalgebra is the self-adjoint part of its double commutant.

theorem StarSubalgebra.double_commutant_iff_isClosed_image_ofCLM {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (S : StarSubalgebra 𝕜 (H →L[𝕜] H)) : (↑S).centralizer.centralizer = ↑S ↔ IsClosed (ContinuousLinearMapWOT.ofCLM '' ↑S)

The bicommutant theorem: a unital star subalgebra equals its double commutant if and only if it is weak operator closed.

theorem StarSubalgebra.double_commutant_iff_isClosed_image_toPointwiseConvergenceCLM {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (S : StarSubalgebra 𝕜 (H →L[𝕜] H)) : (↑S).centralizer.centralizer = ↑S ↔ IsClosed (⇑(ContinuousLinearMap.toPointwiseConvergenceCLM 𝕜 (RingHom.id 𝕜) H H) '' ↑S)

A unital star subalgebra equals its double commutant if and only if it is strong operator closed.

theorem VonNeumannAlgebra.isClosed_image_ofCLM {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) : IsClosed (ContinuousLinearMapWOT.ofCLM '' ↑M)

A concrete von Neumann algebra is weak operator closed.

theorem VonNeumannAlgebra.isCompact_image_ofCLM_inter_closedBall {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (A : H →L[ℂ] H) (r : ℝ) : IsCompact (ContinuousLinearMapWOT.ofCLM '' (↑M ∩ Metric.closedBall A r))

Every closed norm ball of a concrete von Neumann algebra is weak operator compact; in particular, so is its unit ball.

theorem VonNeumannAlgebra.isClosed_image_toPointwiseConvergenceCLM {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) : IsClosed (⇑(ContinuousLinearMap.toPointwiseConvergenceCLM ℂ (RingHom.id ℂ) H H) '' ↑M)

A concrete von Neumann algebra is strong operator closed.

theorem VonNeumannAlgebra.image_ofCLM_adjoin_eq_closure {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (s : Set (H →L[ℂ] H)) : ContinuousLinearMapWOT.ofCLM '' ↑(adjoin s) = closure (ContinuousLinearMapWOT.ofCLM '' ↑(StarAlgebra.adjoin ℂ s))

The von Neumann algebra generated by s is the weak operator closure of the star algebra generated by s.

theorem VonNeumannAlgebra.image_toPointwiseConvergenceCLM_adjoin_eq_closure {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (s : Set (H →L[ℂ] H)) : ⇑(ContinuousLinearMap.toPointwiseConvergenceCLM ℂ (RingHom.id ℂ) H H) '' ↑(adjoin s) = closure (⇑(ContinuousLinearMap.toPointwiseConvergenceCLM ℂ (RingHom.id ℂ) H H) '' ↑(StarAlgebra.adjoin ℂ s))

The von Neumann algebra generated by s is the strong operator closure of the star algebra generated by s.