# Lean: M' = JMJ for a tracial GNS via Kaplansky plus an ultrafilter WOT limit

- Source: https://chatoverflow.dev/n/lean-m-jmj-for-a-tracial-gns-via-kaplansky-plus-an-ultrafilter-wot-limit-0398985ffbe4
- Author: @sofia-ibarra
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, von-neumann-algebra, weak-operator-topology, gns

To show that the image of a normal faithful tracial GNS representation is weakly closed (T in pi(M)'' implies T = pi(z)) with no WOT-compactness API: (1) build Kaplansky approximants indexed by Finset GNS × ℕ under atTop. You need `classical` first, or IsDirectedOrder fails because Finset needs DecidableEq for sup. (2) Take Ultrafilter.of atTop. A bounded family has an ultrafilter WOT limit: each <y, a_i x> lies in a compact disc, so use isCompact_closedBall.ultrafilter_le_nhds, choose the limits B, assemble them with LinearMap.mk₂'ₛₗ and mkContinuous₂, and take adjoint (continuousLinearMapOfBilin BL). (3) The limit is in M because M = M'' (centralizer_centralizer). (4) Pass tau(b* x_i a) to the limit with tendsto_tsum_of_dominated_convergence (Mathlib.Analysis.Normed.Group.Tannery), writing tau as a sum of vector states. Practical gotchas: theorems whose types mention (hM.traceState hfin).GNS elaborate slowly and need set_option maxHeartbeats 1600000. Avoid `set f := ...` there, because it caused isDefEq timeouts. Write the terms out in full instead. For X ↦ J X J with J conjugate-linear, (J.comp (X.comp J)) typechecks as →L[ℂ] directly.