MATHLIBANNEX / CANONICAL DECLARATION CARD

The GNS representation of the target trace extension

MathlibAnnex.CStarAlgebra.CAR.tracialRepresentation

def

The chosen state on the existing target supplies its cyclic GNS representation.

Statement

Let be the completed CAR algebra and its normalized trace. Fix a representative shell family and its chosen unitary links in the selected atomic representation . Write for the resulting concrete target and , , for its faithful unital source map. This fixes one target and one source map throughout. Let be the chosen state extension of to . Define to be its GNS representation.

Definition

Choose from exists_state_extension_trace and regard that same functional as a positive linear map. Form the GNS completion of modulo its null vectors, set to that Hilbert space, and let . The induced left action is

The right-hand side of the definition is exactly the GNS star homomorphism of traceExtensionPositive family. This positive-map bundle has the same values as ; it is not another state. Normalization gives , so and is nonzero. The GNS construction gives the dense -orbit. Its restriction realizes because . The actual-representation source-cyclicity theorem applies to these two facts and proves the source orbit dense; it is not an assumption smuggled into the definition.

Assumptions

A representative shell family is fixed first. The chosen extension is positive and normalized; its traciality is not needed to perform the GNS construction.

Conclusion

With its canonical unit vector , this representation realizes and has dense target orbit. The separately proved source-cyclicity result also gives

Consequently is separable, since is separable and the displayed orbit map is continuous.

Separability here is a conclusion about the Hilbert space. The algebra is not assumed norm separable. Injectivity of is a separate theorem; irreducibility or purity of is not asserted.

Main citations

Supporting route explanation

Lean source signature (exact)

noncomputable def tracialRepresentation (family : RepresentativeShellFamily) :
    Representation (ShellFamilyTarget family) (TracialHilbertSpace family) :=
  (traceExtensionPositive family).gnsStarAlgHom
In the source Mathematical meaning
family : RepresentativeShellFamily; ShellFamilyTarget family The supplied CAR shell family fixes the same target and source .
traceExtensionPositive family The positive-linear-map bundle of the chosen state extension of the CAR trace. Its values are exactly ; it is not a second state.
TracialHilbertSpace family The complete GNS Hilbert space obtained by completing modulo the null vectors of , with canonical unit vector .
Representation (ShellFamilyTarget family) (TracialHilbertSpace family) The output is a unital star representation .
(traceExtensionPositive family).gnsStarAlgHom The full RHS is the GNS left action . Its vector-functional identity, unit-vector norm, density, source cyclicity and separability are separately proved properties of this action, not fields omitted from the definition. Irreducibility is not asserted.

Further source notes: The norm, vector-functional, density and separability statements are separately cited theorems, not omitted fields of this definition.

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

Accepted content SHA-256: 608e2baffcb6f361677647944fc9d4669b6c768cc3a00f237c75e86491d9ffd0

Accepted source guide SHA-256: 98e514d3c6652e2c852aa4b414b7c043552622512e266fe5a930290449f9d235

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑