Faithfulness of the representation on the CAR trace Hilbert space

MathlibAnnex.CStarAlgebra.CAR.traceModelRepresentation_injective

theorem

Unitary conjugation preserves injectivity of the target-state 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 GNS representation of the chosen state extension , and let be the CAR trace GNS representation. Choose once the pointed unitary with and . Then is injective on .

Assumptions

The family, extension, and chosen unitary are the ones used to define traceModelRepresentation. Faithfulness of is the separately proved kernel-dichotomy result.

Conclusion

The same concrete target admits a faithful representation on the nonzero separable space . Its restriction to is the CAR trace representation.

Injectivity concerns the homomorphism into operators, not a vector functional. The result does not assert irreducibility of this representation or norm separability of . Conjugation uses the inverse on the left because points from the CAR space to the target-state space.

Proof route

Undo the same conjugation and apply faithfulness of the original target-state representation.

Proof steps

Suppose . Since is a unitary onto ,

The theorem tracialRepresentation_injective then gives . In the source this is the composition of the injective conjugation equivalence with the injective representation; it does not require another ideal argument.

Main citations

The stated existence or structural result — MathlibAnnex.CStarAlgebra.CAR.traceModelRepresentation_injective
The fixed concrete target and source map — MathlibAnnex.CStarAlgebra.CAR.shellFamilySourceHom
Faithfulness of the source embedding — MathlibAnnex.CStarAlgebra.CAR.shellFamilySourceHom_injective
Definition and direction of the transport — MathlibAnnex.CStarAlgebra.CAR.traceModelRepresentation
Faithfulness before conjugation — MathlibAnnex.CStarAlgebra.CAR.tracialRepresentation_injective
Separable CAR trace space — MathlibAnnex.CStarAlgebra.CAR.separableSpace_traceHilbertSpace
Source action in the transported model — MathlibAnnex.CStarAlgebra.CAR.traceModelRepresentation_shellFamilySourceHom

Supporting route explanation

Lean source signature (exact)

theorem traceModelRepresentation_injective (family : RepresentativeShellFamily) :
    Function.Injective (traceModelRepresentation family)

In the source	Mathematical meaning
`family : RepresentativeShellFamily`	The fixed family, target , trace extension and the same once-chosen pointed unitary .
`traceModelRepresentation family`	The representation defined by , on the CAR trace GNS space .
`Function.Injective (...)`	If as operators on , then in . This is injectivity of the same conjugated action; it does not assert irreducibility or state faithfulness.
Further source notes: The proof uses `(traceGNSUnitary family).symm.conjStarAlgEquiv.injective` and `tracialRepresentation_injective family`. These refer to the exact same and as the definition, not newly selected existence witnesses.

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

Accepted content SHA-256: d4481026b41ec003d55bc2394a2f19bc8eed5d75574b5d6214dbb0d708d075ce

Accepted source guide SHA-256: cc55a5a287db8070a1baad172199034f51921d0b7b746b093d8bd8f4dbe54fe2

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73