MATHLIBANNEX / CANONICAL DECLARATION CARD

A simple C*-algebra with a unique irreducible representation class

MathlibAnnex.CStarAlgebra.CAR.atomicCounterexampleEndpoint

theorem

Establishes the properties that make the fixed algebra a counterexample to Naimark's problem.

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 inclusion representation. Then is a nonzero, norm-closed, infinite-dimensional unital C*-algebra, is injective and unital, and is faithful and nonzero irreducible. Every nonzero irreducible -representation on a complex Hilbert space is unitarily equivalent to , even if is not assumed: there is a unitary with The algebra is simple: every norm-closed two-sided ideal is or . Moreover, for no complex Hilbert space is there an injective -representation with .

Assumptions

The automorphisms and shell unitaries are obtained from CAR homogeneity and fixed once. No simplicity or uniqueness-of-representation assumption is supplied to the theorem. The Hilbert space in the representation and compact-operator assertions is arbitrary; separability and preservation of the identity by the given representation are not assumed.

Conclusion

Thus has exactly one unitary-equivalence class of nonzero irreducible -representations, but is not isomorphic to the full algebra of compact operators on any Hilbert space. The nonzero, norm-closed algebra , its injective unital embedding and its faithful irreducible inclusion are the same throughout these assertions.

Proof route

Apply the cited theorem for a fixed shell family to the family supplied by CAR homogeneity. The construction and the representation-classification theorem give the embedding and unitary equivalences; their cited consequences give simplicity and the exclusion of an algebra of compact operators.

Proof steps

  1. Let denote the class of the distinguished pure state, let be the decreasing root projections, and write for their shells. At choose and . In each other class, CAR homogeneity supplies one automorphism , and exact shell matching supplies all for that same . These choices are made once for the entire construction.

  2. The shell construction supplies an injective unital embedding and an irreducible inclusion . Since embeds the infinite-dimensional algebra , the algebra is infinite dimensional. Its norm closure is part of its construction, and its nonzeroness follows from injectivity of .

  3. The representation-classification theorem for this fixed family gives unitary equivalence with for every unital nonzero irreducible representation. The cited unitality lemma gives for every nonzero irreducible -representation of , so the same conclusion applies without initially assuming that preserves the identity.

  4. The cited simplicity theorem applies because is faithful and all nonzero irreducible representations are unitarily equivalent to it. The cited compact-operator exclusion applies because is unital and infinite dimensional. The Lean theorem collects these proved properties for the same algebra.

Main citations

Lean source signature (exact)

theorem atomicCounterexampleEndpoint : AtomicCounterexampleEndpoint.{v}

AtomicCounterexampleEndpoint abbreviates ShellFamilyEndpoint homogeneityShellFamily; the separate abbreviation and the full structure are linked. Its ten fields are the properties expanded above. In those fields, atomicCounterexampleRepresentation is , atomicCounterexampleSourceHom is , and captures_nonunital is the unitary-equivalence assertion for an arbitrary nonzero irreducible representation, without an initial unit-preservation assumption. not_compactOperatorModel rules out an injective representation whose range is all of . These names occur in the linked structure and proof, not as extra arguments in this short signature.

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

Lean realization notes

In the displayed inclusion representation, one also has . This follows from the stated properties: the intersection is a closed two-sided ideal of ; if it were nonzero, simplicity would give . Then would be compact, so , and hence , would be finite dimensional, a contradiction. This is a consequence of the theorem, not an extra field of its Lean statement.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

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

Card revision: 2 · SHA-256: d10f0a91f19a1e8ff87ebdfcdb4948f6e061fdea3cf835a3652348f1e8084674

Exposition revision: 3 · SHA-256: f161a599b091c62218ee716a708cbc5306b024b90354aedfad6344dc8c94adb3

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 23cae9bdc54bf0854a6d4bc70c3d091c8e781f7338e7ef4fe98f65df83c7a5d9

Back to top ↑