A Naimark counterexample of norm density continuum

MathlibAnnex.CStarAlgebra.CAR.existsNaimarkCounterexampleOfDensity_continuum

theorem

Supplies an unconditional witness to the general density-existence statement.

Statement

There exists a nontrivial complex C*-algebra D of exact norm density 𝔠 = 2^ℵ₀ with a nonzero irreducible representation π such that every nonzero irreducible representation of D is unitarily equivalent to π and π is not a model of the entire compact-operator algebra.

Assumptions

No CH assumption is made. The existence predicate permits nonunital C*-algebras and nonunital complex *-representations. In this closed statement, the algebra carrier, displayed Hilbert space, and comparison Hilbert spaces lie in Type (universe zero).

Conclusion

The density-existence predicate holds at 𝔠. A witness is the fixed unital CAR-based algebra A with its atomic inclusion; its density is exactly 𝔠.

Proof route

Insert the fixed A and atomic representation into the general possibly nonunital existence predicate.

Main citations

• MathlibAnnex.CStarAlgebra.CAR.hasDensityCharacter_atomicCounterexampleAlgebra

  Exact source attribution.

• MathlibAnnex.Analysis.CStarAlgebra.Representation.IsSingletonIrreducibleModelAmongNonUnital.isSingletonIrreducibleModel_toNonUnitalStarAlgHom

  Exact source attribution.

Lean source declaration (exact)

/-- The fixed construction supplies an ordinary counterexample of exact
norm density continuum. This existence assertion has no CH premise. -/
theorem existsNaimarkCounterexampleOfDensity_continuum :
    ExistsNaimarkCounterexampleOfDensity (Cardinal.continuum : Cardinal.{0}) := by
  refine ⟨AtomicCounterexampleAlgebra, inferInstance, inferInstance, inferInstance,
    inferInstance,
    MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState,
    inferInstance, inferInstance, inferInstance,
    (shellFamilyInclusion homogeneityShellFamily).toNonUnitalStarAlgHom, ?_, ?_,
    hasDensityCharacter_atomicCounterexampleAlgebra⟩
  · exact
      Representation.IsSingletonIrreducibleModelAmongNonUnital.isSingletonIrreducibleModel_toNonUnitalStarAlgHom
        (isUniqueIrreducibleModelAmongNonUnital_shellFamilyInclusion.{0}
          homogeneityShellFamily).2
  · exact not_isCompactOperatorModel_shellFamilyTarget homogeneityShellFamily _

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

Lean realization notes

The displayed predicate explicitly negates IsCompactOperatorModel of the displayed π. In ordinary C*-algebraic language this yields a counterexample; it is not a silently added quantified condition in the Lean definition. The predicate has no faithful-separable-representation requirement. Its witness here is nonetheless the same fixed A. This closed existence theorem is not being promoted to an all-universe statement.