Unique extension of the CAR trace among all states

MathlibAnnex.CStarAlgebra.CAR.existsUnique_state_extension_trace

theorem

Establishes uniqueness of a state extension without assuming the extension is tracial.

Statement

For every representative shell family F, the normalized trace τC on the CAR algebra C extends to exactly one state of the associated C*-algebra A_F.

Assumptions

Let C be the completed CAR algebra, φ₀ its distinguished pure state, φᵢ one selected pure state in each GNS-equivalence class, and eₙ the fixed root shell projections. Fix a representative shell family F: for each i, an automorphism αᵢ and elements wᵢ,ₙ of C satisfying φᵢ ∘ αᵢ = φ₀, wᵢ,ₙ* wᵢ,ₙ = αᵢ(eₙ), and wᵢ,ₙ wᵢ,ₙ* = eₙ. At the root class, α₀ is the identity and w₀,ₙ = eₙ. Let A_F ⊆ B(Hₐₜ) be the norm-closed unital *-algebra generated by the atomic image of C and the shell-link unitaries constructed from F; write j_F: C → A_F for the source map. Let τC be the normalized CAR trace. The family parameter F is retained; it is not replaced by an arbitrary C*-algebra.

Conclusion

There exists a unique continuous complex-linear functional φ: A_F → ℂ which is positive, satisfies φ(1) = 1, and obeys φ(j_F(c)) = τC(c) for every c ∈ C.

Proof route

The constructed trace extension gives existence. Compare the cyclic GNS representation of any other state extension with the constructed tracial representation by a pointed unitary; equality of their vector states gives uniqueness.

Main citations

• MathlibAnnex.CStarAlgebra.CAR.eq_traceExtension_of_mem_stateSpace_of_apply_shellFamilySourceHom_eq_trace

  Exact source attribution.

Lean source declaration (exact)

/-- Existence and uniqueness are on the actual fixed target. -/
theorem existsUnique_state_extension_trace (family : RepresentativeShellFamily) :
    ∃! φ : ShellFamilyTarget family →L[ℂ] ℂ,
      φ ∈ MathlibAnnex.Analysis.CStarAlgebra.stateSpace (ShellFamilyTarget family) ∧
        ∀ b, φ (shellFamilySourceHom family b) = trace b := by
  refine ⟨traceExtension family,
    ⟨traceExtension_mem_stateSpace family, traceExtension_shellFamilySourceHom family⟩, ?_⟩
  intro φ hφ
  exact eq_traceExtension_of_mem_stateSpace_of_apply_shellFamilySourceHom_eq_trace family φ hφ.1 hφ.2

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

Lean realization notes

The source theorem is family-parametric. Uniqueness is among all state extensions of this particular trace, not merely among tracial extensions, and not among all states on A_F. Traciality and faithfulness are separate conclusions elsewhere. Taking the fixed homogeneity family recovers the algebra A.