MATHLIBANNEX / CANONICAL DECLARATION CARD

The atomic direct sum of the selected CAR representations

MathlibAnnex.CStarAlgebra.CAR.selectedAtomicRepresentation

def

All selected pure-GNS fibers of the completed CAR algebra act together on one Hilbert direct sum.

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 . The selected atomic representation is this coordinatewise unital representation .

Definition

The common estimate bounds every coordinate action uniformly in . Hence the coordinatewise formula defines a bounded operator on the square-summable families, with . Multiplication, the unit and complex linearity hold coordinatewise. The inner product on the direct sum shows that taking adjoints also holds coordinatewise, giving . The existing arbitrary-index atomic construction packages these properties.

Assumptions

The completed CAR algebra and its root pure state are fixed. Every fiber is the complete GNS Hilbert space of the chosen state. The index set need not be countable, and the Hilbert direct sum is not assumed separable.

Conclusion

For every , and , the defining formula is . In particular, for . Thus the selected individual actions are the coordinate restrictions of one displayed representation.

The symbol denotes one fiber action and denotes their direct sum. The cited faithfulness theorem is a separate property of this CAR representation, obtained from its faithful root summand; faithfulness is not a new input or a field added to this definition.

Main citations

Supporting route explanation

Lean source signature (exact)

noncomputable def selectedAtomicRepresentation :
    Representation Limit
      (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState) :=
  atomicRepresentation
    (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState)
In the source Mathematical meaning
Limit; completedRootPureState The completed CAR algebra and its root state , bundled with the proved purity property.
PureState.selectedRepresentation completedRootPureState The family of GNS actions of one selected representative pure state in every GNS class , based at .
PureState.SelectedAtomicHilbert completedRootPureState The Hilbert direct sum of square-summable families . The index set is arbitrary, not required to be countable.
atomicRepresentation (...) The entire RHS assembles the given family into the coordinatewise action , a unital complex-linear star representation .
selectedAtomicRepresentation This is the direct-sum representation , distinct from an individual . Individual irreducibility does not claim irreducibility of this direct sum; its faithfulness is a separate theorem.

Further source notes: Here Limit is and completedRootPureState is bundled with its purity proof. Coordinate inclusions are the separately defined selectedEmbedding; they are used to state the coordinate restriction formula.

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

Earlier published Card and PDF

Exact content identity

Declaration: MathlibAnnex.CStarAlgebra.CAR.selectedAtomicRepresentation

Accepted content SHA-256: 31d69adcb21f8c0d67d242772866f455d6e39cfe57d7947cd0b2f4a41b67bba8

Accepted source guide SHA-256: 9d255e6f5ab0b8a82903766867c6d72498e219ae2d57756bf7a15ee564337e5f

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑