Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/TraceGNSModel.lean
Pinned GitHub source · Raw UTF-8 source
Back to The target represented on the CAR trace GNS space
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.TracialRepresentation2import MathlibAnnex.Analysis.CStarAlgebra.CAR.TracialTransport34/-!5# The target on the ordinary CAR trace GNS space67The Hilbert space here is constructed from CAR alone and is independent of8the shell-family parameter. The target is unchanged. Its representation is9transported along a proved pointed source-cyclic unitary equivalence.10-/1112set_option autoImplicit false1314open Filter Topology15open scoped InnerProduct1617namespace MathlibAnnex.CStarAlgebra.CAR1819open MathlibAnnex.Analysis.CStarAlgebra2021/-- The ordinary Hilbert space `L²(CAR, trace)`. -/22abbrev TraceHilbertSpace := tracePositive.GNS2324/-- The canonical vector in the CAR trace GNS space. -/25noncomputable def traceVector : TraceHilbertSpace := tracePositive.gnsCyclicVector2627/-- The ordinary CAR trace representation. -/28noncomputable def traceRepresentation : Representation Limit TraceHilbertSpace :=29 tracePositive.gnsStarAlgHom3031@[simp]32theorem norm_traceVector : ‖traceVector‖ = 1 :=33 tracePositive.norm_gnsCyclicVector tracePositive_one3435theorem traceVector_ne_zero : traceVector ≠ 0 := by36 intro hzero37 have h := norm_traceVector38 rw [hzero, norm_zero] at h39 exact zero_ne_one h4041/-- Nontriviality is witnessed by the normalized CAR trace vector. -/42theorem nontrivial_traceHilbertSpace : Nontrivial TraceHilbertSpace :=43 nontrivial_of_ne traceVector 0 traceVector_ne_zero4445@[simp]46theorem inner_traceVector_traceRepresentation (b : Limit) :47 inner ℂ traceVector (traceRepresentation b traceVector) = trace b :=48 tracePositive.inner_gnsCyclicVector_gnsStarAlgHom b4950theorem denseRange_traceRepresentation_orbit :51 DenseRange (fun b ↦ traceRepresentation b traceVector) :=52 tracePositive.denseRange_gnsStarAlgHom_apply_gnsCyclicVector5354theorem separableSpace_traceHilbertSpace : TopologicalSpace.SeparableSpace TraceHilbertSpace :=55 denseRange_traceRepresentation_orbit.separableSpace56 (((ContinuousLinearMap.apply ℂ TraceHilbertSpace traceVector).comp57 (Representation.continuousLinearMap traceRepresentation)).continuous)5859set_option maxHeartbeats 5000000 in60/-- The target-state GNS and CAR-trace GNS have the same dense pointed source61orbit, so a unitary between them exists without any dimension assumption. -/62theorem exists_linearIsometryEquiv_traceHilbertSpace (family : RepresentativeShellFamily) :63 ∃ e : TraceHilbertSpace ≃ₗᵢ[ℂ] TracialHilbertSpace family,64 e traceVector = tracialVector family ∧65 ∀ b, (e : TraceHilbertSpace →L[ℂ] TracialHilbertSpace family).comp66 (traceRepresentation b) =67 (tracialRepresentation family (shellFamilySourceHom family b)).comp68 (e : TraceHilbertSpace →L[ℂ] TracialHilbertSpace family) := by69 let σ : Representation Limit (TracialHilbertSpace family) :=70 (tracialRepresentation family).comp (shellFamilySourceHom family)71 have hσ : DenseRange (StarAlgHom.orbitMap σ (tracialVector family)) := by72 exact denseRange_tracialRepresentation_source_orbit family73 have hstate (b : Limit) :74 inner ℂ traceVector (traceRepresentation b traceVector) =75 inner ℂ (tracialVector family) (σ b (tracialVector family)) := by76 change inner ℂ traceVector (traceRepresentation b traceVector) =77 inner ℂ (tracialVector family)78 (tracialRepresentation family (shellFamilySourceHom family b) (tracialVector family))79 rw [inner_traceVector_traceRepresentation, inner_tracialVector_tracialRepresentation,80 traceExtension_shellFamilySourceHom]81 obtain ⟨e, he, _⟩ := StarAlgHom.existsUnique_pointedCyclicTransport82 traceRepresentation σ83 traceVector (tracialVector family) denseRange_traceRepresentation_orbit84 hσ hstate85 exact ⟨e, he.2.1, he.2.2⟩8687/-- The pointed unitary is fixed once for each already fixed shell family. -/88noncomputable def traceGNSUnitary (family : RepresentativeShellFamily) :89 TraceHilbertSpace ≃ₗᵢ[ℂ] TracialHilbertSpace family :=90 Classical.choose (exists_linearIsometryEquiv_traceHilbertSpace family)9192@[simp]93theorem traceGNSUnitary_traceVector (family : RepresentativeShellFamily) :94 traceGNSUnitary family traceVector = tracialVector family :=95 (Classical.choose_spec (exists_linearIsometryEquiv_traceHilbertSpace family)).19697theorem traceGNSUnitary_comp_traceRepresentation (family : RepresentativeShellFamily) (b : Limit) :98 (traceGNSUnitary family : TraceHilbertSpace →L[ℂ] TracialHilbertSpace family).comp99 (traceRepresentation b) =100 (tracialRepresentation family (shellFamilySourceHom family b)).comp101 (traceGNSUnitary family : TraceHilbertSpace →L[ℂ] TracialHilbertSpace family) :=102 (Classical.choose_spec (exists_linearIsometryEquiv_traceHilbertSpace family)).2 b103104/-- The same target now acts on the original CAR trace GNS space. -/105noncomputable def traceModelRepresentation (family : RepresentativeShellFamily) :106 Representation (ShellFamilyTarget family) TraceHilbertSpace :=107 (traceGNSUnitary family).symm.conjStarAlgEquiv.toStarAlgHom.comp108 (tracialRepresentation family)109110@[simp]111theorem traceModelRepresentation_apply (family : RepresentativeShellFamily)112 (a : ShellFamilyTarget family) (x : TraceHilbertSpace) :113 traceModelRepresentation family a x = (traceGNSUnitary family).symm114 (tracialRepresentation family a (traceGNSUnitary family x)) := rfl115116set_option maxHeartbeats 1000000 in117@[simp]118theorem traceModelRepresentation_shellFamilySourceHom (family : RepresentativeShellFamily) (b : Limit) :119 traceModelRepresentation family (shellFamilySourceHom family b) = traceRepresentation b := by120 ext x121 apply (traceGNSUnitary family).injective122 rw [traceModelRepresentation_apply, LinearIsometryEquiv.apply_symm_apply]123 have hcoe (y : TraceHilbertSpace) :124 (traceGNSUnitary family : TraceHilbertSpace →L[ℂ] TracialHilbertSpace family) y =125 traceGNSUnitary family y := rfl126 have h := congrArg (fun T : TraceHilbertSpace →L[ℂ] TracialHilbertSpace family ↦ T x)127 (traceGNSUnitary_comp_traceRepresentation family b)128 simpa only [ContinuousLinearMap.comp_apply, hcoe] using h.symm129130theorem traceModelRepresentation_injective (family : RepresentativeShellFamily) :131 Function.Injective (traceModelRepresentation family) :=132 (traceGNSUnitary family).symm.conjStarAlgEquiv.injective.comp133 (tracialRepresentation_injective family)134135theorem isometry_traceModelRepresentation (family : RepresentativeShellFamily) :136 Isometry (traceModelRepresentation family) :=137 AddMonoidHomClass.isometry_of_norm (traceModelRepresentation family)138 (NonUnitalStarAlgHom.norm_map (traceModelRepresentation family)139 (traceModelRepresentation_injective family))140141@[simp]142theorem inner_traceVector_traceModelRepresentation (family : RepresentativeShellFamily)143 (a : ShellFamilyTarget family) :144 inner ℂ traceVector (traceModelRepresentation family a traceVector) =145 traceExtension family a := by146 rw [← (traceGNSUnitary family).inner_map_map traceVector147 (traceModelRepresentation family a traceVector)]148 simp only [traceModelRepresentation_apply, LinearIsometryEquiv.apply_symm_apply,149 traceGNSUnitary_traceVector, inner_tracialVector_tracialRepresentation]150151theorem denseRange_traceModelRepresentation_orbit (family : RepresentativeShellFamily) :152 DenseRange (fun a ↦ traceModelRepresentation family a traceVector) := by153 have hsource : DenseRange (fun b ↦ traceModelRepresentation family154 (shellFamilySourceHom family b) traceVector) := by155 simpa only [traceModelRepresentation_shellFamilySourceHom] using denseRange_traceRepresentation_orbit156 exact hsource.mono (by157 rintro _ ⟨b, rfl⟩158 exact ⟨shellFamilySourceHom family b, rfl⟩)159160/-- The strong-sum limit is an actual unitary on the CAR trace Hilbert161space, with both unitary identities inherited through the representation. -/162theorem traceModelRepresentation_shellFamilyGenerator_mem_unitary163 (family : RepresentativeShellFamily)164 (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) :165 traceModelRepresentation family (shellFamilyGenerator family i) ∈166 unitary (TraceHilbertSpace →L[ℂ] TraceHilbertSpace) :=167 Unitary.map_mem (traceModelRepresentation family) (shellFamilyGenerator_mem_unitary family i)168169@[simp]170theorem traceModelRepresentation_shellFamilyGenerator_root171 (family : RepresentativeShellFamily) :172 traceModelRepresentation family173 (shellFamilyGenerator family completedRootPureState.classOf) = 1 := by174 rw [shellFamilyGenerator_root, map_one]175176/-- The R51 shell-sum formula holds in the literal CAR trace GNS model, for177the same links that define the already existing atomic target. -/178theorem stronglyConverges_traceRepresentation_shell_sums179 (family : RepresentativeShellFamily)180 (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) :181 ContinuousLinearMap.StronglyConverges182 (ContinuousLinearMap.partialSum183 (fun n ↦ traceRepresentation ((representativeShellData family i).link n)))184 atTop (traceModelRepresentation family (shellFamilyGenerator family i)) ∧185 ContinuousLinearMap.StronglyConverges186 (ContinuousLinearMap.partialSum187 (fun n ↦ (traceRepresentation ((representativeShellData family i).link n))†))188 atTop ((traceModelRepresentation family (shellFamilyGenerator family i))†) := by189 have htrace (b : Limit) : Representation.vectorFunctional190 ((traceModelRepresentation family).comp (shellFamilySourceHom family)) traceVector b =191 trace b := by192 change inner ℂ traceVector193 (traceModelRepresentation family (shellFamilySourceHom family b) traceVector) = trace b194 rw [traceModelRepresentation_shellFamilySourceHom, inner_traceVector_traceRepresentation]195 simpa only [traceModelRepresentation_shellFamilySourceHom] using196 stronglyConverges_shell_sums_of_trace_of_cyclic family (traceModelRepresentation family)197 traceVector htrace (denseRange_traceModelRepresentation_orbit family) i198199end MathlibAnnex.CStarAlgebra.CAR