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.

Main citations

Lean source signature (exact)

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

TraceHilbertSpace, traceVector, and traceRepresentation are . TracialHilbertSpace family is the different space . traceGNSUnitary family maps from to ; its .symm.conjStarAlgEquiv therefore sends an operator on to on . The complete RHS includes composition with tracialRepresentation family.

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

Lean realization notes

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.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

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

Card revision: 1 · SHA-256: 8a9fbbd1a0305f221e617a417ec288d2563b88c6bb308562369f956067b88ccb

Exposition revision: 1 · SHA-256: 7def775971ef9e1b7577a09e0923b4e8abdf7544c283c1e409fb707725196fa3

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: ab07f8caf89b3e2a6decfd742272c415341eaf45550bfa8fef3ad47077cae2f3