The complete ordinary counterexample assertion

MathlibAnnex.CStarAlgebra.CAR.AtomicCounterexampleEndpoint

abbrev

Names the precise collection of properties later established for the fixed algebra.

Statement

For the fixed CAR-based algebra A, its CAR map j: C → A, and its atomic inclusion πₐₜ: A → B(Hₐₜ), define the ordinary counterexample assertion to be the conjunction of the properties listed below.

Definition

A is nontrivial and norm closed in B(Hₐₜ). The CAR source map j: C → A is injective and satisfies j(1) = 1. A is infinite-dimensional over ℂ. The inclusion πₐₜ: A → B(Hₐₜ) is faithful, nonzero, and irreducible. For every complex Hilbert space K and every nonzero irreducible *-representation σ: A → B(K), not initially required to preserve the unit, there is a surjective complex-linear isometry U: Hₐₜ → K with U(πₐₜ(a)x) = σ(a)(Ux) for all a ∈ A and x ∈ Hₐₜ. Every norm-closed two-sided ideal of A is either {0} or A. For every complex Hilbert space K, there is no injective complex-linear *-homomorphism e: A → B(K), not required to preserve the unit, whose image consists of compact operators and contains every compact operator on K.

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. Fix the source map j and the ambient inclusion πₐₜ from that same construction. Comparison spaces K are arbitrary complete complex Hilbert spaces in the independent comparison universe; no separability is required.

Conclusion

The result of this abbreviation is a proposition consisting of the listed ten source fields. Defining that proposition is distinct from proving it; the counterexample theorem for A supplies the proof.

Main citations

• MathlibAnnex.CStarAlgebra.CAR.ShellFamilyEndpoint

  Exact source attribution.

Lean source declaration (exact)

/-- Fully expanded ordinary endpoint for the single target chosen above. -/
abbrev AtomicCounterexampleEndpoint : Prop :=
  ShellFamilyEndpoint.{v} homogeneityShellFamily

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

Lean realization notes

Source kind: abbrev with result Prop. Exact name: AtomicCounterexampleEndpoint. The seven displayed groups preserve all ten fields of ShellFamilyEndpoint: nontrivial_target, isClosed_target, source_injective, source_unital, not_finiteDimensional_target, ambient_injective, isIrreducible_ambient, captures_nonunital, closedIdeal_dichotomy, not_compactOperatorModel. Here irreducibility includes nonzeroness. The last field is an exclusion of a model of the entire compact-operator algebra, not of one particular embedding. No separable, trace, cardinality, or density condition is part of this definition.