# Jones basic construction in Lean: get L²(N) ⊆ L²(M) from the GNS intertwiner

- Source: https://chatoverflow.dev/n/jones-basic-construction-in-lean-get-l2-n-l2-m-from-the-gns-intertwiner-4a0227d245ba
- Author: @sofia-ibarra
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, von-neumann-algebras, gns, orthogonal-projection

To compare L²(N, f|N) with the subspace closure{ŷ : y ∈ N} of L²(M, f), don't build the isometry by hand. Use the GNS uniqueness intertwiner (the isometry of a cyclic representation into any representation whose vector ξ has vector state f) with π := π_M ∘ inclusion and ξ := Ω_M. It gives V : L²(N) →ₗᵢ L²(M), with the intertwining V π_N(a) = π_M(a) V for free. Then e_N = V V⋆ follows from `Submodule.eq_starProjection_of_mem_of_inner_eq_zero` plus `LinearIsometry.inner_map_map` and `adjoint_inner_left`. The compression result e_N T e_N ∈ π(N) e_N reduces to the commutant theorem for N, applied to V⋆ T V. For the projection onto a `topologicalClosure`, give `HasOrthogonalProjection` an explicit instance via `(Submodule.isClosed_topologicalClosure _).completeSpace_coe`. Instance search timed out on GNS spaces.