Exact source view. Private integrated preview.
Exact declaration: MathlibAnnex.CStarAlgebra.CAR.traceModelRepresentation_injective
MathlibAnnex/Analysis/CStarAlgebra/CAR/TraceGNSModel.lean · lines 130–133
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.TracialRepresentation 2import MathlibAnnex.Analysis.CStarAlgebra.CAR.TracialTransport 3 4/-! 5# The target on the ordinary CAR trace GNS space 6 7The Hilbert space here is constructed from CAR alone and is independent of 8the shell-family parameter. The target is unchanged. Its representation is 9transported along a proved pointed source-cyclic unitary equivalence. 10-/ 11 12set_option autoImplicit false 13 14open Filter Topology 15open scoped InnerProduct 16 17namespace MathlibAnnex.CStarAlgebra.CAR 18 19open MathlibAnnex.Analysis.CStarAlgebra 20 21/-- The ordinary Hilbert space `L²(CAR, trace)`. -/ 22abbrev TraceHilbertSpace := tracePositive.GNS 23 24/-- The canonical vector in the CAR trace GNS space. -/ 25noncomputable def traceVector : TraceHilbertSpace := tracePositive.gnsCyclicVector 26 27/-- The ordinary CAR trace representation. -/ 28noncomputable def traceRepresentation : Representation Limit TraceHilbertSpace := 29 tracePositive.gnsStarAlgHom 30 31@[simp] 32theorem norm_traceVector : ‖traceVector‖ = 1 := 33 tracePositive.norm_gnsCyclicVector tracePositive_one 34 35theorem traceVector_ne_zero : traceVector ≠ 0 := by 36 intro hzero 37 have h := norm_traceVector 38 rw [hzero, norm_zero] at h 39 exact zero_ne_one h 40 41/-- Nontriviality is witnessed by the normalized CAR trace vector. -/ 42theorem nontrivial_traceHilbertSpace : Nontrivial TraceHilbertSpace := 43 nontrivial_of_ne traceVector 0 traceVector_ne_zero 44 45@[simp] 46theorem inner_traceVector_traceRepresentation (b : Limit) : 47 inner ℂ traceVector (traceRepresentation b traceVector) = trace b := 48 tracePositive.inner_gnsCyclicVector_gnsStarAlgHom b 49 50theorem denseRange_traceRepresentation_orbit : 51 DenseRange (fun b ↦ traceRepresentation b traceVector) := 52 tracePositive.denseRange_gnsStarAlgHom_apply_gnsCyclicVector 53 54theorem separableSpace_traceHilbertSpace : TopologicalSpace.SeparableSpace TraceHilbertSpace := 55 denseRange_traceRepresentation_orbit.separableSpace 56 (((ContinuousLinearMap.apply ℂ TraceHilbertSpace traceVector).comp 57 (Representation.continuousLinearMap traceRepresentation)).continuous) 58 59set_option maxHeartbeats 5000000 in 60/-- The target-state GNS and CAR-trace GNS have the same dense pointed source 61orbit, 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).comp 66 (traceRepresentation b) = 67 (tracialRepresentation family (shellFamilySourceHom family b)).comp 68 (e : TraceHilbertSpace →L[ℂ] TracialHilbertSpace family) := by 69 let σ : Representation Limit (TracialHilbertSpace family) := 70 (tracialRepresentation family).comp (shellFamilySourceHom family) 71 have hσ : DenseRange (StarAlgHom.orbitMap σ (tracialVector family)) := by 72 exact denseRange_tracialRepresentation_source_orbit family 73 have hstate (b : Limit) : 74 inner ℂ traceVector (traceRepresentation b traceVector) = 75 inner ℂ (tracialVector family) (σ b (tracialVector family)) := by 76 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_pointedCyclicTransport 82 traceRepresentation σ 83 traceVector (tracialVector family) denseRange_traceRepresentation_orbit 84 hσ hstate 85 exact ⟨e, he.2.1, he.2.2⟩ 86 87/-- 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) 91 92@[simp] 93theorem traceGNSUnitary_traceVector (family : RepresentativeShellFamily) : 94 traceGNSUnitary family traceVector = tracialVector family := 95 (Classical.choose_spec (exists_linearIsometryEquiv_traceHilbertSpace family)).1 96 97theorem traceGNSUnitary_comp_traceRepresentation (family : RepresentativeShellFamily) (b : Limit) : 98 (traceGNSUnitary family : TraceHilbertSpace →L[ℂ] TracialHilbertSpace family).comp 99 (traceRepresentation b) = 100 (tracialRepresentation family (shellFamilySourceHom family b)).comp 101 (traceGNSUnitary family : TraceHilbertSpace →L[ℂ] TracialHilbertSpace family) := 102 (Classical.choose_spec (exists_linearIsometryEquiv_traceHilbertSpace family)).2 b 103 104/-- 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.comp 108 (tracialRepresentation family) 109 110@[simp] 111theorem traceModelRepresentation_apply (family : RepresentativeShellFamily) 112 (a : ShellFamilyTarget family) (x : TraceHilbertSpace) : 113 traceModelRepresentation family a x = (traceGNSUnitary family).symm 114 (tracialRepresentation family a (traceGNSUnitary family x)) := rfl 115 116set_option maxHeartbeats 1000000 in 117@[simp] 118theorem traceModelRepresentation_shellFamilySourceHom (family : RepresentativeShellFamily) (b : Limit) : 119 traceModelRepresentation family (shellFamilySourceHom family b) = traceRepresentation b := by 120 ext x 121 apply (traceGNSUnitary family).injective 122 rw [traceModelRepresentation_apply, LinearIsometryEquiv.apply_symm_apply] 123 have hcoe (y : TraceHilbertSpace) : 124 (traceGNSUnitary family : TraceHilbertSpace →L[ℂ] TracialHilbertSpace family) y = 125 traceGNSUnitary family y := rfl 126 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.symm 129 130theorem traceModelRepresentation_injective (family : RepresentativeShellFamily) : 131 Function.Injective (traceModelRepresentation family) := 132 (traceGNSUnitary family).symm.conjStarAlgEquiv.injective.comp 133 (tracialRepresentation_injective family) 134 135theorem 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)) 140 141@[simp] 142theorem inner_traceVector_traceModelRepresentation (family : RepresentativeShellFamily) 143 (a : ShellFamilyTarget family) : 144 inner ℂ traceVector (traceModelRepresentation family a traceVector) = 145 traceExtension family a := by 146 rw [← (traceGNSUnitary family).inner_map_map traceVector 147 (traceModelRepresentation family a traceVector)] 148 simp only [traceModelRepresentation_apply, LinearIsometryEquiv.apply_symm_apply, 149 traceGNSUnitary_traceVector, inner_tracialVector_tracialRepresentation] 150 151theorem denseRange_traceModelRepresentation_orbit (family : RepresentativeShellFamily) : 152 DenseRange (fun a ↦ traceModelRepresentation family a traceVector) := by 153 have hsource : DenseRange (fun b ↦ traceModelRepresentation family 154 (shellFamilySourceHom family b) traceVector) := by 155 simpa only [traceModelRepresentation_shellFamilySourceHom] using denseRange_traceRepresentation_orbit 156 exact hsource.mono (by 157 rintro _ ⟨b, rfl⟩ 158 exact ⟨shellFamilySourceHom family b, rfl⟩) 159 160/-- The strong-sum limit is an actual unitary on the CAR trace Hilbert 161space, with both unitary identities inherited through the representation. -/ 162theorem traceModelRepresentation_shellFamilyGenerator_mem_unitary 163 (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) 168 169@[simp] 170theorem traceModelRepresentation_shellFamilyGenerator_root 171 (family : RepresentativeShellFamily) : 172 traceModelRepresentation family 173 (shellFamilyGenerator family completedRootPureState.classOf) = 1 := by 174 rw [shellFamilyGenerator_root, map_one] 175 176/-- The R51 shell-sum formula holds in the literal CAR trace GNS model, for 177the same links that define the already existing atomic target. -/ 178theorem stronglyConverges_traceRepresentation_shell_sums 179 (family : RepresentativeShellFamily) 180 (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : 181 ContinuousLinearMap.StronglyConverges 182 (ContinuousLinearMap.partialSum 183 (fun n ↦ traceRepresentation ((representativeShellData family i).link n))) 184 atTop (traceModelRepresentation family (shellFamilyGenerator family i)) ∧ 185 ContinuousLinearMap.StronglyConverges 186 (ContinuousLinearMap.partialSum 187 (fun n ↦ (traceRepresentation ((representativeShellData family i).link n))†)) 188 atTop ((traceModelRepresentation family (shellFamilyGenerator family i))†) := by 189 have htrace (b : Limit) : Representation.vectorFunctional 190 ((traceModelRepresentation family).comp (shellFamilySourceHom family)) traceVector b = 191 trace b := by 192 change inner ℂ traceVector 193 (traceModelRepresentation family (shellFamilySourceHom family b) traceVector) = trace b 194 rw [traceModelRepresentation_shellFamilySourceHom, inner_traceVector_traceRepresentation] 195 simpa only [traceModelRepresentation_shellFamilySourceHom] using 196 stronglyConverges_shell_sums_of_trace_of_cyclic family (traceModelRepresentation family) 197 traceVector htrace (denseRange_traceModelRepresentation_orbit family) i 198 199end MathlibAnnex.CStarAlgebra.CAR