MATHLIBANNEX / CANONICAL DECLARATION CARD

A pure state detects a nonzero square

MathlibAnnex.Analysis.CStarAlgebra.exists_pureState_nonzero_on_star_mul_self

theorem

Detects a nonzero element through its positive square without an algebra separability assumption.

Statement

Let be a nonzero unital complex -algebra, and let be nonzero. There is a pure state on such that Here a state is a continuous complex-linear functional positive on positive elements and satisfying ; pure means extreme in the real convex state space.

Assumptions

No separability assumption is made on . The element detected in the conclusion is , rather than an assertion about .

Conclusion

One functional is simultaneously a state, pure, and nonzero on .

Proof route

Choose a nonzero spectral value of the positive square, realize it as a character value on its generated commutative algebra, and extend that character to a pure state.

Proof steps

  1. Put . The -identity gives , so . It is self-adjoint. Its spectral radius equals , and compactness of its spectrum supplies with .

  2. Let , the norm-closed unital -subalgebra generated by . Since is self-adjoint, is commutative. The character-space identification with gives a character of with . These are the two applications in Spectral radius and the generated-algebra character map: self-adjointness supplies the norm-radius equality, and the chosen spectral point is an input to the surjective character map.

  3. Apply Pure-state extension of a character to this closed commutative unital and this character . It produces a state on which is pure and satisfies for every . Substituting the same gives

    The first two outputs of the extension theorem give the remaining state and purity conditions.

Main citations

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
In the source Mathematical meaning
[Nontrivial A] The algebra is nonzero: . This condition does not say whether a unit is assumed; that information comes from the surrounding -algebra structure.
{a : A} (ha : a ≠ 0) The specified nonzero element .
∃ phi : A →L[ℂ] ℂ One continuous complex-linear functional is chosen.
phi ∈ stateSpace A That functional is positive and normalized by .
IsPureState A phi The same state is an extreme point for real convex combinations of states.
phi (star a * a) ≠ 0 Its value on the particular positive element is nonzero; this is the full final condition, not a claim about .

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.exists_pureState_nonzero_on_star_mul_self

Accepted content SHA-256: 260ae870e3ef4f02167ba7dda12d85a4cfc986bb89f1bb8b0e483235fe4dd56f

Accepted source guide SHA-256: 22fbf06fc6696fefddc92c700ed396d8773bf8d19852b115ccac2a0f89443f13

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑