The completed CAR algebra is infinite-dimensional

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.

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

Here Limit is the completed CAR algebra . The expression FiniteDimensional ℂ Limit means that has finite complex dimension, and the symbol ¬ negates that assertion.

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

Lean realization notes

The conclusion concerns vector-space dimension over . It does not require an irreducible representation or a claim about compact operators.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:65d7b879c0b5f0d302e831d587a4e6e555fe9c2d15bae7acacfc893ed9bcbcf2

Card revision: 1 · SHA-256: 8cb90ce94dfc1cc148315061e79dc108a836a18dfa44f9f57eaf13c52c38ff3e

Exposition revision: 1 · SHA-256: 707caa7d9e51c72dde81699ddc81c889694c5837b1f00de03236ecb7bdd1d72f

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 182c9184c3eee3ce2b2429ff2e1d63708bd4df20723912dff8c623475b78622e