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 .

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.

Main citations

Supporting route explanation

Lean source signature (exact)

noncomputable def separableCounterexampleRepresentation :
    Representation AtomicCounterexampleAlgebra SeparableCounterexampleHilbertSpace :=
  traceModelRepresentation homogeneityShellFamily
In the source Mathematical meaning
AtomicCounterexampleAlgebra The unchanged concrete target of the fixed CAR homogeneity shell construction, with source embedding .
SeparableCounterexampleHilbertSpace The CAR trace GNS space , determined by CAR and its normalized trace, not the atomic sum .
Representation AtomicCounterexampleAlgebra SeparableCounterexampleHilbertSpace The output is a unital star representation of this same target.
traceModelRepresentation homogeneityShellFamily The full RHS specializes the trace-model action to the same fixed family. With its chosen , it is . The source restriction is ; injectivity and separability are separately cited facts, and irreducibility is not asserted.

Further source notes: 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 · Back to Project

Earlier published Card and PDF

Exact content identity

Declaration: MathlibAnnex.CStarAlgebra.CAR.separableCounterexampleRepresentation

Accepted content SHA-256: 24b674e4099ac9c3aba5693224e6dd70d64d3c8811246e466066ee384e78ba24

Accepted source guide SHA-256: 3f9ca3baeef2b3027e1cce09c1a53b3e2af6044881cf45ef3f6f5272ed718ae4

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑