A faithful separable model, but no separable irreducible model

MathlibAnnex.CStarAlgebra.CAR.atomicCounterexampleEndpoint_and_exists_separable_faithful_representation_and_no_separable_irreducible_representation

theorem

Combines the ordinary counterexample and the separable-representation conclusions for one fixed algebra.

Statement

The fixed unital C*-algebra A is simple and infinite-dimensional, has exactly one nonzero irreducible representation class and is not an algebra of compact operators. The same A has a faithful representation on the nonzero separable CAR trace-GNS space Hτ, but has no nonzero irreducible representation on any separable complex 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. Let Hτ = L²(C, τC) be the GNS Hilbert space of the normalized CAR trace τC. There are no additional theorem hypotheses. In particular, neither CH nor separable representability is assumed.

Conclusion

The ordinary counterexample assertion holds for A. In addition, Hτ is nontrivial and separable, there exists an injective unital *-representation A → B(Hτ), and every possibly nonunital *-representation A → B(K) on any separable complex Hilbert space K fails to be nonzero irreducible.

Proof route

Combine the ordinary counterexample theorem, nontriviality and separability of the CAR trace-GNS space, the faithful tracial representation, and the universal exclusion of separable irreducible representations.

Main citations

• MathlibAnnex.CStarAlgebra.CAR.separableCounterexampleRepresentation_injective

  Exact source attribution.

• MathlibAnnex.CStarAlgebra.CAR.not_isIrreducible_of_separable

  Exact source attribution.

Lean source declaration (exact)

/-- The same fixed algebra has a faithful representation on a nontrivial separable
Hilbert space, but has no nonzero irreducible representation on any separable
Hilbert space in the arbitrary comparison universe. This does not assert that
the algebra is nonprimitive: the original irreducible model is retained. -/
theorem atomicCounterexampleEndpoint_and_exists_separable_faithful_representation_and_no_separable_irreducible_representation :
    AtomicCounterexampleEndpoint.{v} ∧
    Nontrivial SeparableCounterexampleHilbertSpace ∧
    TopologicalSpace.SeparableSpace SeparableCounterexampleHilbertSpace ∧
    (∃ ρ : Representation AtomicCounterexampleAlgebra SeparableCounterexampleHilbertSpace,
      Function.Injective ρ) ∧
    (∀ (H : Type v) [NormedAddCommGroup H] [InnerProductSpace ℂ H]
        [CompleteSpace H] [TopologicalSpace.SeparableSpace H],
      ∀ ρ : NonUnitalRepresentation (A := AtomicCounterexampleAlgebra) (H := H),
        ¬ ρ.IsIrreducible) := by
  refine ⟨shellFamilyEndpoint homogeneityShellFamily, nontrivial_traceHilbertSpace,
    separableSpace_separableCounterexampleHilbertSpace,
    ⟨separableCounterexampleRepresentation,
      separableCounterexampleRepresentation_injective⟩, ?_⟩
  intro H _ _ _ _ ρ
  exact not_isIrreducible_of_separable ρ

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

Lean realization notes

The final existential witness and the universal comparison representations refer to the same A. The comparison Hilbert universe is independent. The conclusion excludes separable irreducible realizations, not all irreducible realizations; it does not assert that A is nonprimitive. The theorem has no tracial uniqueness clause: that is included separately in the counterexample theorem with its faithful separable tracial model.