MATHLIBANNEX / CANONICAL DECLARATION CARD

Faithfulness of the target-state GNS representation

MathlibAnnex.CStarAlgebra.CAR.tracialRepresentation_injective

theorem

The ideal dichotomy of the same target forces the constructed nonzero representation to be injective.

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. Choose the state extension of supplied by state extension along . Its GNS representation is , with

The inner product is linear in its second argument. The -orbit of is dense by the GNS construction. The representation is injective.

Assumptions

The representative shell family is fixed. The established closed two-sided ideal dichotomy of this same is available as a theorem. The GNS space is nonzero because its canonical vector has norm .

Conclusion

If , then . Thus the GNS representation of the chosen state on is faithful as an algebra representation.

Proof route

Apply the closed-ideal dichotomy to the kernel and exclude the whole-algebra case using the unit on the nonzero GNS space.

Proof steps

  1. The kernel is a norm-closed two-sided ideal. The previously established result shellFamilyTarget_closedIdeal_dichotomy gives or .

  2. If , then . But is unital, so

    contradicting . Hence , which is precisely injectivity. The source applies Representation.injective_of_closed_ideal_dichotomy after installing the separately proved nontriviality of .

Main citations

Lean source signature (exact)

theorem tracialRepresentation_injective (family : RepresentativeShellFamily) :
    Function.Injective (tracialRepresentation family)

Function.Injective (tracialRepresentation family) concerns the map from to bounded operators on . In the linked proof, nontrivial_tracialHilbertSpace supplies a nonzero codomain, and shellFamilyTarget_closedIdeal_dichotomy is passed to the generic faithful-representation lemma. Neither is a new assumption added to the displayed signature.

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

Lean realization notes

This does not infer faithfulness of an arbitrary vector state from faithfulness of its representation. State faithfulness requires its own argument. No irreducibility of , purity of , or separability of is assumed.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:4584f92dc8d9b60095a3711eeec03fed2358049e92cda4b562ca383ff56817c3

Card revision: 1 · SHA-256: 083694f92a81054269d1db41236e51316cbd3d901c399e192b23a742ca2ef266

Exposition revision: 1 · SHA-256: 5b192ccbb19e7e6073ddf15a64483af45d140b2f508b20849f1d6b11f420d154

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: bb2397e2041d52060aaa9a0ed63de94c61e877ae3edb367ee3b12846fa504723

Back to top ↑