The target represented on the CAR trace GNS space

MathlibAnnex.CStarAlgebra.CAR.traceModelRepresentation

def

A fixed pointed unitary transports the target action onto the Hilbert space constructed from CAR alone.

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 GNS representation of the CAR trace, and let be the target-state GNS representation for the chosen extension . Fix the pointed unitary described below. Define the target representation on by

Definition

Set , , and . The GNS identities give and . Thus , and its dense continuous CAR orbit makes it separable. The target GNS has the same source vector functional and a dense source orbit. Pointed cyclic transport therefore gives, and traceGNSUnitary chooses once,

Conjugate the whole target action by its inverse. Then and

The dense orbit is contained in the target orbit, proving target cyclicity. The defining RHS below uses the inverse of this same chosen .

Assumptions

The representative shell family and chosen state extension are fixed. Both GNS representations restrict to the same source trace, and both source orbits are dense; source cyclicity in is a proved result.

Conclusion

The new representation has and realizes at . Its target orbit is dense. The space is nonzero and separable and is defined from CAR alone, independently of the family; the target action still depends on the fixed family.

The direction determines the conjugation . This is one chosen pointed unitary, used throughout the definition and its consequences. Injectivity of this representation is stated separately. The target itself has not been replaced.

Supporting route explanation

noncomputable def traceModelRepresentation (family : RepresentativeShellFamily) :
    Representation (ShellFamilyTarget family) TraceHilbertSpace :=
  (traceGNSUnitary family).symm.conjStarAlgEquiv.toStarAlgHom.comp
    (tracialRepresentation family)

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

Earlier published Card and PDF