Faithfulness of the representation on the CAR trace Hilbert space

MathlibAnnex.CStarAlgebra.CAR.separableCounterexampleRepresentation_injective

theorem

Proves that the representation is injective.

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 CAR trace and its chosen state extension to . Write for the GNS representation of , and use the chosen unitary from the cited trace construction. For ,

Assumptions

The automorphisms and unitaries defining are those fixed by CAR homogeneity. The cited injectivity theorem for the conjugated GNS representation applies to every such shell family, hence to this one.

Conclusion

Thus is faithful. Together with the separately established separability of , it realizes this same faithfully on a separable Hilbert space.

This statement concerns injectivity of a representation, not faithfulness of a vector state, and does not assert irreducibility.

Proof route

Cancel the fixed unitary conjugation and use faithfulness of the GNS representation of the state extension.

Supporting route explanation

theorem separableCounterexampleRepresentation_injective :
    Function.Injective separableCounterexampleRepresentation

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

Earlier published Card and PDF