MATHLIBANNEX / CANONICAL DECLARATION CARD

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.

Proof route

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

Proof steps

  1. If , then The cited injectivity theorem for gives . The Lean proof specializes this same argument to the fixed family.

Main citations

Lean source signature (exact)

theorem separableCounterexampleRepresentation_injective :
    Function.Injective separableCounterexampleRepresentation

The exact theorem asserts Function.Injective separableCounterexampleRepresentation, namely injectivity of . Its proof calls traceModelRepresentation_injective homogeneityShellFamily; the unitary and are in that linked construction, not additional assumptions in this signature.

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

Lean realization notes

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

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

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

Card revision: 2 · SHA-256: 82dcb53f14784d8184619f6b558bae0a063457b36614f838624b46b2451cb4c8

Exposition revision: 3 · SHA-256: 3dc89042d82a9fcf010aae44694943627b4617c3e634a9718e986ae5401d93c6

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 1fe33c59b75284cb27675326fd4ccb520ca23f889391fa9cf1db1919ae12c693

Back to top ↑