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.

Main citations

Lean source signature (exact)

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

Here root is , j is a GNS equivalence class, representative root j is , and SelectedGNS root j is . The RHS positiveFunctional.gnsStarAlgHom is . The vector is named selectedVector root j in its separate cited definition; the normalization, vector-functional identity and irreducibility are separate cited theorems, not extra fields of this definition.

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

Lean realization notes

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.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:ad01be2e337dc8b82ab777026820a387f45a7b982625ae89324c84e796897a26

Card revision: 1 · SHA-256: dc502af1f12012931543b84153b5333bda1d2d5ab24463cec516f75c4482f1ee

Exposition revision: 1 · SHA-256: af9004dce076d51049a2e04d5af836787c064af87a8d49609c96985a418fbc9c

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 00fdec4eeaae55b967c9b4eb57d8e7b5d9807fcf7965ba20f902009f90337bcf