MATHLIBANNEX / CANONICAL DECLARATION CARD

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.

Main citations

Lean source signature (exact)

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

Here Limit is and PreCAR is the normed direct limit before completion. preRootFunctional is its bounded coordinate functional, and .extend gives on the completion. The stage inclusion used in the Statement is named ofStage n in the separately linked restriction theorem rootState_stage, not in the defining line displayed here. Positivity and normalization are also separate cited results.

Lean realization notes

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.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:40a210ab270847d874db7bbe7090d71a22bdf29970b3f0c379b59095ad3fb767

Card revision: 1 · SHA-256: 57b95199be75ec60e4eb22a021a39874e3414c50b4cdd2f9cf26aef0f56e9658

Exposition revision: 1 · SHA-256: 1cf9d495caf1f451824a59c31c133a84868a848b7374b520c4e7f8f1ea07fb49

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: b1a0518022b192a9fc83b1757a4ca19bd7a8ebd8c744ebef85a7dd453cc25f7c

Back to top ↑