MathlibAnnex.CStarAlgebra.CAR.not_isCompactOperatorModel_shellFamilyTarget
Excludes an injective representation of the infinite-dimensional unital algebra onto all compact operators.
Statement
For the fixed shell-generated algebra
Assumptions
Let
Index chosen pure-state Gelfand-Naimark-Segal (GNS) representations by their unitary-equivalence classes
A fixed shell family consists of complex-linear unital star automorphisms
At the root,
Let
Choose once a family of unitary operators
Put
The comparison space
Conclusion
Thus
Proof route
Assume such a map exists. Injectivity and
Proof steps
The zero Hilbert space admits only the zero operator, so it cannot receive an injective representation of the nonzero algebra
. For
, choose a unit vector . The rank-one operator lies in the image for any ; evaluating at gives . A compact identity operator forces finite dimension. Injectivity of the complex-linear map
then transfers finite dimension back to , a contradiction.
Main citations
- Exact declaration and proof · Exact source
- MathlibAnnex.CStarAlgebra.CAR.RepresentativeShellFamily · Exact source
- MathlibAnnex.CStarAlgebra.CAR.exists_completedAtomicShellModel · Exact source
- MathlibAnnex.CStarAlgebra.CAR.not_finiteDimensional_shellFamilyTarget · Exact source
- MathlibAnnex.CStarAlgebra.CAR.shellFamilySourceHom_injective · Exact source
- MathlibAnnex.CStarAlgebra.CAR.not_finiteDimensional · Exact source
- MathlibAnnex.Analysis.CStarAlgebra.not_isCompactOperatorModel_of_infiniteDimensional · Exact source
Lean source signature (exact)
theorem not_isCompactOperatorModel_shellFamilyTarget
(family : RepresentativeShellFamily)
{K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K]
[CompleteSpace K]
(e : ShellFamilyTarget family →⋆ₙₐ[ℂ] (K →L[ℂ] K)) :
¬ IsCompactOperatorModel eHere ShellFamilyTarget family is e is the possibly nonunital star representation into IsCompactOperatorModel e combines three conditions: injectivity, compactness of every
Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF
Lean realization notes
The obstruction uses that
Exact Card identity
Language: en
CARD_CONTENT_COMPLETE
Card UID: lfh:lfh-declaration-card:sha256:613fdafd1f323fb659d8b89d248b1f5902a2cc42585e5fe30392ece18490eeea
Card revision: 1 · SHA-256: 63eb23bc6a8d3e7555fba85b8fa2b3034c6655a355c5a79f27854ee042fbc82b
Exposition revision: 1 · SHA-256: eca1da9d8c8943a3bf1bd549653590a608fec2d3e8df1a4568ca82366332c2a2
Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73
Header SHA-256: 2f51b63ed49da6a9858c2c5c44633ffb35dbc65d72a058ccf36b0f1705919bd3