The fixed CAR-based C*-algebra

MathlibAnnex.CStarAlgebra.CAR.AtomicCounterexampleAlgebra

abbrev

Defines the one algebra used throughout the irreducible, separable, tracial, and density results.

Statement

Let C be the completed CAR algebra and Π its atomic representation on Hₐₜ. Use the source-defined family of homogeneity automorphisms and shell data to choose shell-link unitaries Lᵢ on Hₐₜ. Define A = C*(Π(C) ∪ {Lᵢ : i ∈ I}) ⊆ B(Hₐₜ), where C*(…) means the norm-closed unital *-algebra generated by the displayed operators.

Definition

The Hilbert space Hₐₜ is the Hilbert direct sum of the selected pure-state GNS spaces, including the designated root component. The operators Lᵢ are the full shell-link unitaries obtained from the shell data, not the individual partial-isometry elements of C. The algebra is generated inside an existing bounded-operator algebra; no universal completion is postulated.

Assumptions

The CAR algebra C, the distinguished root pure state, the selected atomic GNS representation Π on Hₐₜ, and the one homogeneity-based shell family have already been fixed by the construction. There is no additional assumption of simplicity, capture of representations, or the KOS theorem.

Conclusion

The abbreviation denotes the concrete closed unital *-subalgebra A of B(Hₐₜ). Its carrier is used as a C*-algebra in later declarations. This declaration defines A; it does not by itself assert all the later counterexample properties.

Main citations

• MathlibAnnex.CStarAlgebra.CAR.homogeneityShellFamily

  Exact source attribution.

• MathlibAnnex.CStarAlgebra.CAR.ShellFamilyTarget

  Exact source attribution.

Lean source declaration (exact)

/-- The single concrete C-star algebra used by every field of `AtomicCounterexampleEndpoint`. -/
abbrev AtomicCounterexampleAlgebra := ShellFamilyTarget homogeneityShellFamily

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

Lean realization notes

Source kind: abbrev. Exact name: AtomicCounterexampleAlgebra. The elaborated value has type StarSubalgebra ℂ B(Hₐₜ); its use as a carrier employs the standard coercion. The chosen family is homogeneityShellFamily and the target is ShellFamilyTarget of that family. “Fixed” refers to one source-defined classical choice, not uniqueness of all possible presentations. The counterexample properties are established by the counterexample theorem for A; they are not inputs to this abbreviation.