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.

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.

Main citations

Definition and its exact construction — MathlibAnnex.CStarAlgebra.CAR.atomicCounterexampleRepresentation
The inclusion before specialization — MathlibAnnex.CStarAlgebra.CAR.shellFamilyInclusion
The CAR embedding into the same generated algebra — MathlibAnnex.CStarAlgebra.CAR.atomicCounterexampleSourceHom
Faithfulness of the inclusion — MathlibAnnex.CStarAlgebra.CAR.shellFamilyInclusion_injective
Irreducibility of the inclusion — MathlibAnnex.CStarAlgebra.CAR.isIrreducible_shellFamilyInclusion

Supporting route explanation

Lean source signature (exact)

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

In the source	Mathematical meaning
`AtomicCounterexampleAlgebra`	The one fixed algebra supplied by the CAR homogeneity shell construction.
`SelectedAtomicHilbert completedRootPureState`	The selected atomic Hilbert sum based at the bundled root pure state . It is not assumed separable.
`Representation AtomicCounterexampleAlgebra (...)`	The output is the unital star representation .
`shellFamilyInclusion homogeneityShellFamily`	The complete RHS is the literal inclusion for the same fixed family: . It is distinct from the later trace-model action on . Faithfulness and irreducibility are separate theorems, not data chosen here.
Further source notes: `SelectedAtomicHilbert completedRootPureState` is ; `completedRootPureState` is bundled with its purity proof. The map is explained through the separately cited source-map declaration.

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.atomicCounterexampleRepresentation

Accepted content SHA-256: e3afaf04cc08e85ac394ecbf13dd409b7a55543224dc769f0e8a5d20c4548b0b

Accepted source guide SHA-256: dcee1d5b2df53f811ca47b8374102e814f95ea0fc3002417b733b2766363585b

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73