MATHLIBANNEX / CANONICAL DECLARATION CARD

The fixed algebra on the CAR trace Hilbert space

MathlibAnnex.CStarAlgebra.CAR.separableCounterexampleRepresentation

def

Defines a representation of the same algebra on the GNS Hilbert space of the CAR trace.

Statement

Let be the completed CAR algebra and the algebra generated by the selected direct sum of pure-state GNS representations indexed by their unitary-equivalence classes and the unitaries from the fixed homogeneity and shell construction. Write for the embedding . Let be the normalized CAR trace, its GNS Hilbert space, and its GNS representation. Let be the chosen state on with , and let be its GNS representation with cyclic vector. The cited trace construction provides a chosen unitary carrying the canonical trace vector to and intertwining the two representations of . Define

Definition

The representation is obtained by conjugating with the same chosen unitary : . Its operators therefore act on , not on .

Assumptions

The algebra and the state extension are fixed as in the cited construction. The same unitary is used throughout. The Hilbert space is determined by and , independently of the added unitaries .

Conclusion

This is a unital -representation . It extends the CAR trace representation in the sense that for all .

Main citations

Lean source signature (exact)

noncomputable def separableCounterexampleRepresentation :
    Representation AtomicCounterexampleAlgebra SeparableCounterexampleHilbertSpace :=
  traceModelRepresentation homogeneityShellFamily

separableCounterexampleRepresentation is the same obtained from traceModelRepresentation at the fixed family. SeparableCounterexampleHilbertSpace is . The names traceGNSUnitary () and tracialRepresentation () occur in the linked defining construction, explaining the conjugation although they are absent from this short signature.

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

Lean realization notes

The space is separable by its dense CAR orbit, and injectivity is a separately cited theorem. Neither fact asserts norm separability of or irreducibility of this representation.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:f0336a753a8f202333b869aaaeb1d7630c9a50e9edb8c7ec3a05b58fb89ab611

Card revision: 2 · SHA-256: 47d4f0b7c34f13bd52725a8e51e896bc85168489e7892a0a473cf0eac009e425

Exposition revision: 3 · SHA-256: edb66b0baf7da1042ae39d445777a8f7278a1b1ad7b92a6aeda274e321cbe5ea

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 923143f02d5200008e5972ad27e35ee32008f03ade1ddec40056350d62fb1aa0

Back to top ↑