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.

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

Here Limit is and trace is . The type of f already requires a continuous complex-linear functional. The hypotheses hf1 and hf are respectively and . 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

Lean realization notes

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.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:e409951550e6bcc3cae01d9629ee27cb7ecfa02f4c8c15e123c847dd0e9a3483

Card revision: 1 · SHA-256: fafb2f938443a7ab0bee926c777a77a8e375101daf89d13a6474ac14c23a46eb

Exposition revision: 1 · SHA-256: 69817d0b5b4ca0039f01b01b7dcb4b66aa597051117f42357723459ee4361dd0

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 205aaf3d7861e1808c6b0414f4cd54b83b0cb1d84c180beda2e999a91ba2b923

Back to top ↑