MATHLIBANNEX / CANONICAL DECLARATION CARD

The unique trace extension is tracial on the whole target

MathlibAnnex.CStarAlgebra.CAR.traceExtension_mul_comm

theorem

Unitary invariance, strong shell sums, and a closed centralizer extend the trace identity beyond the source.

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. Choose the state extension of supplied by state extension along . Its GNS representation is , with

The inner product is linear in its second argument. The -orbit of is dense by the GNS construction. The chosen state is tracial: for every .

Assumptions

The representative shell family is fixed. The state is the chosen extension of the CAR trace, not an arbitrary state. Its uniqueness among all extensions has already been established by the separately cited extension-uniqueness theorem.

Conclusion

Every element of lies in the centralizer of . Thus the trace identity holds for arbitrary pairs of target elements, not just pairs coming from .

Strong convergence is used inside the actual GNS representation . No norm convergence of shell partial sums in , and no strong continuity of an arbitrary representation, is asserted.

Proof route

Use extension uniqueness to prove source-unitary invariance. Linear spanning gives the source centralizer; vector-functional limits give the shell generators. The norm-closed star centralizer then contains the generated algebra.

Proof steps
  1. For a unitary , put and . Unitarity gives , so is a state. Its source restriction is

The last equality uses the source trace and . Extension uniqueness applies and gives , hence for all . This is traceExtension_star_unitary_mul_mul.

  1. Substitute into that invariance equality. Since ,

The four-unitary spanning theorem for a unital complex C*-algebra writes each as . Linearity therefore gives

The exact application of CStarAlgebra.exists_sum_four_unitary is in traceExtension_shellFamilySourceHom_mul.

  1. For a class , let regarded as an element of , let be its source shell partial isometries, and set . The actual-representation shell-sum theorem applies to : the vector functional restricts to , and the target orbit is dense. It gives strongly.

  2. Fix . The source centralizer equality holds for every . Strong convergence at both and , followed by continuity of and the inner product, gives

Uniqueness of the scalar limit proves . This is the precise input/output of vectorFunctional_mul_eq_mul_of_stronglyConverges in traceExtension_shellFamilyGenerator_mul.

  1. Define . State positivity supplies , so is a unital star subalgebra; continuity makes it norm closed. The preceding steps put and all in . The concrete-generation theorem eq_top_of_source_mem_of_generator_mem now yields . Substituting any into its defining property gives .

Main citations

Supporting route explanation

Lean source signature (exact)

theorem traceExtension_mul_comm (family : RepresentativeShellFamily)
    (a b : ShellFamilyTarget family) :
    traceExtension family (a * b) = traceExtension family (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 .
traceExtension family The chosen state extension with . It is this extension, rather than an arbitrary state.
a b : ShellFamilyTarget family Any two target elements , not necessarily elements of the source image.
traceExtension family (a * b) = traceExtension family (b * a) The whole conclusion is , reversing the order of these target products. Source-unitary invariance, shell sums and the centralizer belong to the linked proof, not additional input assumptions.

Further source notes: The linked proof’s stateCentralizer is . Its source and generator membership suppliers carry the unitary argument and strong-limit argument described above; they are separately linked proof results, not extra signature assumptions.

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

Accepted content SHA-256: 3a52e5a31078343188f579eccaf3be4ebdbf2a81c6a275283c4ea5e9e76c794d

Accepted source guide SHA-256: dd153865910b9d9ad61dda16a5ad0a3992bf911be3fc810695d1cc4602b8b185

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑