MATHLIBANNEX / CANONICAL DECLARATION CARD

Faithfulness of the representation on the CAR trace Hilbert space

MathlibAnnex.CStarAlgebra.CAR.traceModelRepresentation_injective

theorem

Unitary conjugation preserves injectivity of the target-state representation.

Statement

Let be the completed CAR algebra and its normalized trace. Fix a representative shell family and its chosen unitary links in the selected atomic representation . Write for the resulting concrete target and , , for its faithful unital source map. This fixes one target and one source map throughout. Let be the GNS representation of the chosen state extension , and let be the CAR trace GNS representation. Choose once the pointed unitary with and . Then is injective on .

Assumptions

The family, extension, and chosen unitary are the ones used to define traceModelRepresentation. Faithfulness of is the separately proved kernel-dichotomy result.

Conclusion

The same concrete target admits a faithful representation on the nonzero separable space . Its restriction to is the CAR trace representation.

Proof route

Undo the same conjugation and apply faithfulness of the original target-state representation.

Proof steps

  1. Suppose . Since is a unitary onto ,

    The theorem tracialRepresentation_injective then gives . In the source this is the composition of the injective conjugation equivalence with the injective representation; it does not require another ideal argument.

Main citations

Lean source signature (exact)

theorem traceModelRepresentation_injective (family : RepresentativeShellFamily) :
    Function.Injective (traceModelRepresentation family)

traceModelRepresentation family is on TraceHilbertSpace. The proof uses (traceGNSUnitary family).symm.conjStarAlgEquiv.injective and tracialRepresentation_injective family. These refer to the exact same and as the definition, not newly selected existence witnesses.

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

Lean realization notes

Injectivity concerns the homomorphism into operators, not a vector functional. The result does not assert irreducibility of this representation or norm separability of . Conjugation uses the inverse on the left because points from the CAR space to the target-state space.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:258daaeaf0a6caefd2a19aba5c4244ab2dd8f7cc41e99be671bfe548cc8bf77e

Card revision: 1 · SHA-256: d604a2745ef32d61d8f9b60d3479ff7289bed7fccdc662ee899b3feace46bafd

Exposition revision: 1 · SHA-256: 462078ea562693ed5553e7331061073cfbafd297f1330ceb6ae70b08c1a6b407

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 7483c4398beb7120be237424d6d5e363f30c3a4a69a5e784753b754fbb70609a

Back to top ↑