MATHLIBANNEX / CANONICAL DECLARATION CARD

A Naimark counterexample of continuum norm density

MathlibAnnex.CStarAlgebra.CAR.existsNaimarkCounterexampleOfDensity_continuum

theorem

Gives a C*-algebra of norm density whose nonzero irreducible representations form one unitary-equivalence class, without an identification with the compact operators.

Statement

There exist a nonzero complex C*-algebra , not required to be unital, a complex Hilbert space , and a nonzero irreducible -representation with the following properties. Every nonzero irreducible -representation of is unitarily equivalent to . The representation is not both injective and surjective onto , the full algebra of compact operators on . Finally, Here density refers to the norm topology. None of the representations is required in advance to preserve an identity.

Assumptions

This is an existence theorem with no CH hypothesis. Its statement allows nonunital C*-algebras and places no requirement on the existence of a faithful representation on a separable Hilbert space.

Conclusion

One may take , where is CAR, is the selected GNS direct sum, and are the unitaries from the fixed homogeneity and shell construction. Take and , the inclusion of this concrete algebra in . Thus the constructed example is unital, even though unitality is not required by the existence statement.

Proof route

Use the constructed algebra and its inclusion representation . The classification theorem gives the single unitary-equivalence class, the compact-operator exclusion applies to , and the density theorem gives the required value .

Proof steps

  1. Take the algebra , its selected GNS direct sum , and the inclusion . The representation-classification theorem says that is nonzero irreducible and that, for any nonzero irreducible -representation , a unitary satisfies . This statement does not require as an initial assumption.

  2. The compact-operator exclusion rules out every injective representation of onto the full algebra of compact operators, in particular the specified inclusion . The density theorem gives . These are precisely the other conditions of the existential predicate in the Lean statement.

Main citations

Lean source signature (exact)

theorem existsNaimarkCounterexampleOfDensity_continuum :
    ExistsNaimarkCounterexampleOfDensity (Cardinal.continuum : Cardinal.{0})

(Cardinal.continuum : Cardinal.{0}) denotes the continuum , explicitly typed as a cardinal of types in Type 0 (also written Type). The colon is a type annotation, and .{0} specifies a universe level: it is not the cardinal number zero and imposes no countability assumption. The cardinal universe convention explains this type. The separately linked ExistsNaimarkCounterexampleOfDensity quantifies over the algebra, Hilbert space and representations in that universe. In the linked proof, AtomicCounterexampleAlgebra is , SelectedAtomicHilbert completedRootPureState is , and .toNonUnitalStarAlgHom retains the same inclusion while forgetting the requirement to preserve the identity. inferInstance supplies the existing C*-algebra, Hilbert-space and spectral-order structures; these are not extra hypotheses of the theorem.

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

Lean realization notes

The fixed example also admits a faithful representation on a separable Hilbert space, but that is not a condition in this existence statement and is not asserted for every C*-algebra satisfying it.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:9e4fa34878df2ba18cbc8247c4d9da4877ccd5abd32747c76de2e936615fa461

Card revision: 2 · SHA-256: 228ba19d3e6f019d7447205532137a8eabdb20491d59bbae4fa507ce55cb654f

Exposition revision: 3 · SHA-256: f9aed14a1af813b49cd2d48d81057a30890a81ebf2926060f799249cafc0e381

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 2f65c53190eadf8d11dd45715899c993fe42cbe4de2f33a47222e65facbd9f5a

Back to top ↑