Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/Capture.lean
Pinned GitHub source · Raw UTF-8 source
Back to Every irreducible representation is unitarily equivalent to the inclusion
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.CaptureRange23/-!4# Full target capture56The surjective cyclic-sum isometry also intertwines the additional target7generators. The proof compares the two independently constructed strong8shell sums and then identifies the remaining rank-one corner from the9selected-vector transport. No arbitrary representation is asked to preserve10the source strong-operator limits.11-/1213set_option autoImplicit false14set_option maxHeartbeats 18000001516noncomputable section1718open Filter Topology19open scoped ComplexOrder ENNReal lp InnerProduct2021namespace MathlibAnnex.CStarAlgebra.CAR2223open MathlibAnnex.Analysis.CStarAlgebra24open MathlibAnnex.Analysis.InnerProductSpace2526universe v2728/-- The displayed actual completed-CAR atomic target captures every29irreducible representation on an arbitrary target Hilbert universe. -/30theorem ambientInclusion_unitaryEquivalent31 (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 ∈ unitary36 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]37 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState))38 (hLmap : ∀ i, L i39 (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i40 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) =41 MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState42 completedRootPureState.classOf43 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState44 completedRootPureState.classOf))45 (hLsource : ∀ i n, (L i).comp (selectedAtomicRepresentation46 (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).UnitaryEquivalent53 rho := by54 classical55 let sigma := restrictedRepresentation L rho56 obtain ⟨eta_o, eta, W, hWsurj, heta_o_norm, heta_norm, hWpoint,57 heta_gen, hWsource⟩ :=58 exists_surjective_selectedAtomicCyclicIsometry59 family L hLunit hLsource hLroot rho hrho60 let E : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState ≃ₗᵢ[ℂ] K :=61 LinearIsometryEquiv.ofSurjective W hWsurj62 have hEsource (a : Limit) :63 (E : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K).comp64 (selectedAtomicRepresentation a) =65 (sigma a).comp66 (E : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K) := by67 change W.toContinuousLinearMap.comp (selectedAtomicRepresentation a) =68 (restrictedRepresentation L rho a).comp W.toContinuousLinearMap69 exact hWsource a70 have hEpoint (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) :71 E (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i72 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) = eta i := by73 simpa [E] using hWpoint i74 have htargetRoot : MathlibAnnex.CStarAlgebra.AtomicConstruction.generator selectedAtomicRepresentation L75 completedRootPureState.classOf =76 MathlibAnnex.CStarAlgebra.AtomicConstruction.sourceHom selectedAtomicRepresentation L 1 := by77 apply Subtype.ext78 simpa using hLroot79 have hrootGenerator :80 ((Unitary.linearIsometryEquiv81 (representedGeneratorUnitary L hLunit rho82 completedRootPureState.classOf) : K ≃ₗᵢ[ℂ] K) : K →L[ℂ] K) = 1 := by83 change rho (MathlibAnnex.CStarAlgebra.AtomicConstruction.generator selectedAtomicRepresentation L84 completedRootPureState.classOf) = 185 rw [htargetRoot, map_one]86 exact map_one rho87 have heta_root : eta completedRootPureState.classOf = eta_o := by88 have h := heta_gen completedRootPureState.classOf89 change (((Unitary.linearIsometryEquiv90 (representedGeneratorUnitary L hLunit rho91 completedRootPureState.classOf) : K ≃ₗᵢ[ℂ] K) : K →L[ℂ] K)92 (eta completedRootPureState.classOf)) = eta_o at h93 rw [hrootGenerator] at h94 simpa using h95 refine ⟨E, ?_⟩96 intro a97 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) := by101 let rho₀ := MathlibAnnex.CStarAlgebra.AtomicConstruction.ambientInclusion selectedAtomicRepresentation L102 let w := (representativeShellData family i).link103 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₀ i107 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 i111 have hrepresented₀ :112 (((Unitary.linearIsometryEquiv113 (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 := by118 rfl119 rw [hrepresented₀] at hgenerator₀ hR₀120 have hS₀' : ContinuousLinearMap.StronglyConverges121 (ContinuousLinearMap.partialSum122 (fun n ↦ selectedAtomicRepresentation (w n))) atTop S₀ := by123 change ContinuousLinearMap.StronglyConverges124 (ContinuousLinearMap.partialSum125 (fun n ↦ selectedAtomicRepresentation126 ((representativeShellData family i).link n))) atTop S₀ at hS₀127 simpa [w] using hS₀128 have hS' : ContinuousLinearMap.StronglyConverges129 (ContinuousLinearMap.partialSum (fun n ↦ sigma (w n))) atTop S := by130 simpa [w] using hS131 have hpartial (N : ℕ) :132 (E : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K).comp133 (ContinuousLinearMap.partialSum134 (fun n ↦ selectedAtomicRepresentation (w n)) N) =135 (ContinuousLinearMap.partialSum (fun n ↦ sigma (w n)) N).comp136 (E : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K) := by137 apply ContinuousLinearMap.ext138 intro y139 rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.comp_apply,140 ContinuousLinearMap.partialSum_apply,141 ContinuousLinearMap.partialSum_apply, map_sum]142 apply Finset.sum_congr rfl143 intro n hn144 have h := congrArg145 (fun A : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K ↦146 A y) (hEsource (w n))147 simpa [ContinuousLinearMap.comp_apply] using h148 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_strongLimits152 (E : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K)153 (E : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K)154 hS₀' hS' hpartial155 have hP₀range' : P₀.range =156 ⨅ n, (selectedAtomicRepresentation (transportedFlag family i n)).range := by157 change P₀.range =158 ⨅ n, (selectedAtomicRepresentation (transportedFlag family i n)).range at hP₀range159 exact hP₀range160 have hP₀eq : P₀ = commonFixedProjection161 (fun n ↦ selectedAtomicRepresentation (transportedFlag family i n)) := by162 exact starProjection_eq_commonFixedProjection_of_range_iInf163 selectedAtomicRepresentation (transportedFlag family i)164 (isStarProjection_transportedFlag family i) P₀ hP₀proj hP₀range'165 have hPeq : P = commonFixedProjection166 (fun n ↦ sigma (transportedFlag family i n)) := by167 exact starProjection_eq_commonFixedProjection_of_range_iInf sigma168 (transportedFlag family i) (isStarProjection_transportedFlag family i)169 P hPproj hPrange170 let F₀ : Submodule ℂ171 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState) :=172 commonFixedSubspace173 (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 := by178 ext y179 constructor180 · rintro ⟨z, hz, rfl⟩181 change z ∈ commonFixedSubspace182 (fun n ↦ selectedAtomicRepresentation (transportedFlag family i n)) at hz183 rw [mem_commonFixedSubspace_iff] at hz184 change E z ∈ commonFixedSubspace185 (fun n ↦ sigma (transportedFlag family i n))186 rw [mem_commonFixedSubspace_iff]187 intro n188 have h := congrArg189 (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 h193 exact h.symm194 · intro hy195 change y ∈ commonFixedSubspace196 (fun n ↦ sigma (transportedFlag family i n)) at hy197 rw [mem_commonFixedSubspace_iff] at hy198 refine ⟨E.symm y, ?_, E.apply_symm_apply y⟩199 change E.symm y ∈ commonFixedSubspace200 (fun n ↦ selectedAtomicRepresentation (transportedFlag family i n))201 rw [mem_commonFixedSubspace_iff]202 intro n203 apply E.injective204 have h := congrArg205 (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 h209 calc210 E (selectedAtomicRepresentation (transportedFlag family i n) (E.symm y)) =211 sigma (transportedFlag family i n) (E (E.symm y)) := h212 _ = sigma (transportedFlag family i n) y := by rw [E.apply_symm_apply]213 _ = y := hy n214 _ = E (E.symm y) := (E.apply_symm_apply y).symm215 have hPintertwines :216 (E : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K).comp P₀ =217 P.comp (E : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K) := by218 apply ContinuousLinearMap.ext219 intro y220 rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.comp_apply,221 hP₀eq, hPeq]222 change E (F₀.starProjection y) = F.starProjection (E y)223 symm224 apply Submodule.eq_starProjection_of_mem_of_inner_eq_zero225 · rw [← hFmap]226 exact ⟨F₀.starProjection y,227 Submodule.starProjection_apply_mem F₀ y, rfl⟩228 · intro z hz229 rw [← hFmap] at hz230 obtain ⟨z₀, hz₀, rfl⟩ := hz231 rw [← E.map_sub]232 change inner ℂ (E (y - F₀.starProjection y)) (E z₀) = 0233 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 i237 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i) := by238 rw [show F₀ = ⨅ n,239 (selectedAtomicRepresentation (transportedFlag family i n)).range by240 exact commonFixedSubspace_eq_iInf_range selectedAtomicRepresentation241 (transportedFlag family i) (isStarProjection_transportedFlag family i)]242 simpa [selectedAtomicRepresentation] using243 iInf_range_atomic_transportedFlag_eq_span family i244 have hRintertwines :245 (E : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K).comp R₀ =246 R.comp (E : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K) := by247 apply ContinuousLinearMap.ext248 intro y249 have hPmem : P₀ y ∈ F₀ := by250 rw [hP₀eq]251 exact commonFixedProjection_mem _ _252 rw [hF₀span] at hPmem253 obtain ⟨c, hc⟩ := Submodule.mem_span_singleton.mp hPmem254 have hleft : E (R₀ y) = c • eta_o := by255 rw [hR₀, ContinuousLinearMap.comp_apply, ← hc, map_smul,256 hLmap, map_smul, hEpoint, heta_root]257 have hPpoint : P (E y) = c • eta i := by258 have h := congrArg259 (fun A : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K ↦260 A y) hPintertwines261 change E (P₀ y) = P (E y) at h262 rw [← hc, map_smul, hEpoint] at h263 exact h.symm264 have hright : R (E y) = c • eta_o := by265 rw [hR, ContinuousLinearMap.comp_apply, hPpoint, map_smul]266 have hgen_i :267 (((Unitary.linearIsometryEquiv268 (representedGeneratorUnitary L hLunit rho i) : K ≃ₗᵢ[ℂ] K) :269 K →L[ℂ] K) (eta i)) = eta_o := heta_gen i270 rw [hgen_i]271 exact hleft.trans hright.symm272 have hsourceDecomp : L i = S₀ + R₀ := by273 simpa [rho₀] using hgenerator₀274 have htargetDecomp :275 rho (MathlibAnnex.CStarAlgebra.AtomicConstruction.generator selectedAtomicRepresentation L i) = S + R := by276 simpa using hgenerator277 have hSpoint : E (S₀ x) = S (E x) := by278 have h := congrArg279 (fun A : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K ↦280 A x) hSintertwines281 simpa [ContinuousLinearMap.comp_apply] using h282 have hRpoint : E (R₀ x) = R (E x) := by283 have h := congrArg284 (fun A : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K ↦285 A x) hRintertwines286 simpa [ContinuousLinearMap.comp_apply] using h287 calc288 E (L i x) = E ((S₀ + R₀) x) := by rw [hsourceDecomp]289 _ = E (S₀ x) + E (R₀ x) := by simp290 _ = S (E x) + R (E x) := by rw [hSpoint, hRpoint]291 _ = (S + R) (E x) := rfl292 _ = rho (MathlibAnnex.CStarAlgebra.AtomicConstruction.generator selectedAtomicRepresentation L i) (E x) := by293 rw [htargetDecomp]294 have hgeneratorAll (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) :295 (E : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K).comp296 (L i) =297 (rho (MathlibAnnex.CStarAlgebra.AtomicConstruction.generator selectedAtomicRepresentation L i)).comp298 (E : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K) := by299 apply ContinuousLinearMap.ext300 intro x301 exact hsourceGenerator i x302 have hall := MathlibAnnex.CStarAlgebra.AtomicConstruction.intertwines_concreteTarget_of_generators303 selectedAtomicRepresentation L E rho hEsource hgeneratorAll a304 intro x305 have h := congrArg306 (fun A : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K ↦307 A x) hall308 change E ((MathlibAnnex.CStarAlgebra.AtomicConstruction.ambientInclusion selectedAtomicRepresentation L a) x) =309 rho a (E x) at h310 exact h311312/-- Ordinary conditional endpoint: the actual completed-CAR construction313removes every representation-local shell, defect, and capture hypothesis.314Only the explicitly parameterized KOS statement remains. -/315theorem exists_completedAtomicTarget_uniqueIrreducibleModel316 (family : RepresentativeShellFamily) :317 ∃ L : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit →318 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]319 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState,320 Representation.IsUniqueIrreducibleModel321 (MathlibAnnex.CStarAlgebra.AtomicConstruction.ambientInclusion selectedAtomicRepresentation L) := by322 obtain ⟨L, hLunit, hLmap, hLsource, hLroot, hsourceFaithful, hambientIrr⟩ :=323 exists_completedAtomicShellModel family324 refine ⟨L, ?_, hambientIrr, ?_⟩325 · exact MathlibAnnex.CStarAlgebra.AtomicConstruction.ambientInclusion_injective selectedAtomicRepresentation L326 · intro K _ _ _ rho hrho327 exact ambientInclusion_unitaryEquivalent328 family L hLunit hLmap hLsource hLroot rho hrho329330end MathlibAnnex.CStarAlgebra.CAR