A fixed counterexample to Naimark’s problem

MathlibAnnex.CStarAlgebra.CAR.atomicCounterexampleEndpoint

theorem

Proves the ordinary counterexample properties for the source-defined algebra, with no additional homogeneity premise.

Statement

The fixed CAR-based algebra A is a nontrivial unital simple infinite-dimensional C*-algebra. Its atomic inclusion is a faithful nonzero irreducible representation, every nonzero irreducible representation is unitarily equivalent to that inclusion, and A has no model as the algebra of all compact operators on a Hilbert space.

Assumptions

Let A ⊆ B(Hₐₜ) be the fixed unital C*-algebra obtained by adjoining the chosen shell-link unitaries to the atomic representation of the CAR algebra C, and then taking the norm-closed unital *-algebra they generate. The map j: C → A and the atomic inclusion πₐₜ are the fixed maps from this construction. There are no additional theorem hypotheses. The comparison Hilbert spaces are arbitrary and need not be separable.

Conclusion

A is nontrivial and norm closed in B(Hₐₜ). The CAR source map j: C → A is injective and satisfies j(1) = 1. A is infinite-dimensional over ℂ. The inclusion πₐₜ: A → B(Hₐₜ) is faithful, nonzero, and irreducible. For every complex Hilbert space K and every nonzero irreducible *-representation σ: A → B(K), not initially required to preserve the unit, there is a surjective complex-linear isometry U: Hₐₜ → K with U(πₐₜ(a)x) = σ(a)(Ux) for all a ∈ A and x ∈ Hₐₜ. Every norm-closed two-sided ideal of A is either {0} or A. For every complex Hilbert space K, there is no injective complex-linear *-homomorphism e: A → B(K), not required to preserve the unit, whose image consists of compact operators and contains every compact operator on K.

Proof route

Apply the proved shell-family theorem to the one family selected by CAR homogeneity. This is a specialization of already established conclusions, not an assumption of those conclusions.

Main citations

• MathlibAnnex.CStarAlgebra.CAR.shellFamilyEndpoint

  Exact source attribution.

Lean source declaration (exact)

/-- Closed ordinary Naimark main for the actual CAR construction.  It has no
generic KOS, shell-data, rank-one, capture, simplicity, or compactness premise. -/
theorem atomicCounterexampleEndpoint : AtomicCounterexampleEndpoint.{v} :=
  shellFamilyEndpoint homogeneityShellFamily

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

Lean realization notes

The exact proof is shellFamilyEndpoint homogeneityShellFamily. The comparison universe v is independent of the fixed carrier universe. Nonunital comparison maps are included. The result does not say that all irreducible representations are absent: πₐₜ is one. Later declarations add separable and tracial conclusions.