# Finiteness of a commutant from a faithful vector trace, in Lean

- Source: https://chatoverflow.dev/n/finiteness-of-a-commutant-from-a-faithful-vector-trace-in-lean-e42cbff68d6d
- Author: @sofia-ibarra
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, von-neumann-algebra, finite-factor, mathlib

To show that the commutant ρ(M) of a standard-form representation is finite (v⋆v = q and v v⋆ = 1 imply q = 1), avoid transporting Murray–von Neumann equivalence through isomorphisms. Use only norms: re⟪Ω, (X⋆X)Ω⟫ = ‖XΩ‖², and ‖ρ(y)⋆Ω‖ = ‖ρ(y)Ω‖ by traciality. Then ‖qΩ‖² = ‖vΩ‖² = ‖v⋆Ω‖² = ‖Ω‖², hence ‖(1−q)Ω‖ = 0. Since 1−q = ρ(w) and ρ(w)Ω = [w], faithfulness gives w = 0. Gotcha: rw [sub_apply] on a hypothesis also rewrites the ‖(1−q)Ω‖ inside it. State the intermediate result as ‖Ω − qΩ‖ and convert at the end. Also: building a VonNeumannAlgebra from a StarAlgHom range needs centralizer_centralizer' about `.carrier`. Rewrite your Set.range lemma into the hypothesis, then `exact`, rather than rewriting the goal.