Comparing the strong and weak operator topologies

The identity from the pointwise-convergence copy of continuous linear maps to the weak operator copy is continuous. Centralizers of sets of operators are weak-operator closed. These facts allow strong approximation results to identify weak operator closures without changing the norm topology on the original operator space.

The two topologies have the same continuous linear functionals: every functional continuous for pointwise convergence is a finite sum T ↦ ∑ x ∈ s, g x (T x) of continuous functionals of values (PointwiseConvergenceCLM.exists_finset_sum_eq, in TauCeti.Analysis.LocallyConvex.PointwiseConvergence), hence weak-operator continuous, and conversely (ContinuousLinearMapWOT.exists_finset_sum_eq). On a Hilbert space, writing each g x as an inner product gives the usual finite sums of matrix coefficients. By locally convex separation, a convex set of operators therefore has the same closure in both topologies (Convex.toPointwiseConvergenceCLM_mem_closure_image_iff).

References

Kadison–Ringrose, Fundamentals of the Theory of Operator Algebras I, Theorem 5.1.2 and Corollary 5.1.3.

theorem ContinuousLinearMapWOT.continuous_ofPointwiseConvergenceCLM {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module 𝕜₂ F] [ContinuousConstSMul 𝕜₂ F] : Continuous fun (T : E →SLₚₜ[σ] F) => ofCLM T

Pointwise (strong operator) convergence is stronger than weak operator convergence.

theorem Set.isClosed_image_ofCLM_centralizer {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [Module 𝕜 E] [ContinuousConstSMul 𝕜 E] [SeparatingDual 𝕜 E] (s : Set (E →L[𝕜] E)) : IsClosed (ContinuousLinearMapWOT.ofCLM '' s.centralizer)

The commutant of any set of operators is closed in the weak operator topology.

theorem ContinuousLinearMapWOT.continuous_strongDual_apply_toPointwiseConvergenceCLM {𝕜₁ : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [NormedField 𝕜₁] [RCLike 𝕜] {σ : 𝕜₁ →+* 𝕜} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [ContinuousSMul 𝕜₁ E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (φ : StrongDual 𝕜 (E →SLₚₜ[σ] F)) : Continuous fun (A : E →SWOT[σ] F) => φ ((ContinuousLinearMap.toPointwiseConvergenceCLM 𝕜 σ E F) A.toCLM)

A linear functional on operators which is continuous for the topology of pointwise convergence is continuous for the weak operator topology.

theorem ContinuousLinearMapWOT.exists_finset_sum_eq {𝕜₁ : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [NormedField 𝕜₁] [RCLike 𝕜] {σ : 𝕜₁ →+* 𝕜} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [ContinuousSMul 𝕜₁ E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (φ : StrongDual 𝕜 (E →SWOT[σ] F)) : ∃ (s : Finset E) (g : E → StrongDual 𝕜 F), ∀ (A : E →SWOT[σ] F), φ A = ∑ x ∈ s, (g x) (A x)

Continuous functionals in the weak operator topology. A linear functional on operators which is continuous for the weak operator topology is a finite sum of functionals A ↦ g x (A x).

theorem Convex.toPointwiseConvergenceCLM_mem_closure_image_iff {𝕜₁ : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [NormedField 𝕜₁] [RCLike 𝕜] {σ : 𝕜₁ →+* 𝕜} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [ContinuousSMul 𝕜₁ E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [IsScalarTower ℝ 𝕜 F] {s : Set (E →SL[σ] F)} (hs : Convex ℝ s) {T : E →SL[σ] F} : (ContinuousLinearMap.toPointwiseConvergenceCLM 𝕜 σ E F) T ∈ closure (⇑(ContinuousLinearMap.toPointwiseConvergenceCLM 𝕜 σ E F) '' s) ↔ ContinuousLinearMapWOT.ofCLM T ∈ closure (ContinuousLinearMapWOT.ofCLM '' s)

For a convex set of operators, the closures in the topology of pointwise convergence (the strong operator topology) and in the weak operator topology contain the same operators.