MATHLIBANNEX / CANONICAL DECLARATION CARD

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.

Main citations

Lean source signature (exact)

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

Here family fixes the shell data, shellFamilyLinks family is , and ShellFamilyTarget family is . completedRootPureState is the CAR root state bundled with its purity proof, so SelectedAtomicHilbert completedRootPureState is . The RHS AtomicConstruction.ambientInclusion is . The separately defined shellFamilySourceHom family is ; the underlying-operator formula gives . The cited irreducibility theorem is separate from this defining RHS.

Lean realization notes

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 .

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

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

Card revision: 1 · SHA-256: 608748718c9b2fa8d4a3f8b34ab899dc76f70c13f6b41b13231b5aa918686622

Exposition revision: 1 · SHA-256: dcb3559cfc538c702d2b99364db637cf2e502471606b7a64efecd50aae28b11e

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: a61bce75172a10087824d5bebaffac33cdcf1c3284cf7494435313367660be91

Back to top ↑