Purity of the completed root state

MathlibAnnex.CStarAlgebra.CAR.isPureState_rootState

theorem

Passes extremality of the root vector states from every finite matrix stage to the completed CAR algebra.

Statement

Let be the completed CAR algebra with stage embeddings . Let be the continuous linear functional characterized by for every stage matrix . Then is a pure state: it is an extreme point of the convex set of continuous positive unital complex-linear functionals on .

Assumptions

The embeddings come from . The index is the distinguished first coordinate in each stage. The coordinate functionals are compatible and bounded by the matrix norm, so they extend to the specified functional on the completion. Positivity and are established before the purity argument. Convex combinations use real coefficients.

Conclusion

If and are states on , , and , then . Thus completion has not introduced a nontrivial convex decomposition of this state.

The purity asserted here is extremality in the state space. The proof uses the pure finite-stage restrictions and density; it makes no assertion that all states on are pure.

Proof route

Restrict a proposed convex decomposition of to each finite matrix stage. The restriction of a state is again a state, because is unital and preserves positivity. The root coordinate state is pure on each matrix algebra, so both restricted states equal it. The two continuous functionals therefore agree with on the dense union of stages, and hence on all of .

theorem isPureState_rootState : MathlibAnnex.CStarAlgebra.IsPureState Limit rootState

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project

Earlier published Card and PDF