The selected GNS representation of a pure-state class

MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation

def

A choice of representative pure states, fixed literally at a root, gives one concrete GNS representation per equivalence class.

Statement

Let be a unital complex C*-algebra, with the positive order used for its states, and fix a pure state . A pure state is an extreme point of the normalized positive continuous linear functionals. Let be the set of pure-state GNS representations modulo unitary equivalence. For each , choose a pure state in that class, retaining literally at . Write for its GNS space, representation and canonical cyclic vector. The selected representation is the GNS action associated to this particular . The choice concerns the representative state; the construction then uses its actual GNS Hilbert space and action.

Definition

Take the chosen state , regard it as a positive linear functional, and form its GNS completion . Left multiplication induces the bounded action on that completion. The selected vector is the GNS cyclic vector. Its orbit is dense. The vector-functional identity and purity of , together with this cyclicity and normalization, supply the separate irreducibility theorem.

Assumptions

The class and the root pure state are given. GNS representations here are unital complex-linear star homomorphisms on complete complex Hilbert spaces. No separability or faithfulness of is assumed.

Conclusion

The definition specifies on . The separate selected-vector and pure-GNS results give , , and irreducibility of . These properties explain why this selected family supplies the summands of the direct-sum representation.

The inner product is conjugate linear in its first argument. Irreducibility means that the only closed reducing subspaces are and ; this Hilbert space is nonzero because it contains the unit vector . The definition does not itself prove those properties, and it does not claim that different pure states always have inequivalent GNS representations.

Supporting route explanation

noncomputable def selectedRepresentation (root : PureState A) (j : GNSClass A) :
    MathlibAnnex.Analysis.CStarAlgebra.Representation A (SelectedGNS root j) :=
  (representative root j).positiveFunctional.gnsStarAlgHom

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project

Earlier published Card and PDF