MathlibAnnex.CStarAlgebra.CAR.not_finiteDimensional
theorem
Rules out finite dimension by retaining matrix subalgebras of unbounded dimension.
Statement
Let be the norm completion of the matrix system with embeddings . Then is not finite-dimensional as a complex vector space.
Assumptions
The algebra is the fixed completed CAR algebra. For every , its canonical stage map is complex-linear and injective, and . These are established properties of this construction, not new assumptions on an arbitrary algebra.
Conclusion
No finite integer can be the complex dimension of : every stage contributes an embedded vector space of dimension , and these dimensions are unbounded.
The conclusion concerns vector-space dimension over . It does not require an irreducible representation or a claim about compact operators.
Proof route
If had finite dimension , injectivity of each would give . Take . The elementary inequality contradicts that bound.
Proof steps
Assume that is finite-dimensional and write .
The linear injection forces .
The stage dimension is , yielding the contradiction.
Main citations
Lean source signature (exact)
theorem not_finiteDimensional : ¬ FiniteDimensional ℂ Limit| In the source | Mathematical meaning |
|---|---|
Limit |
The completed CAR algebra of the Statement. |
FiniteDimensional ℂ Limit |
The assertion that has a finite basis as a complex vector space. |
¬ FiniteDimensional ℂ Limit |
The theorem denies that assertion: is not finite. It says nothing about the dimension of a representing Hilbert space and does not deny separability. |
Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project
Exact content identity
Declaration: MathlibAnnex.CStarAlgebra.CAR.not_finiteDimensional
Accepted content SHA-256: f5c7800f7da0e611f2f6db1575a66fc56320e596083feacd87fcaffeb7cab4e0
Accepted source guide SHA-256: 9582d2284e34052391ae7ccc55cdda58e1b2d1de85339f17560f45da55c6bd9f
Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73