MathlibAnnex.CStarAlgebra.CAR.not_isCompactOperatorModel_shellFamilyTarget
theorem
Excludes an injective representation of the infinite-dimensional unital algebra onto all compact operators.
Statement
For the fixed shell-generated algebra below and any complete complex Hilbert space , there is no injective complex-linear star representation whose image is exactly the compact operators on . The map is not assumed to preserve the unit.
Assumptions
Let be the completed CAR algebra with matrix stages embedded by . Write for the image of the first diagonal matrix unit, , and for the root state characterized by on each stage, where is its canonical embedding.
Index chosen pure-state Gelfand-Naimark-Segal (GNS) representations by their unitary-equivalence classes , with root index and representative states .
A fixed shell family consists of complex-linear unital star automorphisms and elements satisfying , and .
At the root, is the identity and .
Let be the Hilbert direct sum of these GNS spaces, their representation of , and its embedded unit cyclic vector, where is the selected unit cyclic vector and is coordinate inclusion.
Choose once a family of unitary operators from the construction of the shell unitaries: , , and . Here denotes the bounded complex-linear operators on .
Put , the norm-closed unital star algebra generated by these operators. Let be with its codomain restricted to , and let be inclusion.
The comparison space may have any dimension and belongs to an arbitrary independent universe. The exact range condition says both that each is compact and that every compact operator on equals some . Inner products in the rank-one formula are linear in the second argument.
Conclusion
Thus is not isomorphic to the C*-algebra of all compact operators on any complete complex Hilbert space , including the zero Hilbert space. No preservation of the identity is imposed on the candidate representation.
The obstruction uses that is unital and infinite-dimensional, with infinite dimension established in the target-dimension theorem using its injective copy of the completed CAR algebra. It is distinct from results about the intersection of one represented image with the compact operators.
Proof route
Assume such a map exists. Injectivity and first force . Since every rank-one operator is in the image, acts as the identity on every vector: apply to a rank-one operator sending a fixed unit vector to the desired vector. Thus . But is compact, forcing to be finite-dimensional. Then and its complex-linear subspace are finite-dimensional, contradicting the infinite dimension of .
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
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 e
| In the source | Mathematical meaning |
|---|---|
family; ShellFamilyTarget family |
The fixed CAR shell family and its same generated unital infinite-dimensional algebra , containing CAR through the injective source map. |
K; [InnerProductSpace ℂ K]; [CompleteSpace K] |
Any complete complex Hilbert space , including the zero space, in an arbitrary independent universe. |
e : ShellFamilyTarget family →⋆ₙₐ[ℂ] (K →L[ℂ] K) |
A candidate complex-linear star homomorphism , not assumed injective or unital at the outset. |
IsCompactOperatorModel e |
The three simultaneous properties are: is injective; every is a compact operator; and every compact operator on is for some . Thus the range is exactly all compact operators, not merely a subalgebra of them. |
¬ IsCompactOperatorModel e |
These three properties cannot hold together for this candidate . This does not say that no individual represented operator can be compact. |
Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project
Exact content identity
Declaration: MathlibAnnex.CStarAlgebra.CAR.not_isCompactOperatorModel_shellFamilyTarget
Accepted content SHA-256: 7c83a8b40beea4f2dc739cbd22c198fac2f53043ce96a4c8d5fb44139ee92362
Accepted source guide SHA-256: 82930c83bb11b4669f97e66703b5d77ce7e01f26d12965b2d009fe41bee74294
Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73