The representation on the CAR trace-GNS space

MathlibAnnex.CStarAlgebra.CAR.separableCounterexampleRepresentation

def

Defines a separable-space representation of exactly the same algebra A.

Statement

Define ρ: A → B(Hτ) on the CAR trace-GNS space Hτ = L²(C, τC) by transporting the previously constructed tracial representation along the pointed unitary identifying its CAR-cyclic model with Hτ.

Definition

The unitary V preserves the distinguished cyclic trace vector and intertwines the CAR actions. Conjugating the tracial representation by V places the target algebra on the original CAR trace-GNS space. Separability of Hτ and faithfulness of ρ are established separately; this definition does not assert irreducibility.

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 fixed homogeneity shell family and the chosen pointed unitary V: Hτ → Htr from the CAR GNS space to the constructed target-state GNS space.

Conclusion

A specified unital complex *-homomorphism ρ: A → B(Hτ), with ρ(a) = V⁻¹ πtr(a) V. The domain is the same A as in the atomic representation.

Main citations

• MathlibAnnex.CStarAlgebra.CAR.traceModelRepresentation

  Exact source attribution.

Lean source declaration (exact)

/-- A faithful representation of exactly the existing atomic counterexample
on a separable Hilbert space. -/
noncomputable def separableCounterexampleRepresentation :
    Representation AtomicCounterexampleAlgebra SeparableCounterexampleHilbertSpace :=
  traceModelRepresentation homogeneityShellFamily

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

Lean realization notes

Source kind: noncomputable def. Exact name: separableCounterexampleRepresentation. SeparableCounterexampleHilbertSpace abbreviates TraceHilbertSpace. The definition is traceModelRepresentation homogeneityShellFamily. The faithfulness theorem for the separable tracial representation proves injectivity; the exclusion of separable irreducible representations excludes nonzero irreducibility on a separable space.