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.

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.

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.

  1. 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

Supporting route explanation

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)
In the source Mathematical meaning
family : RepresentativeShellFamily; ShellFamilyTarget family The fixed CAR shell family and once-chosen links determine the same concrete target throughout.
shellFamilySourceHom family; trace The faithful unital source map , , and the normalized CAR trace .
∃! φ : ShellFamilyTarget family →L[ℂ] ℂ There is exactly one continuous complex-linear functional satisfying the following state and trace conditions simultaneously.
φ ∈ ... stateSpace (ShellFamilyTarget family) is positive and normalized: .
∀ a b, φ (a * b) = φ (b * a) For every pair , . The quantifier includes all target elements. No source-restriction condition is imposed in this predicate; is derived in the proof before extension uniqueness is applied.

Further source notes: 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 · Back to Project

Earlier published Card and PDF

Exact content identity

Declaration: MathlibAnnex.CStarAlgebra.CAR.existsUnique_tracial_state

Accepted content SHA-256: d5f53c2203ea9706a87a450b8a5bf899e58fdfcadcf555dea645e6613ebc82d4

Accepted source guide SHA-256: 76bfcb9157448d43db1de5128c1d282c39747e29c2f09b046e566eace27b79d8

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑