Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/TraceExtensionUnique.lean
Pinned GitHub source · Raw UTF-8 source
Back to Uniqueness among all state extensions of the CAR trace · Back to The fixed shell target has a unique tracial state · Back to The unique trace extension is tracial on the whole target
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.TracialRepresentation2import MathlibAnnex.Analysis.CStarAlgebra.CAR.TracialTransport34/-!5# Uniqueness of the extension of the CAR trace67This is uniqueness among all state extensions, not merely among traces.8-/910set_option autoImplicit false1112open scoped InnerProduct1314namespace MathlibAnnex.CStarAlgebra.CAR1516open MathlibAnnex.Analysis.CStarAlgebra1718/-- Any state extending the original CAR trace is the chosen extension. -/19theorem eq_traceExtension_of_mem_stateSpace_of_apply_shellFamilySourceHom_eq_trace20 (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 := by24 let f := positiveLinearMapOfMemStateSpace φ hφ25 let ρ : Representation (ShellFamilyTarget family) f.GNS := f.gnsStarAlgHom26 let ξ : f.GNS := f.gnsCyclicVector27 have hξ (b : Limit) : Representation.vectorFunctional28 (ρ.comp (shellFamilySourceHom family)) ξ b = trace b := by29 change inner ℂ f.gnsCyclicVector (f.gnsStarAlgHom _ f.gnsCyclicVector) = _30 rw [PositiveLinearMap.inner_gnsCyclicVector_gnsStarAlgHom]31 exact hφB b32 have hcyclic : DenseRange (fun a ↦ ρ a ξ) :=33 f.denseRange_gnsStarAlgHom_apply_gnsCyclicVector34 obtain ⟨e, heξ, he⟩ := exists_pointed_unitary_of_trace_of_cyclic family35 ρ (tracialRepresentation family) ξ (tracialVector family) hξ36 (vectorFunctional_tracialRepresentation_source family) hcyclic37 (denseRange_tracialRepresentation_orbit family)38 apply ContinuousLinearMap.ext39 intro a40 calc41 φ a = inner ℂ ξ (ρ a ξ) := (f.inner_gnsCyclicVector_gnsStarAlgHom a).symm42 _ = inner ℂ (e ξ) (e (ρ a ξ)) := (e.inner_map_map ξ (ρ a ξ)).symm43 _ = inner ℂ (tracialVector family)44 (tracialRepresentation family a (tracialVector family)) := by45 have hcoe (y : f.GNS) :46 (e : f.GNS →L[ℂ] TracialHilbertSpace family) y = e y := rfl47 have h := congrArg (fun T : f.GNS →L[ℂ] TracialHilbertSpace family ↦ T ξ) (he a)48 simpa only [ContinuousLinearMap.comp_apply, hcoe, heξ] using49 congrArg (fun y ↦ inner ℂ (e ξ) y) h50 _ = traceExtension family a := inner_tracialVector_tracialRepresentation family a5152/-- 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 := by57 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φ.26162end MathlibAnnex.CStarAlgebra.CAR