MATHLIBANNEX / CANONICAL DECLARATION CARD

The GNS representation of a pure state is irreducible

MathlibAnnex.Analysis.CStarAlgebra.isIrreducible_pureState_gnsStarAlgHom

theorem

Applies the cyclic pure-state criterion to the space and vector constructed from the same state.

Statement

Let be a unital complex -algebra, and let be a pure state: a positive normalized continuous complex-linear functional extreme in the real state space. Let be its GNS representation. Then the only closed reducing subspaces of for are and .

Assumptions

The representation and space in the conclusion are the canonical GNS construction from , not an independently chosen representation on an arbitrary Hilbert space. No separability hypothesis is present.

Conclusion

The canonical GNS star-algebra homomorphism is irreducible. Its norm-one cyclic vector also ensures that its Hilbert space is nonzero.

Proof route

Verify the norm, cyclicity and pure vector-functional hypotheses of the cyclic irreducibility criterion.

Proof steps

  1. The GNS construction for the positive functional underlying supplies

    Normalization gives the first equation; cyclicity of the construction gives the second.

  2. For every , the GNS inner-product identity is

    Hence the entire vector functional of equals the same pure state , rather than merely agreeing at the unit.

  3. Apply Cyclic pure vector states force irreducibility with and . Step 1 verifies the norm-one and dense-orbit inputs; Step 2 transports the given purity to its vector-functional input. The output is exactly irreducibility of .

  4. To see the mechanism of the criterion, let be a closed reducing subspace, and let be its orthogonal projection. Then and for every . Define the positive functional

    Orthogonality of and , and invariance of both, give

    Hence for every positive . Apply A positive functional dominated by a pure state to the given pure and this : there is such that .

  5. For arbitrary , self-adjointness and idempotence of , followed by its commutation with the representation, yield

    Here the inner product is linear in its second argument. For fixed , density of the vectors makes . Density in and continuity now give on all of .

  6. Finally implies . The norm-one vector is nonzero, so and . Thus or , and its range is respectively or , as required.

Main citations

Lean source signature (exact)

theorem isIrreducible_pureState_gnsStarAlgHom
    (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) (hpure : IsPureState A phi) :
    StarAlgHom.IsIrreducible
      (positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom
In the source Mathematical meaning
(phi : A →L[ℂ] ℂ) The given continuous complex-linear functional on the unital ordered -algebra .
(hphi : phi ∈ stateSpace A) is positive and ; this permits its positive-map and GNS construction.
(hpure : IsPureState A phi) The same is an extreme point of the real state space.
positiveLinearMapOfMemStateSpace phi hphi The same functional, now carrying the positivity supplied by its state hypothesis.
(positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom The canonical representation on the GNS space of that functional.
StarAlgHom.IsIrreducible For that represented action, every closed reducing complex subspace is either zero or the entire GNS space.

Exact source and proof.

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.Analysis.CStarAlgebra.isIrreducible_pureState_gnsStarAlgHom

Accepted content SHA-256: a06c2fefa7ef3ba2809a91d4191be765fce148e7cfb0384d0d2ff0e3dfb01184

Accepted source guide SHA-256: 14c3741bb3641fc6585c7e3dbc8271befe699a74b5c18c7bfd822ee9ee2e24af

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑