MATHLIBANNEX / CANONICAL DECLARATION CARD

The ambient representation of the fixed algebra

MathlibAnnex.CStarAlgebra.CAR.atomicCounterexampleRepresentation

def

Defines the inclusion representation .

Statement

Let be the completed CAR algebra and the algebra generated by the selected direct sum of pure-state GNS representations indexed by their unitary-equivalence classes and the unitaries from the fixed homogeneity and shell construction. Write for the embedding . The inclusion representation is

Definition

The map is the literal inclusion: as a bounded operator on . The source map is regarded as an element of , so .

Assumptions

The GNS direct sum, the unitaries and the generated algebra are fixed as above. Each is already a bounded operator on .

Conclusion

is a unital -representation and . Its definition introduces no new choice of Hilbert space or operators.

Main citations

Lean source signature (exact)

noncomputable def atomicCounterexampleRepresentation :
    Representation AtomicCounterexampleAlgebra
      (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState) :=
  shellFamilyInclusion homogeneityShellFamily

atomicCounterexampleRepresentation is . SelectedAtomicHilbert completedRootPureState is ; completedRootPureState is bundled with its purity proof. The right-hand side specializes shellFamilyInclusion to the same family. The map is explained through the separately cited source-map declaration.

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

Lean realization notes

Faithfulness and irreducibility of this particular inclusion are separate theorems cited below. They are not additional data chosen in the definition; no separability of is assumed.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

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

Card revision: 2 · SHA-256: 516a57a8f062ef0a6234d796e52b96c61eb3b141eb155771b24f65817dddb0ea

Exposition revision: 3 · SHA-256: cef5d882030e1a2f04b20a8daa51af0a5c0030a977e83892fd660334d8f908ea

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: e3e25bb6b0f59876779367210ebb8d97ed989713896d700c24200a34c5b185f5

Back to top ↑