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 .

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.

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

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

Supporting route explanation

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
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 exists exactly one continuous complex-linear functional satisfying the two following conditions together.
φ ∈ ... stateSpace (ShellFamilyTarget family) is positive and satisfies .
∀ b, φ (shellFamilySourceHom family b) = trace b Its restriction is for every . Any other state with this same restriction equals , without being assumed tracial. This does not say that all states on coincide.

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

Earlier published Card and PDF

Exact content identity

Declaration: MathlibAnnex.CStarAlgebra.CAR.existsUnique_state_extension_trace

Accepted content SHA-256: 7cc334a512bcad3c43e64c59aa327eebe3bab0ab009cb16edc4bb10ead4246c0

Accepted source guide SHA-256: 47b788ef24df2c4709a275c1dd408f69f0c1c06a10ced2368a90d8c8cf3f452f

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑