MATHLIBANNEX / CANONICAL DECLARATION CARD

Uniqueness among all state extensions of the CAR trace

MathlibAnnex.CStarAlgebra.CAR.existsUnique_state_extension_trace

theorem

Pointed transport identifies arbitrary state extensions before traciality is proved.

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 is exactly one state on such that . Uniqueness here ranges over all state extensions, including those not assumed tracial.

Assumptions

Only the fixed representative shell family is given. A competing functional must be a state on and satisfy for every .

Conclusion

Every such equals the chosen extension . The existence and uniqueness refer to the same fixed algebra .

Proof route

Construct the two target GNS representations and apply pointed unitary transport from their common source trace. Equality of the vector functionals then gives equality of states.

Proof steps

  1. Existence is exists_state_extension_trace. For an arbitrary competing state , let be its GNS representation; define for the chosen extension. Both target orbits are dense and their source vector functionals are .

  2. Apply exists_pointed_unitary_of_trace_of_cyclic with the representation first and the representation second. Its hypotheses are exactly the two restriction equalities and target cyclicity. It gives a unitary

  3. For every , preservation of the inner product and these two identities give

    This is the pointwise equality used by eq_traceExtension_of_mem_stateSpace_of_apply_shellFamilySourceHom_eq_trace; extensionality then gives .

Main citations

Lean source signature (exact)

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

∃! φ quantifies a continuous functional on the fixed ShellFamilyTarget family. The conjunction requires state-space membership and restriction equal to trace. The linked uniqueness supplier calls the arbitrary competing state φ and its positive-map bundle f; these correspond to and its positive bundle in the mathematics above. Its proof-local ρ, ξ, and e are the competitor's GNS action, vector and pointed transport toward the chosen extension. Thus records the direction of that e.

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

Lean realization notes

The argument does not use uniqueness among tracial states to prove this stronger extension uniqueness. The unitary below compares the GNS representations of two possibly different extension states; it is not an identification of independently chosen vectors without a transport theorem.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

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

Card revision: 2 · SHA-256: 4e50c44f14a48c8f061646a405c75ba136829cab84f8fd45d4e52cf87386ca33

Exposition revision: 3 · SHA-256: e14c11c65ccfaa24799d351ac5da4d424bf2f2045b087d272589498455e3306c

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: d61ab675d95118f4058336b0fe6bd90d2c6fcb1b1ee5d0b98f88b87262cbb17c

Back to top ↑