The CAR source map into the fixed shell-family target

Let be the completed CAR algebra, the norm completion of the unital matrix system with embeddings . Let be its distinguished pure product-vector state. Index pure-state GNS equivalence classes by , choose one representative in each class with at , and denote its GNS data by . Write for the Hilbert direct sum, for coordinate inclusion, and . Here the sum consists of square-summable families and has no countability restriction on . Fix a representative shell family: for each class it gives an automorphism with and shell links satisfying and . Here is the image of the distinguished matrix projection in , and . At , the family specifies and . Choose once the family of unitary operators supplied for this shell family by the completed CAR atomic-shell realization theorem, and fix . The source map is the unital star homomorphism defined by , viewed as an element of .

The generic map into a concrete generated target sends an algebra element to its represented operator, now with codomain that target. Apply this construction to the selected CAR atomic action and the already chosen links . The source and target units agree because is a unital star subalgebra of . No new completion, quotient, or choice of representation is performed by this map.

The given representative shell family, its selected link family , and the resulting target are fixed throughout. The containment follows from the definition of the generated algebra, so the codomain restriction is defined on every . No target representation or target Hilbert space is an additional input to this definition.

If is literal inclusion, then . In particular . The separate source-injectivity theorem shows that this particular is faithful; it uses the faithful direct-sum representation of CAR, rather than any simplicity assumption on .

The choice of is made once in the cited shell-family-links definition. The maps and use that same choice and the same , not unrelated witnesses of existence statements. The defining RHS is a codomain restriction; injectivity is a separately proved property.