Physicslib4.AQFT.HaagKastler.StrongDensity

The von Neumann density theorem for a unital *-representation

The bridge between physical observables and the local von Neumann algebras R(B) = π(𝔘(B))'' of Physicslib4/AQFT/HaagKastler/LocalVonNeumann.lean rests on the fact that a bicommutant, though generally strictly larger than the image it is formed from, is its strong closure: no measurement of finite precision can distinguish an element of the bicommutant from a quasilocal observable close to it.

The strong operator topology is Mathlib's topology of pointwise convergence, PointwiseConvergenceCLM (notation H →Lₚₜ[ℂ] H), and the commutant is Set.centralizer, as in LocalVonNeumann.lean. What Mathlib does not have is the density theorem itself (nor its Kaplansky strengthening); it is proved in Physicslib4/Operators/DensityTheorem.lean together with this file.

Main statements

• Physicslib4.AQFT.HaagKastler.dense_range_in_bicommutant

theorem Physicslib4.AQFT.HaagKastler.hasBasis_nhds_ofFun {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (T : H →L[ℂ] H) : (nhds ((UniformConvergenceCLM.ofFun (RingHom.id ℂ) H {s : Set H | s.Finite}) T)).HasBasis (fun (sε : Set H × ℝ) => sε.1.Finite ∧ 0 < sε.2) fun (sε : Set H × ℝ) => {S : UniformConvergenceCLM (RingHom.id ℂ) H {s : Set H | s.Finite} | ∀ x ∈ sε.1, ‖S x - T x‖ < sε.2}

Basic strong neighbourhoods of an operator. In the strong operator topology (pointwise convergence on finite sets), the neighbourhoods of T have as a basis the sets of S with ‖S x - T x‖ < ε for all x in a finite set.

Blueprint reference: lmm:strong-neighbourhood-basis.

theorem Physicslib4.AQFT.HaagKastler.dense_range_in_bicommutant {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {𝔄 : Type u_2} [Ring 𝔄] [StarRing 𝔄] [Algebra ℂ 𝔄] (π : 𝔄 →⋆ₐ[ℂ] H →L[ℂ] H) : ⇑(UniformConvergenceCLM.ofFun (RingHom.id ℂ) H {s : Set H | s.Finite}) '' (Set.range ⇑π).centralizer.centralizer ⊆ closure (⇑(UniformConvergenceCLM.ofFun (RingHom.id ℂ) H {s : Set H | s.Finite}) '' Set.range ⇑π)

The von Neumann density theorem, in the form the observable bridge needs: the image of a unital *-representation π of the quasilocal algebra 𝔘 on H is dense, in the strong operator topology, in its bicommutant π(𝔘)''.

Unitality is the hypothesis that does the work — for the zero representation on a nonzero H the image {0} is already strongly closed while the bicommutant is ℂ · 1 — and it is carried here by StarAlgHom, whose map_one field is exactly π 1 = 1.

The statement is phrased through the equivalence UniformConvergenceCLM.ofFun, which re-topologizes H →L[ℂ] H as H →Lₚₜ[ℂ] H; both sets of operators are transported along it so that the closure is taken in the strong topology.

This is Murphy's Lemma 4.1.4. It is not available in Mathlib: Mathlib has the double commutant property of a bundled von Neumann algebra (VonNeumannAlgebra.commutant_commutant), which is not a density result, and norm-topology closures of star subalgebras (StarSubalgebra.topologicalClosure), which is the wrong topology. It is proved here from the finitely-many-vectors approximation exists_forall_norm_sub_lt_of_mem_bicommutant of Physicslib4/Operators/DensityTheorem.lean and the basic strong neighbourhoods hasBasis_nhds_ofFun.

The self-adjoint strengthening — that every self-adjoint element of the bicommutant is a strong limit of self-adjoint elements of the image — is the Kaplansky density theorem and is deliberately not claimed: nothing in the bridge argument needs it.

Blueprint reference: thrm:quasilocal-strongly-dense.