MathlibAnnex.CStarAlgebra.CAR.rootState
Compatible evaluation at the distinguished matrix coordinate extends continuously to the CAR completion.
Statement
Let
Definition
The coordinate estimate
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
Main citations
- Definition and its exact construction · Exact source
- Stage coordinate functional · Exact source
- Compatibility of the coordinate functional · Exact source
- Bounded functional before completion · Exact source
- Stage restriction of the extended functional · Exact source
- Normalization of the root state · Exact source
- Positivity of the root state · Exact source
- Uniqueness from the dense stage restrictions · Exact source
Lean source signature (exact)
noncomputable def rootState : Limit →L[ℂ] ℂ := preRootFunctional.extend (UniformSpace.Completion.toComplL : PreCAR →L[ℂ] Limit)
Here Limit is PreCAR is the normed direct limit before completion. preRootFunctional is its bounded coordinate functional, and .extend gives 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.
Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF
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