Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/Capture.lean, lines 28–310.
Back to Every irreducible representation is unitarily equivalent to the inclusion · Back to The cyclic sum fills every irreducible target representation
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.CaptureRange 2 3/-! 4# Full target capture 5 6The surjective cyclic-sum isometry also intertwines the additional target 7generators. The proof compares the two independently constructed strong 8shell sums and then identifies the remaining rank-one corner from the 9selected-vector transport. No arbitrary representation is asked to preserve 10the source strong-operator limits. 11-/ 12 13set_option autoImplicit false 14set_option maxHeartbeats 1800000 15 16noncomputable section 17 18open Filter Topology 19open scoped ComplexOrder ENNReal lp InnerProduct 20 21namespace MathlibAnnex.CStarAlgebra.CAR 22 23open MathlibAnnex.Analysis.CStarAlgebra 24open MathlibAnnex.Analysis.InnerProductSpace 25 26universe v 27 28/-- The displayed actual completed-CAR atomic target captures every 29irreducible representation on an arbitrary target Hilbert universe. -/ 30theorem ambientInclusion_unitaryEquivalent 31 (family : RepresentativeShellFamily) 32 (L : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit → 33 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] 34 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState) 35 (hLunit : ∀ i, L i ∈ unitary 36 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] 37 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)) 38 (hLmap : ∀ i, L i 39 (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i 40 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) = 41 MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState 42 completedRootPureState.classOf 43 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState 44 completedRootPureState.classOf)) 45 (hLsource : ∀ i n, (L i).comp (selectedAtomicRepresentation 46 (transportedFlag family i n - transportedFlag family i (n + 1))) = 47 representedShellLink family i n) 48 (hLroot : L completedRootPureState.classOf = 1) 49 {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] 50 [CompleteSpace K] (rho : Representation (AtomicTarget L) K) 51 (hrho : rho.IsIrreducible) : 52 (MathlibAnnex.CStarAlgebra.AtomicConstruction.ambientInclusion selectedAtomicRepresentation L).UnitaryEquivalent 53 rho := by 54 classical 55 let sigma := restrictedRepresentation L rho 56 obtain ⟨eta_o, eta, W, hWsurj, heta_o_norm, heta_norm, hWpoint, 57 heta_gen, hWsource⟩ := 58 exists_surjective_selectedAtomicCyclicIsometry 59 family L hLunit hLsource hLroot rho hrho 60 let E : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState ≃ₗᵢ[ℂ] K := 61 LinearIsometryEquiv.ofSurjective W hWsurj 62 have hEsource (a : Limit) : 63 (E : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K).comp 64 (selectedAtomicRepresentation a) = 65 (sigma a).comp 66 (E : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K) := by 67 change W.toContinuousLinearMap.comp (selectedAtomicRepresentation a) = 68 (restrictedRepresentation L rho a).comp W.toContinuousLinearMap 69 exact hWsource a 70 have hEpoint (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : 71 E (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i 72 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) = eta i := by 73 simpa [E] using hWpoint i 74 have htargetRoot : MathlibAnnex.CStarAlgebra.AtomicConstruction.generator selectedAtomicRepresentation L 75 completedRootPureState.classOf = 76 MathlibAnnex.CStarAlgebra.AtomicConstruction.sourceHom selectedAtomicRepresentation L 1 := by 77 apply Subtype.ext 78 simpa using hLroot 79 have hrootGenerator : 80 ((Unitary.linearIsometryEquiv 81 (representedGeneratorUnitary L hLunit rho 82 completedRootPureState.classOf) : K ≃ₗᵢ[ℂ] K) : K →L[ℂ] K) = 1 := by 83 change rho (MathlibAnnex.CStarAlgebra.AtomicConstruction.generator selectedAtomicRepresentation L 84 completedRootPureState.classOf) = 1 85 rw [htargetRoot, map_one] 86 exact map_one rho 87 have heta_root : eta completedRootPureState.classOf = eta_o := by 88 have h := heta_gen completedRootPureState.classOf 89 change (((Unitary.linearIsometryEquiv 90 (representedGeneratorUnitary L hLunit rho 91 completedRootPureState.classOf) : K ≃ₗᵢ[ℂ] K) : K →L[ℂ] K) 92 (eta completedRootPureState.classOf)) = eta_o at h 93 rw [hrootGenerator] at h 94 simpa using h 95 refine ⟨E, ?_⟩ 96 intro a 97 have hsourceGenerator (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (x : 98 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState) : 99 E (L i x) = 100 rho (MathlibAnnex.CStarAlgebra.AtomicConstruction.generator selectedAtomicRepresentation L i) (E x) := by 101 let rho₀ := MathlibAnnex.CStarAlgebra.AtomicConstruction.ambientInclusion selectedAtomicRepresentation L 102 let w := (representativeShellData family i).link 103 obtain ⟨S₀, T₀, P₀, Q₀, R₀, hS₀, hT₀, -, -, hAdj₀, 104 hP₀proj, hP₀range, hQ₀proj, hQ₀range, -, -, hgenerator₀, 105 hR₀, -, -, -, -⟩ := 106 exists_targetShellReconstruction family L hLunit hLsource rho₀ i 107 obtain ⟨S, T, P, Q, R, hS, hT, -, -, hAdj, 108 hPproj, hPrange, hQproj, hQrange, -, -, hgenerator, 109 hR, -, -, -, -⟩ := 110 exists_targetShellReconstruction family L hLunit hLsource rho i 111 have hrepresented₀ : 112 (((Unitary.linearIsometryEquiv 113 (representedGeneratorUnitary L hLunit rho₀ i) : 114 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState ≃ₗᵢ[ℂ] 115 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState) : 116 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] 117 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)) = L i := by 118 rfl 119 rw [hrepresented₀] at hgenerator₀ hR₀ 120 have hS₀' : ContinuousLinearMap.StronglyConverges 121 (ContinuousLinearMap.partialSum 122 (fun n ↦ selectedAtomicRepresentation (w n))) atTop S₀ := by 123 change ContinuousLinearMap.StronglyConverges 124 (ContinuousLinearMap.partialSum 125 (fun n ↦ selectedAtomicRepresentation 126 ((representativeShellData family i).link n))) atTop S₀ at hS₀ 127 simpa [w] using hS₀ 128 have hS' : ContinuousLinearMap.StronglyConverges 129 (ContinuousLinearMap.partialSum (fun n ↦ sigma (w n))) atTop S := by 130 simpa [w] using hS 131 have hpartial (N : ℕ) : 132 (E : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K).comp 133 (ContinuousLinearMap.partialSum 134 (fun n ↦ selectedAtomicRepresentation (w n)) N) = 135 (ContinuousLinearMap.partialSum (fun n ↦ sigma (w n)) N).comp 136 (E : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K) := by 137 apply ContinuousLinearMap.ext 138 intro y 139 rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.comp_apply, 140 ContinuousLinearMap.partialSum_apply, 141 ContinuousLinearMap.partialSum_apply, map_sum] 142 apply Finset.sum_congr rfl 143 intro n hn 144 have h := congrArg 145 (fun A : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K ↦ 146 A y) (hEsource (w n)) 147 simpa [ContinuousLinearMap.comp_apply] using h 148 have hSintertwines : 149 (E : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K).comp S₀ = 150 S.comp (E : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K) := 151 ContinuousLinearMap.intertwines_strongLimits 152 (E : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K) 153 (E : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K) 154 hS₀' hS' hpartial 155 have hP₀range' : P₀.range = 156 ⨅ n, (selectedAtomicRepresentation (transportedFlag family i n)).range := by 157 change P₀.range = 158 ⨅ n, (selectedAtomicRepresentation (transportedFlag family i n)).range at hP₀range 159 exact hP₀range 160 have hP₀eq : P₀ = commonFixedProjection 161 (fun n ↦ selectedAtomicRepresentation (transportedFlag family i n)) := by 162 exact starProjection_eq_commonFixedProjection_of_range_iInf 163 selectedAtomicRepresentation (transportedFlag family i) 164 (isStarProjection_transportedFlag family i) P₀ hP₀proj hP₀range' 165 have hPeq : P = commonFixedProjection 166 (fun n ↦ sigma (transportedFlag family i n)) := by 167 exact starProjection_eq_commonFixedProjection_of_range_iInf sigma 168 (transportedFlag family i) (isStarProjection_transportedFlag family i) 169 P hPproj hPrange 170 let F₀ : Submodule ℂ 171 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState) := 172 commonFixedSubspace 173 (fun n ↦ selectedAtomicRepresentation (transportedFlag family i n)) 174 let F : Submodule ℂ K := 175 commonFixedSubspace (fun n ↦ sigma (transportedFlag family i n)) 176 have hFmap : F₀.map (E.toLinearEquiv : 177 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →ₗ[ℂ] K) = F := by 178 ext y 179 constructor 180 · rintro ⟨z, hz, rfl⟩ 181 change z ∈ commonFixedSubspace 182 (fun n ↦ selectedAtomicRepresentation (transportedFlag family i n)) at hz 183 rw [mem_commonFixedSubspace_iff] at hz 184 change E z ∈ commonFixedSubspace 185 (fun n ↦ sigma (transportedFlag family i n)) 186 rw [mem_commonFixedSubspace_iff] 187 intro n 188 have h := congrArg 189 (fun A : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K ↦ 190 A z) (hEsource (transportedFlag family i n)) 191 rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.comp_apply, 192 hz n] at h 193 exact h.symm 194 · intro hy 195 change y ∈ commonFixedSubspace 196 (fun n ↦ sigma (transportedFlag family i n)) at hy 197 rw [mem_commonFixedSubspace_iff] at hy 198 refine ⟨E.symm y, ?_, E.apply_symm_apply y⟩ 199 change E.symm y ∈ commonFixedSubspace 200 (fun n ↦ selectedAtomicRepresentation (transportedFlag family i n)) 201 rw [mem_commonFixedSubspace_iff] 202 intro n 203 apply E.injective 204 have h := congrArg 205 (fun A : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K ↦ 206 A (E.symm y)) (hEsource (transportedFlag family i n)) 207 change E (selectedAtomicRepresentation (transportedFlag family i n) 208 (E.symm y)) = sigma (transportedFlag family i n) (E (E.symm y)) at h 209 calc 210 E (selectedAtomicRepresentation (transportedFlag family i n) (E.symm y)) = 211 sigma (transportedFlag family i n) (E (E.symm y)) := h 212 _ = sigma (transportedFlag family i n) y := by rw [E.apply_symm_apply] 213 _ = y := hy n 214 _ = E (E.symm y) := (E.apply_symm_apply y).symm 215 have hPintertwines : 216 (E : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K).comp P₀ = 217 P.comp (E : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K) := by 218 apply ContinuousLinearMap.ext 219 intro y 220 rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.comp_apply, 221 hP₀eq, hPeq] 222 change E (F₀.starProjection y) = F.starProjection (E y) 223 symm 224 apply Submodule.eq_starProjection_of_mem_of_inner_eq_zero 225 · rw [← hFmap] 226 exact ⟨F₀.starProjection y, 227 Submodule.starProjection_apply_mem F₀ y, rfl⟩ 228 · intro z hz 229 rw [← hFmap] at hz 230 obtain ⟨z₀, hz₀, rfl⟩ := hz 231 rw [← E.map_sub] 232 change inner ℂ (E (y - F₀.starProjection y)) (E z₀) = 0 233 rw [E.inner_map_map] 234 exact F₀.starProjection_inner_eq_zero y z₀ hz₀ 235 have hF₀span : F₀ = 236 ℂ ∙ MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i 237 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i) := by 238 rw [show F₀ = ⨅ n, 239 (selectedAtomicRepresentation (transportedFlag family i n)).range by 240 exact commonFixedSubspace_eq_iInf_range selectedAtomicRepresentation 241 (transportedFlag family i) (isStarProjection_transportedFlag family i)] 242 simpa [selectedAtomicRepresentation] using 243 iInf_range_atomic_transportedFlag_eq_span family i 244 have hRintertwines : 245 (E : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K).comp R₀ = 246 R.comp (E : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K) := by 247 apply ContinuousLinearMap.ext 248 intro y 249 have hPmem : P₀ y ∈ F₀ := by 250 rw [hP₀eq] 251 exact commonFixedProjection_mem _ _ 252 rw [hF₀span] at hPmem 253 obtain ⟨c, hc⟩ := Submodule.mem_span_singleton.mp hPmem 254 have hleft : E (R₀ y) = c • eta_o := by 255 rw [hR₀, ContinuousLinearMap.comp_apply, ← hc, map_smul, 256 hLmap, map_smul, hEpoint, heta_root] 257 have hPpoint : P (E y) = c • eta i := by 258 have h := congrArg 259 (fun A : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K ↦ 260 A y) hPintertwines 261 change E (P₀ y) = P (E y) at h 262 rw [← hc, map_smul, hEpoint] at h 263 exact h.symm 264 have hright : R (E y) = c • eta_o := by 265 rw [hR, ContinuousLinearMap.comp_apply, hPpoint, map_smul] 266 have hgen_i : 267 (((Unitary.linearIsometryEquiv 268 (representedGeneratorUnitary L hLunit rho i) : K ≃ₗᵢ[ℂ] K) : 269 K →L[ℂ] K) (eta i)) = eta_o := heta_gen i 270 rw [hgen_i] 271 exact hleft.trans hright.symm 272 have hsourceDecomp : L i = S₀ + R₀ := by 273 simpa [rho₀] using hgenerator₀ 274 have htargetDecomp : 275 rho (MathlibAnnex.CStarAlgebra.AtomicConstruction.generator selectedAtomicRepresentation L i) = S + R := by 276 simpa using hgenerator 277 have hSpoint : E (S₀ x) = S (E x) := by 278 have h := congrArg 279 (fun A : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K ↦ 280 A x) hSintertwines 281 simpa [ContinuousLinearMap.comp_apply] using h 282 have hRpoint : E (R₀ x) = R (E x) := by 283 have h := congrArg 284 (fun A : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K ↦ 285 A x) hRintertwines 286 simpa [ContinuousLinearMap.comp_apply] using h 287 calc 288 E (L i x) = E ((S₀ + R₀) x) := by rw [hsourceDecomp] 289 _ = E (S₀ x) + E (R₀ x) := by simp 290 _ = S (E x) + R (E x) := by rw [hSpoint, hRpoint] 291 _ = (S + R) (E x) := rfl 292 _ = rho (MathlibAnnex.CStarAlgebra.AtomicConstruction.generator selectedAtomicRepresentation L i) (E x) := by 293 rw [htargetDecomp] 294 have hgeneratorAll (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : 295 (E : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K).comp 296 (L i) = 297 (rho (MathlibAnnex.CStarAlgebra.AtomicConstruction.generator selectedAtomicRepresentation L i)).comp 298 (E : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K) := by 299 apply ContinuousLinearMap.ext 300 intro x 301 exact hsourceGenerator i x 302 have hall := MathlibAnnex.CStarAlgebra.AtomicConstruction.intertwines_concreteTarget_of_generators 303 selectedAtomicRepresentation L E rho hEsource hgeneratorAll a 304 intro x 305 have h := congrArg 306 (fun A : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K ↦ 307 A x) hall 308 change E ((MathlibAnnex.CStarAlgebra.AtomicConstruction.ambientInclusion selectedAtomicRepresentation L a) x) = 309 rho a (E x) at h 310 exact h 311 312/-- Ordinary conditional endpoint: the actual completed-CAR construction 313removes every representation-local shell, defect, and capture hypothesis. 314Only the explicitly parameterized KOS statement remains. -/ 315theorem exists_completedAtomicTarget_uniqueIrreducibleModel 316 (family : RepresentativeShellFamily) : 317 ∃ L : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit → 318 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] 319 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState, 320 Representation.IsUniqueIrreducibleModel 321 (MathlibAnnex.CStarAlgebra.AtomicConstruction.ambientInclusion selectedAtomicRepresentation L) := by 322 obtain ⟨L, hLunit, hLmap, hLsource, hLroot, hsourceFaithful, hambientIrr⟩ := 323 exists_completedAtomicShellModel family 324 refine ⟨L, ?_, hambientIrr, ?_⟩ 325 · exact MathlibAnnex.CStarAlgebra.AtomicConstruction.ambientInclusion_injective selectedAtomicRepresentation L 326 · intro K _ _ _ rho hrho 327 exact ambientInclusion_unitaryEquivalent 328 family L hLunit hLmap hLsource hLroot rho hrho 329 330end MathlibAnnex.CStarAlgebra.CAR