OAI/Analysis/KadisonKastler/TracialCommutantSpatialSplit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Spatial splitting with a faithful tracial commutant vector

The weakly compact convex family of bounded implementers has a unique center for the commutant trace metric. Unitary invariance of that metric forces the center into the original algebra. No injectivity is needed.

  1. theorem OAI.KadisonKastler.exists_selfAdjoint_split_of_tracial_commutant line 21