MATHLIBANNEX / CANONICAL DECLARATION CARD

Extending the CAR trace to the fixed shell target

MathlibAnnex.CStarAlgebra.CAR.exists_state_extension_trace

theorem

The source trace first becomes a state on the existing target algebra.

Statement

Let be the completed CAR algebra, the completion of the matrix system , and let be its normalized trace. Fix a representative shell family: for each chosen pure-GNS class it specifies an automorphism and partial isometries between the transported and root shells. Fix the links chosen by this family in the selected atomic representation . Throughout this Card,

Thus is the already constructed concrete unital C*-algebra, and is its injective source map. The links and target are kept fixed. A state means a positive continuous complex linear functional taking to . There exists a state on satisfying for every .

Assumptions

The representative shell family is fixed. No representation of the target is an additional input to this extension theorem.

Conclusion

The set of state extensions of to this same is nonempty. Traciality on all of and uniqueness of the extension are separate results.

Proof route

Transfer to the isometric copy , extend the bounded functional, and use normalization to obtain positivity.

Proof steps

  1. The injective unital C*-homomorphism is isometric. Consequently is well-defined and satisfies

    The input bounds are norm_trace_le and trace_one, and injectivity is shellFamilySourceHom_injective.

  2. Apply the state-extension theorem for an injective unital star homomorphism, exists_state_extension_of_injective, with source functional . Its Hahn–Banach step extends with norm at most ; its normalized-contraction positivity argument makes the extension a state. Its restriction equality gives exactly .

Main citations

Lean source signature (exact)

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

Here Limit, trace, ShellFamilyTarget family, and shellFamilySourceHom family are . The quantified φ is a state on , and the final ∀ b is equality on every source element. The linked proof invokes exists_state_extension_of_injective; that supplier is named in the proof, not in the displayed theorem signature.

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

Lean realization notes

The extension theorem supplies an existence witness. The later definition traceExtension chooses one such witness; it does not change or create a universal completion.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:38f9dd2dee94e30e47039f5563b5824820090e96460226e5f8062b19b31c285b

Card revision: 1 · SHA-256: 27922027d64747500d388ffe7fff3d06d4640882cdd419547b722bf62435216f

Exposition revision: 1 · SHA-256: 707d398151dff952b4ac7f9f3a2d77758871512cb5e2c89ecf821bee48815366

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: d1486a60cf0e297220cb4332e4da33794189a958f967133070af063b89255d8e

Back to top ↑