Pure-state extension of a character

MathlibAnnex.Analysis.CStarAlgebra.exists_pureState_extension

theorem

Extends a character of a closed unital star subalgebra to a pure state of the ambient algebra.

Statement

Let A be a nonzero unital complex C*-algebra, D a closed unital star subalgebra of A, and χ a character of D. There is a continuous complex-linear functional φ on A in stateSpace A that is pure and restricts to χ: for every d in D, φ(d)=χ(d).

Assumptions

Let A be a nonzero unital complex C*-algebra, D a closed unital star subalgebra of A, and χ a character of D.

Conclusion

There is a continuous complex-linear functional φ on A in stateSpace A that is pure and restricts to χ: for every d in D, φ(d)=χ(d).

Proof route

The source obtains an extreme point of the compact weak state-extension face. It maps that weak functional to the strong dual, preserves its restriction to D, and transports extremality to show purity. Closedness of D is used by the extension-face construction.

Main citations

• MathlibAnnex.Analysis.CStarAlgebra.IsPureState

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

Lean source signature (exact)

theorem exists_pureState_extension (D : StarSubalgebra ℂ A) [IsClosed (D : Set A)]
    (chi : WeakDual.characterSpace ℂ D) :
    ∃ phi : A →L[ℂ] ℂ,
      phi ∈ stateSpace A ∧ IsPureState A phi ∧ ∀ d : D, phi d = chi d

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