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.

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.

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

Supporting route explanation

Lean source signature (exact)

theorem existsNaimarkCounterexampleOfDensity_continuum :
    ExistsNaimarkCounterexampleOfDensity (Cardinal.continuum : Cardinal.{0})
In the source Mathematical meaning
(Cardinal.continuum : Cardinal.{0}) The cardinal in the universe of Type 0 types. The colon specifies a type and .{0} specifies a universe level, not cardinal zero or countability.
ExistsNaimarkCounterexampleOfDensity The linked exact existential predicate chooses one nonzero possibly nonunital complex C*-algebra , its spectral order, one complete complex Hilbert space , and one star representation in the indicated universe. Source letters A, H, pi in that definition denote here.
NonUnitalCStarRepresentation.IsSingletonIrreducibleModel pi That same is nonzero irreducible, and every nonzero irreducible possibly nonunital on any complete complex Hilbert space in the comparison universe is unitarily equivalent to . This means a surjective complex-linear isometry satisfies for every .
¬ IsCompactOperatorModel pi The same does not simultaneously have all three properties: injectivity, compactness of every , and coverage of every compact operator on . It is the full compact-operator model that is excluded, not a single compact image.
HasDensityCharacter A κ The same has a norm-dense subset of cardinality , and every norm-dense subset has cardinality at least . This is exact norm density of the existential algebra; no faithful separable model is imposed.

Further source notes: 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.

Separate complete definition of the existential result predicate, from the fixed source, lines 56–72. Its letters A, H, pi denote the same explained in the table; this is not a continuation of the theorem signature.

def ExistsNaimarkCounterexampleOfDensity (κ : Cardinal.{u}) : Prop :=
  ∃ (A : Type u) (iA : NonUnitalCStarAlgebra A),
    letI := iA
    ∃ (oA : PartialOrder A),
      letI := oA
      ∃ (sA : StarOrderedRing A) (nA : Nontrivial A),
        letI := sA
        letI := nA
        ∃ (H : Type u) (nH : NormedAddCommGroup H),
          letI := nH
          ∃ (iH : InnerProductSpace ℂ H),
            letI := iH
            ∃ (cH : CompleteSpace H),
              letI := cH
              ∃ pi : NonUnitalCStarRepresentation A H,
                NonUnitalCStarRepresentation.IsSingletonIrreducibleModel.{u, u, u} pi ∧
                (¬ IsCompactOperatorModel pi) ∧ HasDensityCharacter A κ

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

Earlier published Card and PDF

Exact content identity

Declaration: MathlibAnnex.CStarAlgebra.CAR.existsNaimarkCounterexampleOfDensity_continuum

Accepted content SHA-256: ac159c66a014ea67c887a6885485419b0ef5c4f9f437c1a8759e3fe21ef9d3fb

Accepted source guide SHA-256: db51c328deb14579b22abd0b9e9333a5fd31f62f353baa5e546103c12fd3979b

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑