The CAR algebra as a completion of finite matrix stages

MathlibAnnex.CStarAlgebra.CAR.Limit

abbrev

Names the completed CAR algebra in which finite matrix calculations can be extended by norm approximation.

Statement

For , let with its operator norm, and include in by . The completed CAR algebra is the norm completion of the resulting increasing algebraic union. The declaration names this completion; the cited constructions supply its algebra and involution.

Definition

Identify two finite-stage elements when their images agree in a common later stage. Addition, multiplication, scalar multiplication and adjoint can then be computed after passing to such a common stage. Isometry of the embeddings makes the norm of a represented element independent of its stage. Denote this normed union by . Define , its Hausdorff norm completion. Equivalently, elements of are limits of Cauchy sequences from , with two sequences identified when their difference tends to zero. The Lean name Limit denotes this CAR algebra ; PreCAR denotes the normed union . Here abbrev introduces a readily unfoldable name for UniformSpace.Completion PreCAR, not a second algebra or an additional theorem. Its full defining expression is displayed below.

Assumptions

The stages carry their usual complex matrix algebra operations and adjoint. The fixed embeddings are unital, preserve adjoints and are isometric. The index begins at , where . There is no freely chosen representation or additional hypothesis on another algebra.

Conclusion

Each stage has a canonical unital star homomorphism . These maps preserve norms, hence are injective, satisfy , and have a dense union of ranges. With the operations extended from the union, is a unital complex C*-algebra. These structural facts are furnished by the separately cited stage maps, density result and completion instances; they explain how the named completion is used.

The finite matrix stages form a dense subalgebra. The completion allows limits of norm-Cauchy sequences from that union. The construction uses the compatible operator norms of the stages; no new norm is chosen by taking a supremum over representations.

abbrev Limit := UniformSpace.Completion PreCAR

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

Earlier published Card and PDF