The CAR source map into the fixed shell-family target

MathlibAnnex.CStarAlgebra.CAR.shellFamilySourceHom

def

Restricting the codomain of the selected atomic representation gives the source map into one fixed generated target.

Statement

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 .

Definition

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.

Assumptions

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.

Conclusion

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.

Supporting route explanation

noncomputable def shellFamilySourceHom (family : RepresentativeShellFamily) :
    Limit →⋆ₐ[ℂ] ShellFamilyTarget family :=
  MathlibAnnex.CStarAlgebra.AtomicConstruction.sourceHom selectedAtomicRepresentation (shellFamilyLinks family)

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

Earlier published Card and PDF