The separable trace-GNS space is infinite-dimensional

MathlibAnnex.CStarAlgebra.CAR.not_finiteDimensional_separableCounterexampleHilbertSpace

theorem

Rules out a finite-dimensional Hilbert space for the faithful tracial model.

Statement

The CAR trace-GNS Hilbert space Hτ carrying the specified faithful representation of the fixed algebra A is infinite-dimensional over ℂ.

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. Use the established faithful representation ρ: A → B(Hτ). No finite-dimensionality or CH hypothesis is assumed.

Conclusion

Hτ is not finite-dimensional over ℂ. Together with the separate separability and nontriviality results, it is a nonzero separable infinite-dimensional complex Hilbert space.

Proof route

If Hτ were finite-dimensional, B(Hτ) would be finite-dimensional. The injective linear map underlying ρ would then make A finite-dimensional, contradicting the counterexample theorem for A.

Main citations

• MathlibAnnex.CStarAlgebra.CAR.not_finiteDimensional_shellFamilyTarget

  Exact source attribution.

• MathlibAnnex.CStarAlgebra.CAR.separableCounterexampleRepresentation_injective

  Exact source attribution.

Lean source declaration (exact)

theorem not_finiteDimensional_separableCounterexampleHilbertSpace :
    ¬ FiniteDimensional ℂ SeparableCounterexampleHilbertSpace := by
  intro hfinite
  letI : FiniteDimensional ℂ SeparableCounterexampleHilbertSpace := hfinite
  letI : FiniteDimensional ℂ
      (SeparableCounterexampleHilbertSpace →L[ℂ] SeparableCounterexampleHilbertSpace) :=
    ContinuousLinearMap.finiteDimensional
  exact (not_finiteDimensional_shellFamilyTarget homogeneityShellFamily)
    (FiniteDimensional.of_injective
      (LinearMapClass.linearMap separableCounterexampleRepresentation)
      separableCounterexampleRepresentation_injective)

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

Lean realization notes

The exact conclusion is ¬ FiniteDimensional ℂ Hτ. A countably infinite orthonormal basis follows by standard Hilbert-space theory from this and separability, not by a new basis-cardinality theorem in the cited declaration. FiniteDimensional here is the ordinary finite-dimensional vector-space predicate.