The product-vector state on the completed CAR algebra

MathlibAnnex.CStarAlgebra.CAR.rootState

def

Compatible evaluation at the distinguished matrix coordinate extends continuously to the CAR completion.

Statement

Let be the completed CAR algebra: the norm completion of the increasing union of under the unital embeddings (with the fixed coordinate reindexing). Write for the canonical isometric inclusion and for its matrix units. At each stage take , the vector functional of the distinguished coordinate vector. These functionals determine a continuous linear functional satisfying for every and . The definition called the root state is this extension.

Definition

The coordinate estimate bounds each stage functional by . The standard inclusion preserves the zero coordinate, so these maps agree on common representatives in the algebraic direct limit. They therefore define a bounded linear functional on the normed direct limit. Extending that functional to its completion gives ; the extension keeps the stage values unchanged. Positivity passes from the stage functionals to the completion by continuity, and evaluation at the common unit gives normalization.

Assumptions

The stage system and distinguished zero coordinate are fixed as above. The completion uses the CAR norm. No ambient Hilbert-space representation is chosen in this definition.

Conclusion

The defining restriction formula determines uniquely among continuous linear functionals, because the stage union is dense. The cited positivity and normalization results give and , so this functional is a state.

Normalization and positivity are properties proved after the definition. The state evaluates one distinguished coordinate; it is not the normalized trace on a matrix stage. Its definition does not assert that it is faithful.

noncomputable def rootState : Limit →L[ℂ] ℂ :=
  preRootFunctional.extend (UniformSpace.Completion.toComplL : PreCAR →L[ℂ] Limit)

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

Earlier published Card and PDF