MATHLIBANNEX / CANONICAL DECLARATION CARD

A separably represented C*-algebra with no separable irreducible representation

MathlibAnnex.CStarAlgebra.CAR.atomicCounterexampleEndpoint_and_exists_separable_faithful_representation_and_no_separable_irreducible_representation

theorem

The same algebra has a faithful representation on a separable Hilbert space, but no nonzero irreducible representation on any separable Hilbert space.

Statement

Let be the completed CAR algebra. Let be the direct sum of one chosen GNS representation from each pure-state GNS equivalence class, and let be the unitaries obtained from the fixed CAR homogeneity and shell construction. Put , and write for the embedding into . Let be the normalized trace of . The algebra retains all the properties in the cited representation-classification theorem: it is nonzero, norm closed, unital, infinite dimensional and simple; is injective and unital; the inclusion is faithful and irreducible; every nonzero irreducible -representation of is unitarily equivalent to ; and is not isomorphic to the full algebra of compact operators on any Hilbert space. In addition, is nonzero and separable, and there exists a faithful unital representation . No separable complex Hilbert space carries a nonzero irreducible -representation of , even without assuming preservation of the identity.

Assumptions

All assertions concern the same generated algebra and the same fixed shell unitaries. The absence of irreducible representations is quantified over arbitrary separable complex Hilbert spaces. Norm separability of is neither required nor asserted.

Conclusion

has both the faithful representation on the separable space and the faithful irreducible representation on . The representation is reducible, whereas cannot be separable.

Proof route

Combine the classification and simplicity results for with the normalized CAR trace vector, the dense CAR orbit, faithfulness of , and the theorem excluding nonzero irreducible representations on separable Hilbert spaces.

Proof steps

  1. Let be the GNS representation and cyclic vector of . One has , so . The continuous map has dense range. Since is separable, is separable.

  2. Take the GNS representation of the chosen extension of to , and the unitary from the cited trace construction. Then is the established faithful representation on . The cited theorem excluding nonzero irreducible representations on separable Hilbert spaces applies to every -representation with separable. These statements are conjoined with the classification and structural properties of the same .

Main citations

Lean source signature (exact)

theorem atomicCounterexampleEndpoint_and_exists_separable_faithful_representation_and_no_separable_irreducible_representation :
    AtomicCounterexampleEndpoint.{v} ∧
    Nontrivial SeparableCounterexampleHilbertSpace ∧
    TopologicalSpace.SeparableSpace SeparableCounterexampleHilbertSpace ∧
    (∃ ρ : Representation AtomicCounterexampleAlgebra SeparableCounterexampleHilbertSpace,
      Function.Injective ρ) ∧
    (∀ (H : Type v) [NormedAddCommGroup H] [InnerProductSpace ℂ H]
        [CompleteSpace H] [TopologicalSpace.SeparableSpace H],
      ∀ ρ : NonUnitalRepresentation (A := AtomicCounterexampleAlgebra) (H := H),
        ¬ ρ.IsIrreducible)

The long conjunction in the exact signature keeps AtomicCounterexampleEndpoint, Nontrivial and SeparableSpace of , an existential injective representation, and the universal exclusion statement separate. SeparableCounterexampleHilbertSpace is and NonUnitalRepresentation does not initially require . The proof chooses separableCounterexampleRepresentation, the same .

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

Lean realization notes

The faithful representation in the existential assertion is the already chosen . No different algebra or unrelated representation is chosen to establish the two separability assertions.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:496fb09fae36f8b07e1641152da97643e6c1b595cfc8bf458629debfabf9c241

Card revision: 2 · SHA-256: 676839944ea44aba2ad0d82eecf10f9d7de497d78bdc437392982049cd4644ee

Exposition revision: 3 · SHA-256: 9f7c84764bbb25b92b7c4902e233aa74a31f37794608360c1a4c9f1be8bc4418

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: d3c63a89bb452a85d6d2d6cd29822144644d64057b2c8d5ffa306c19504ce7f9

Back to top ↑