Faithfulness of the separable tracial representation

MathlibAnnex.CStarAlgebra.CAR.separableCounterexampleRepresentation_injective

theorem

Proves injectivity of the specified representation rather than introducing a new algebra or a new witness.

Statement

The tracial representation ρ: A → B(Hτ) of the fixed CAR-based algebra on the CAR trace-GNS space is faithful.

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. Let ρ be the specified representation obtained by pointed unitary transport of the tracial model.

Conclusion

ρ is injective: for all a, b ∈ A, ρ(a) = ρ(b) implies a = b. In particular, ρ(a) = 0 implies a = 0.

Proof route

Specialize injectivity of the family-parametric trace-model representation to the fixed homogeneity family.

Main citations

• MathlibAnnex.CStarAlgebra.CAR.traceModelRepresentation_injective

  Exact source attribution.

Lean source declaration (exact)

theorem separableCounterexampleRepresentation_injective :
    Function.Injective separableCounterexampleRepresentation :=
  traceModelRepresentation_injective homogeneityShellFamily

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

Lean realization notes

The literal conclusion is Function.Injective separableCounterexampleRepresentation. Separability of Hτ is a separate established fact; the isometry property and the faithfulness of the scalar trace are separate statements as well. Injectivity does not imply irreducibility here.