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.

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.

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

Supporting route explanation

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)
In the source Mathematical meaning
root : PureState A; i j : GNSClass A Fix the root pure state of and two indices in the set of pure-GNS unitary-equivalence classes. Each has selected data or .
hij : i ≠ j The GNS classes are distinct, a stronger condition than merely unequal state functionals.
e : SelectedGNS root i ≃ₗᵢ[ℂ] SelectedGNS root j A candidate surjective complex-linear isometry , already a unitary between these Hilbert spaces.
(e : SelectedGNS root i →L[ℂ] SelectedGNS root j) The same unitary read as a bounded complex-linear map, without changing its direction or values.
¬ StarAlgHom.Intertwines (selectedRepresentation root i) (selectedRepresentation root j) ... The equations cannot hold for every and . No condition is imposed. The theorem excludes unitary intertwiners, not all bounded maps.

Further source notes: 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 · Back to Project

Earlier published Card and PDF

Exact content identity

Declaration: MathlibAnnex.CStarAlgebra.PureState.no_unitaryIntertwiner_selectedRepresentation

Accepted content SHA-256: d05909d87e1bf86548852e6e5126f3e546c42bbbb21dac861bb8bbfebd012a23

Accepted source guide SHA-256: ddb408f27abc434f4a84e440e167ab826e8bd98d4a32bbb591497bb1836cd8b0

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑