MATHLIBANNEX / CANONICAL DECLARATION CARD

The fixed shell target has a unique tracial state

MathlibAnnex.CStarAlgebra.CAR.existsUnique_tracial_state

theorem

Every tracial state is forced back to the CAR trace and hence to its unique extension.

Statement

Let be the completed CAR algebra and its normalized trace. Fix a representative shell family and its chosen unitary links in the selected atomic representation . Write for the resulting concrete target and , , for its faithful unital source map. This fixes one target and one source map throughout. There exists exactly one state such that for all .

Assumptions

The representative shell family is fixed. A competing functional is required to be a state and tracial on ; equality with on the source is derived, not assumed.

Conclusion

The unique tracial state is the chosen extension traceExtension family. This uniqueness quantifies all tracial states on , whereas extension uniqueness quantifies all states with the prescribed source restriction.

Proof route

Produce the tracial extension, restrict any other tracial state to the source, and invoke the two uniqueness results in that order.

Proof steps

  1. The extension theorem gives a state with , and traceExtension_mul_comm proves it tracial on . This supplies the existence part.

  2. For any tracial state on , the functional is continuous and complex linear. Since preserves and products,

    CAR trace uniqueness, eq_trace_of_apply_one_of_mul_comm, therefore gives . That source theorem determines values on matrix units and extends from finite stages by density; no target-separability hypothesis is used.

  3. Now is a state extension of . The extension-equality theorem applies and gives . In the source, these two steps are apply_shellFamilySourceHom_eq_trace_of_apply_one_of_mul_comm followed by eq_traceExtension_of_mem_stateSpace_of_mul_comm.

Main citations

Lean source signature (exact)

theorem existsUnique_tracial_state (family : RepresentativeShellFamily) :
    ∃! φ : ShellFamilyTarget family →L[ℂ] ℂ,
      φ ∈ MathlibAnnex.Analysis.CStarAlgebra.stateSpace (ShellFamilyTarget family) ∧
        ∀ a b, φ (a * b) = φ (b * a)

∃! φ ranges over continuous functionals on ShellFamilyTarget family; the predicate includes state-space membership and the identity for all a b. In contrast to the extension-uniqueness signature, it does not prescribe source values. The proof derives those values using CAR trace uniqueness before applying extension uniqueness.

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

Lean realization notes

Faithfulness of a representation and faithfulness of this state are different assertions. This theorem asserts existence and uniqueness of a tracial state. The separate result traceExtension_star_mul_self_eq_zero_iff concerns state faithfulness and is not an additional hypothesis here.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

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

Card revision: 2 · SHA-256: b44fc1eb359af758468f55442e998fc4f91a92be8dcf566311f37e8b000bc06f

Exposition revision: 3 · SHA-256: 0bd44fead9f058ef6ab97fcb1774f55d403cba3f128d6d1f602d5374423d3282

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: d9616be03bf1f37107e291058c9b4567c3482f114198ecb6d4b99c687513b78c

Back to top ↑