Pure-state GNS irreducibility

MathlibAnnex.Analysis.CStarAlgebra.isIrreducible_pureState_gnsStarAlgHom

theorem

Turns purity of a state into irreducibility of its canonical GNS representation.

Statement

Let A be a unital complex C*-algebra and let φ be a pure state of A. The canonical GNS star-algebra homomorphism built from the positive map associated to φ is irreducible.

Assumptions

Let A be a unital complex C*-algebra and let φ be a pure state of A.

Conclusion

The canonical GNS star-algebra homomorphism built from the positive map associated to φ is irreducible.

Proof route

The source invokes the cyclic-vector irreducibility criterion: the GNS cyclic vector has norm one and dense orbit, its vector functional equals φ by the GNS inner-product identity, and purity supplies the criterion's extremality premise.

Main citations

• MathlibAnnex.Analysis.CStarAlgebra.IsPureState

  Exact formal dependency; inspect the linked Card and exact source.

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

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