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 .

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.

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

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

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

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

Lean source signature (exact)

theorem traceExtension_mul_comm (family : RepresentativeShellFamily)
    (a b : ShellFamilyTarget family) :
    traceExtension family (a * b) = traceExtension family (b * a)

traceExtension family is on the fixed target. The displayed signature states the final identity for arbitrary a b. 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. Stars on operators in the explanation mean Hilbert adjoints; the source uses its exact operator notation.

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

Lean realization notes

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.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

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

Card revision: 1 · SHA-256: 620fecbf0a4335ede2fbb821725d07328b78484d0203a58f214549901eb839bd

Exposition revision: 1 · SHA-256: ac498d0b64ed15dfa1ed369a0c13d7395f866f4e7699d1bf021b06f8d4b48be6

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 27c0a439359ea108d821a45ba0f7fb8b84762c8ec0d4b4257d0fd1db4d5201d0

Back to top ↑