MATHLIBANNEX / CANONICAL DECLARATION CARD

Normalization and the trace identity determine the CAR trace

MathlibAnnex.CStarAlgebra.CAR.eq_trace_of_apply_one_of_mul_comm

theorem

Proves uniqueness without assuming positivity of the competing continuous functional.

Statement

Let be the completion of under , with normalized trace . If a continuous complex-linear functional satisfies and for every , then .

Assumptions

Continuity, complex linearity, normalization and the trace identity are the hypotheses on . Positivity, faithfulness and an a priori norm bound of one are not additional hypotheses. Let be the canonical stage embedding. Write for the matrix units of a stage of size .

Conclusion

There is at most one normalized continuous trace on , and the continuous functional defined in the CAR trace construction supplies it. In particular any tracial state equals , but the assertion applies to the larger class of functionals specified above.

The argument depends on continuity at the last density step. It makes no uniqueness assertion for arbitrary discontinuous algebraic functionals, or for states without the trace identity.

Proof route

The trace identity and matrix-unit multiplication force all diagonal values to agree and all off-diagonal values to vanish. Since , each diagonal value equals . Hence equals the normalized matrix trace on every stage. The union of stage images is dense in , so continuity gives equality everywhere.

Proof steps

  1. Apply the trace identity to and to obtain equal diagonal values.

  2. For , the products and give . Normalization now gives .

  3. Expand any stage matrix in matrix units. Linear equality on all stages extends to the completion because and are continuous and the stage union is dense.

Main citations

Lean source signature (exact)

theorem eq_trace_of_apply_one_of_mul_comm
    (f : Limit →L[ℂ] ℂ) (hf1 : f 1 = 1)
    (hf : ∀ a b, f (a * b) = f (b * a)) : f = trace
In the source Mathematical meaning
f : Limit →L[ℂ] ℂ A given continuous complex-linear functional , with the completed CAR algebra.
hf1 : f 1 = 1 The normalization .
hf : ∀ a b, f (a * b) = f (b * a) For every ordered pair , assume . This is the trace identity, with no positivity assumption.
f = trace The conclusion : for every , where is the normalized continuous CAR trace.

Further source notes: Thus the source conclusion f = trace is the uniqueness assertion in the Statement, without a positivity hypothesis.

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

Earlier published Card and PDF

Exact content identity

Declaration: MathlibAnnex.CStarAlgebra.CAR.eq_trace_of_apply_one_of_mul_comm

Accepted content SHA-256: 50c42fa3076bcd131e25d8f69c490ba6bcf5ebe57f66a8177b4fe903b6d8c939

Accepted source guide SHA-256: e1958dc14ce8b4b354e4bc20754f36ee25d859e1e7d3556a93a1314ab06a1d25

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑