The counterexample with its faithful separable tracial model

MathlibAnnex.CStarAlgebra.CAR.atomicCounterexampleEndpoint_and_separable_tracial_representation

theorem

Collects the ordinary counterexample, its separable representation, and its faithful unique trace without changing the algebra.

Statement

The fixed CAR-based C*-algebra A satisfies the complete ordinary counterexample assertion and has a faithful isometric representation ρ on a nonzero separable Hilbert space Hτ. This representation is not irreducible. The distinguished state τ on A is a faithful trace and is the unique tracial state of A.

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 on Hτ, and let τ be the distinguished extension of the CAR trace to A. No extra assumptions of faithfulness, traciality, simplicity, or CH are made.

Conclusion

The ordinary counterexample assertion holds for this A, including the faithful atomic irreducible model and uniqueness among all nonzero irreducible comparison representations. In addition: Hτ is nontrivial and separable; ρ is injective and isometric; ρ is not nonzero irreducible; τ is a state; τ(ab) = τ(ba) for all a, b ∈ A; τ(a*a) = 0 if and only if a = 0; and every tracial state of A equals τ.

Proof route

Assemble the independently proved ordinary, representation, and trace statements for the fixed homogeneity family.

Main citations

• MathlibAnnex.CStarAlgebra.CAR.atomicCounterexampleTrace_star_mul_self_eq_zero_iff

  Exact source attribution.

• MathlibAnnex.CStarAlgebra.CAR.eq_atomicCounterexampleTrace_of_mem_stateSpace_of_mul_comm

  Exact source attribution.

Lean source declaration (exact)

theorem atomicCounterexampleEndpoint_and_separable_tracial_representation :
    AtomicCounterexampleEndpoint.{v} ∧
    Nontrivial SeparableCounterexampleHilbertSpace ∧
    TopologicalSpace.SeparableSpace SeparableCounterexampleHilbertSpace ∧
    Function.Injective separableCounterexampleRepresentation ∧
    Isometry separableCounterexampleRepresentation ∧
    ¬ Representation.IsIrreducible separableCounterexampleRepresentation ∧
    atomicCounterexampleTrace ∈
      MathlibAnnex.Analysis.CStarAlgebra.stateSpace AtomicCounterexampleAlgebra ∧
    (∀ a b, atomicCounterexampleTrace (a * b) = atomicCounterexampleTrace (b * a)) ∧
    (∀ a, atomicCounterexampleTrace (star a * a) = 0 ↔ a = 0) ∧
    (∀ φ : AtomicCounterexampleAlgebra →L[ℂ] ℂ,
      φ ∈ MathlibAnnex.Analysis.CStarAlgebra.stateSpace AtomicCounterexampleAlgebra →
      (∀ a b, φ (a * b) = φ (b * a)) → φ = atomicCounterexampleTrace) :=
  ⟨shellFamilyEndpoint homogeneityShellFamily,
    nontrivial_traceHilbertSpace,
    separableSpace_separableCounterexampleHilbertSpace,
    separableCounterexampleRepresentation_injective,
    isometry_separableCounterexampleRepresentation,
    not_isIrreducible_separableCounterexampleRepresentation,
    atomicCounterexampleTrace_mem_stateSpace,
    atomicCounterexampleTrace_mul_comm,
    atomicCounterexampleTrace_star_mul_self_eq_zero_iff,
    eq_atomicCounterexampleTrace_of_mem_stateSpace_of_mul_comm⟩

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

Lean realization notes

Faithfulness of τ means its explicit square-vanishing criterion and is distinct from injectivity of ρ. The theorem does not infer faithfulness from uniqueness alone. The atomic irreducible model acts on Hₐₜ, not Hτ. The GNS interpretation is supported by the cyclic-vector and pointed-unitary results; the exact conjunction is displayed separately below. This declaration has no assigned level in the pinned Project scope.