OAI/Analysis/KadisonKastler/FaithfulCoisometryBicentralizers.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

All faithful vector states under the constructed modular coisometries

Positive state representation keeps the same modular conjugation. Thus the fixed-conjugation coisometry argument applies at every faithful vector state, without assuming state homogeneity.

  1. theorem OAI.KadisonKastler.faithful_bicentralizers_scalar_of_modular_coisometries line 25