MATHLIBANNEX / CANONICAL DECLARATION CARD

Distinct GNS classes have no unitary intertwiner

MathlibAnnex.CStarAlgebra.PureState.no_unitaryIntertwiner_selectedRepresentation

theorem

The class index makes the selected pure-GNS family pairwise unitarily inequivalent.

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. If , no surjective complex-linear isometry intertwines the two selected representations. Explicitly, for every such , the equations cannot hold for all .

Assumptions

The GNS classes are assumed to be distinct. A candidate is a unitary map between the two complete Hilbert spaces; it need not carry to . The same representative selection based at is used on both sides.

Conclusion

The selected representations form a family with no unitary intertwiners between distinct indices. This supplies precisely the pairwise-inequivalence hypothesis of the generic atomic-shell construction.

Proof route

An intertwining unitary would certify GNS equivalence of the two selected states. Taking their quotient classes would therefore identify and , contradicting their assumed distinctness.

Proof steps

  1. Assume that the candidate unitary satisfies the intertwining equations. The selected representations are exactly the GNS actions of and , so witnesses their GNS equivalence.

  2. The cited representative-class theorem says that GNS-equivalent selected representatives have equal indices: each chosen representative has the class it was chosen from. Applying that theorem gives , contrary to the hypothesis.

Main citations

Lean source signature (exact)

theorem no_unitaryIntertwiner_selectedRepresentation (root : PureState A)
    {i j : GNSClass A} (hij : i ≠ j) (e : SelectedGNS root i ≃ₗᵢ[ℂ] SelectedGNS root j) :
    ¬ StarAlgHom.Intertwines (selectedRepresentation root i)
      (selectedRepresentation root j)
      (e : SelectedGNS root i →L[ℂ] SelectedGNS root j)

Here root is and hij is . The linear isometry equivalence e is the candidate , so it is already surjective. StarAlgHom.Intertwines expresses for every . In the linked proof, representative_injective_on_classes converts that unitary equivalence into equality of the class indices; it is separately cited.

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

Lean realization notes

Two distinct pure states can belong to the same GNS class. The assertion here is about distinct classes. Vanishing of arbitrary bounded intertwiners requires an additional irreducibility argument and is not the conclusion of this declaration.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:178df2065d1b34c05297ba2f0fe9b100f95f502f46c736e02f62f0cef0c8dc7e

Card revision: 1 · SHA-256: 8c78f205e340bea56aec97118cab2578ff73f99177c73f7ce3982828a4d49537

Exposition revision: 1 · SHA-256: 557337b0dc01c1feef1dfba6501ca3f7f27f23f478b276fcf94d407c67d0a078

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 6080d9cf0514564efb41dd0ce48080354b1bd34efade9be5947bc75d4a7fda15

Back to top ↑