Pure state detecting a nonzero square

MathlibAnnex.Analysis.CStarAlgebra.exists_pureState_nonzero_on_star_mul_self

theorem

Supplies a pure state that detects a* a, enabling faithfulness arguments without separability of the algebra.

Statement

Let A be a nonzero unital complex C*-algebra and let a ∈ A be nonzero. No separability assumption on A is required. Some pure state φ in stateSpace A satisfies φ(a* a)≠0.

Assumptions

Let A be a nonzero unital complex C*-algebra and let a ∈ A be nonzero. No separability assumption on A is required.

Conclusion

Some pure state φ in stateSpace A satisfies φ(a* a)≠0.

Proof route

The source sets b=a* a, uses its nonzero spectral radius to obtain a nonzero character value on the closed elemental commutative star subalgebra generated by b, extends that character to a pure state, and transfers the nonzero value back to b.

Main citations

• MathlibAnnex.Analysis.CStarAlgebra.exists_pureState_extension

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

Lean source signature (exact)

theorem exists_pureState_nonzero_on_star_mul_self [Nontrivial A]
    {a : A} (ha : a ≠ 0) :
    ∃ phi : A →L[ℂ] ℂ,
      phi ∈ stateSpace A ∧ IsPureState A phi ∧ phi (star a * a) ≠ 0

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