The ambient inclusion of the fixed shell-family target

MathlibAnnex.CStarAlgebra.CAR.shellFamilyInclusion

def

The same concrete target has a literal representation on the selected atomic Hilbert space.

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 ambient inclusion is , . With the source map , , it satisfies .

Definition

The generic ambient-inclusion construction takes a concrete generated star algebra to its inclusion in the existing operator algebra. Using the atomic CAR action and the fixed links gives exactly . Since is the same operator regarded as an element of , composing with this inclusion recovers for every ; no new operator is constructed by the composition.

Assumptions

The representative shell family is the only input beyond the fixed CAR construction. Both and its ambient Hilbert space have already been determined by that family and its once-chosen links . The target is a concrete norm-closed unital star subalgebra of .

Conclusion

The definition supplies the displayed unital representation of this same on this same . Its injectivity is the injectivity of literal inclusion. The separately cited irreducibility theorem uses the construction of the chosen shell unitaries to show that this representation has no proper nonzero closed reducing subspace.

The inclusion and source map have different domains: acts on and on . Irreducibility and universal capture are separate results, not fields of this definition. This construction does not identify arbitrary target representations or change the choice of .

Supporting route explanation

noncomputable def shellFamilyInclusion (family : RepresentativeShellFamily) :
    Representation (ShellFamilyTarget family)
      (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState) :=
  MathlibAnnex.CStarAlgebra.AtomicConstruction.ambientInclusion selectedAtomicRepresentation
    (shellFamilyLinks family)

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

Earlier published Card and PDF