OAI/Analysis/KadisonKastler/PublishedStandardRepresentation.lean

Faithful cyclic representations and tensor functoriality

Blackadar, Operator Algebras, III.2.2.29 (p.273), supplies a faithful normal state for a countably decomposable algebra. Its normal GNS representation (III.2.2.1--3, pp.265--266) is faithful, with a cyclic separating unit vector; on a separably acting algebra it is separable (III.2.1.4 and III.2.2.8). This does not claim that the original representation has a cyclic separating vector.

The tensor extension of a normal star isomorphism is the isomorphism case of III.2.2.5 (p.267). Algebraic star isomorphisms between von Neumann algebras are automatically normal (III.2.2.1, III.2.2.12).