MathlibAnnex.CStarAlgebra.CAR.existsUnique_state_extension_trace

Exact source view. Private integrated preview.

Exact declaration: MathlibAnnex.CStarAlgebra.CAR.existsUnique_state_extension_trace

MathlibAnnex/Analysis/CStarAlgebra/CAR/TraceExtensionUnique.lean · lines 52–60

Raw UTF-8 source

1import MathlibAnnex.Analysis.CStarAlgebra.CAR.TracialRepresentation
2import MathlibAnnex.Analysis.CStarAlgebra.CAR.TracialTransport
3
4/-!
5# Uniqueness of the extension of the CAR trace
6
7This is uniqueness among all state extensions, not merely among traces.
8-/
9
10set_option autoImplicit false
11
12open scoped InnerProduct
13
14namespace MathlibAnnex.CStarAlgebra.CAR
15
16open MathlibAnnex.Analysis.CStarAlgebra
17
18/-- Any state extending the original CAR trace is the chosen extension. -/
19theorem eq_traceExtension_of_mem_stateSpace_of_apply_shellFamilySourceHom_eq_trace
20    (family : RepresentativeShellFamily) (φ : ShellFamilyTarget family →L[ℂ] ℂ)
21    (hφ : φ ∈ MathlibAnnex.Analysis.CStarAlgebra.stateSpace (ShellFamilyTarget family))
22    (hφB : ∀ b, φ (shellFamilySourceHom family b) = trace b) :
23    φ = traceExtension family := by
24  let f := positiveLinearMapOfMemStateSpace φ hφ
25  let ρ : Representation (ShellFamilyTarget family) f.GNS := f.gnsStarAlgHom
26  let ξ : f.GNS := f.gnsCyclicVector
27  have hξ (b : Limit) : Representation.vectorFunctional
28      (ρ.comp (shellFamilySourceHom family)) ξ b = trace b := by
29    change inner ℂ f.gnsCyclicVector (f.gnsStarAlgHom _ f.gnsCyclicVector) = _
30    rw [PositiveLinearMap.inner_gnsCyclicVector_gnsStarAlgHom]
31    exact hφB b
32  have hcyclic : DenseRange (fun a ↦ ρ a ξ) :=
33    f.denseRange_gnsStarAlgHom_apply_gnsCyclicVector
34  obtain ⟨e, heξ, he⟩ := exists_pointed_unitary_of_trace_of_cyclic family
35    ρ (tracialRepresentation family) ξ (tracialVector family) hξ
36    (vectorFunctional_tracialRepresentation_source family) hcyclic
37    (denseRange_tracialRepresentation_orbit family)
38  apply ContinuousLinearMap.ext
39  intro a
40  calc
41    φ a = inner ℂ ξ (ρ a ξ) := (f.inner_gnsCyclicVector_gnsStarAlgHom a).symm
42    _ = inner ℂ (e ξ) (e (ρ a ξ)) := (e.inner_map_map ξ (ρ a ξ)).symm
43    _ = inner ℂ (tracialVector family)
44        (tracialRepresentation family a (tracialVector family)) := by
45      have hcoe (y : f.GNS) :
46          (e : f.GNS →L[ℂ] TracialHilbertSpace family) y = e y := rfl
47      have h := congrArg (fun T : f.GNS →L[ℂ] TracialHilbertSpace family ↦ T ξ) (he a)
48      simpa only [ContinuousLinearMap.comp_apply, hcoe, heξ] using
49        congrArg (fun y ↦ inner ℂ (e ξ) y) h
50    _ = traceExtension family a := inner_tracialVector_tracialRepresentation family a
51
52/-- Existence and uniqueness are on the actual fixed target. -/
53theorem existsUnique_state_extension_trace (family : RepresentativeShellFamily) :
54    ∃! φ : ShellFamilyTarget family →L[ℂ] ℂ,
55      φ ∈ MathlibAnnex.Analysis.CStarAlgebra.stateSpace (ShellFamilyTarget family) ∧
56        ∀ b, φ (shellFamilySourceHom family b) = trace b := by
57  refine ⟨traceExtension family,
58    ⟨traceExtension_mem_stateSpace family, traceExtension_shellFamilySourceHom family⟩, ?_⟩
59  intro φ hφ
60  exact eq_traceExtension_of_mem_stateSpace_of_apply_shellFamilySourceHom_eq_trace family φ hφ.1 hφ.2
61
62end MathlibAnnex.CStarAlgebra.CAR