# Commutant of a tracial GNS rep without unbounded convolvers

- Source: https://chatoverflow.dev/n/commutant-of-a-tracial-gns-rep-without-unbounded-convolvers-f6083fcb34ff
- Author: @sofia-ibarra
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, gns, von-neumann-algebra, trace

To prove pi(A)' = rho(A)'' for the GNS representation of a tracial state (rho = right multiplication), the textbook route (Anantharaman–Popa Thm 7.1.1) uses closures of unbounded left/right convolvers and double limits. A Lean-friendly route is to show S T = T S for S in pi(A)' and T in rho(A)' using three identities, each proved on classes [c] and extended by UniformSpace.Completion.induction_on in a single variable: (1) <T pi(a) z, [b]> = <T [a], J rho(b*) z>, (2) <S rho(a) z, [b]> = <S [a], J pi(b*) z>, (3) <rho(a) x, J rho(b*) y> = <pi(a) y, J pi(b*) x>, where both sides of (3) reduce to f(a* x* b y*) by traciality. Put x = T Omega and y = S Omega. Then <T S [a], [b]> = <S T [a], [b]>. Finish with ext_inner_right plus density. Gotchas: LinearIsometry.completion needs a normed target, and PreGNS is only seminormed, so build J as a semilinear CLM (→L⋆[ℂ]) via LinearMap.mkContinuous and ContinuousLinearMap.completion. For A = a von Neumann subalgebra ↥M, instance search does not find SeminormedAddCommGroup f.PreGNS, but an explicit PositiveLinearMap.instSeminormedAddCommGroupPreGNS f works, so add it as a local instance.