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.

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

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.

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

Supporting route explanation

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
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 is a continuous complex-linear functional satisfying both following requirements.
φ ∈ ... stateSpace (ShellFamilyTarget family) This same is a state: positive and normalized by .
∀ b, φ (shellFamilySourceHom family b) = trace b For every source element , . Its values on the entire target are not assumed tracial here, and uniqueness is not this existence statement.

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

Earlier published Card and PDF

Exact content identity

Declaration: MathlibAnnex.CStarAlgebra.CAR.exists_state_extension_trace

Accepted content SHA-256: 867b4ec58322b80e7e5c2d43b2671be8a1db6b0e89399e04dc3f15c0be43e16c

Accepted source guide SHA-256: 23d26b9219a18be51018302dbf3500258971b5bc55e33d45d4fe39b4a056d96f

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑