Constructing the normalized trace on the completed CAR algebra

MathlibAnnex.CStarAlgebra.CAR.trace

def

Carries compatible bounded matrix traces through the algebraic limit, normed union and completion.

Statement

Let with connecting maps , and let embed the stages in the completed CAR algebra. The trace constructed here is the continuous complex-linear functional extending . In particular, .

Definition

At a matrix stage of size , each diagonal entry satisfies . Consequently . Under , each diagonal entry is repeated twice and the normalizing denominator doubles, so the trace is unchanged. Iterating proves compatibility with every later-stage embedding.

The algebraic direct limit identifies two matrices when their images agree in a common later stage. Trace compatibility makes the value independent of the chosen representative. Transport this linear functional to the normed union. Every element there is represented at a finite stage; the stage embeddings preserve norm, so the same bound holds on the union.

For a Cauchy sequence in that union, define the value at its limit by . The bound makes the scalar sequence Cauchy and makes the limit independent of the representing sequence. This is the continuous extension used in the declaration.

Assumptions

The matrix norm is the C*-operator norm. The map is a unital star homomorphism. Its entries with both added bit coordinates zero recover the entries of , so it is injective; relabelling the coordinates does not affect injectivity. The C*-norm theorem for injective star homomorphisms then makes the stage map isometric. Thus the normed union has an unambiguous norm and its completion is . These are proved features of the fixed construction, not new hypotheses about arbitrary directed systems.

Conclusion

The cited extension and stage-evaluation results identify one continuous functional on . The contractivity, normalization, positivity, and trace-identity theorems show , , , and . Thus this extension is a normalized tracial state.

The declaration defines the continuous extension. Positivity, normalization and traciality are separate proved results, not conclusions established merely by giving the definition. Uniqueness among all normalized continuous traces is proved in the CAR trace-uniqueness theorem. No statement about extending this trace to the larger shell-generated target is part of this construction.

noncomputable def trace : Limit →L[ℂ] ℂ :=
  preTrace.extend (UniformSpace.Completion.toComplL : PreCAR →L[ℂ] Limit)

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

Earlier published Card and PDF