Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/AtomicModel.lean, lines 34–42.
Back to Realizing a shell family by a faithful irreducible operator algebra
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.AtomicSource 2import MathlibAnnex.Analysis.CStarAlgebra.Representation.ShellReconstruction 3 4/-! 5# The completed CAR atomic shell model 6 7This file discharges the representation-local shell hypotheses of the generic 8atomic construction using the actual completed CAR algebra. The only 9remaining input is `KishimotoOzawaSakaiProperty`; in particular, rank-one limiting defects and 10capture conclusions are not fields of a source-data structure. 11-/ 12 13set_option autoImplicit false 14set_option maxHeartbeats 1200000 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 26/-- The displayed arbitrary-index direct sum of all selected pure GNS 27representations of the completed CAR algebra. -/ 28noncomputable def selectedAtomicRepresentation : 29 Representation Limit 30 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState) := 31 atomicRepresentation 32 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState) 33 34/-- The literal root summand is faithful; this is inherited from the actual 35completed CAR root GNS representation, not from simplicity of a future 36target. -/ 37theorem selectedRootRepresentation_injective : 38 Function.Injective 39 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState 40 completedRootPureState.classOf) := by 41 exact (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState 42 completedRootPureState.classOf).toRingHom.injective 43 44/-- The displayed atomic source representation is faithful because it 45contains the faithful literal root summand. -/ 46theorem selectedAtomicRepresentation_injective : 47 Function.Injective selectedAtomicRepresentation := by 48 exact atomicRepresentation_injective_of_component 49 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState) 50 completedRootPureState.classOf selectedRootRepresentation_injective 51 52/-- The represented initial flag for one selected state. -/ 53noncomputable def representedInitialFlag (family : RepresentativeShellFamily) 54 (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (n : ℕ) : 55 Submodule ℂ (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState) := 56 (selectedAtomicRepresentation (transportedFlag family i n)).range 57 58/-- The common represented final (root) flag. -/ 59noncomputable def representedRootFlag (n : ℕ) : 60 Submodule ℂ (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState) := 61 (selectedAtomicRepresentation (rootFlag n)).range 62 63noncomputable instance instHasOrthogonalProjectionRepresentedInitialFlag 64 (family : RepresentativeShellFamily) (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (n : ℕ) : 65 (representedInitialFlag family i n).HasOrthogonalProjection := 66 (isStarProjection_iff_eq_starProjection_range.mp 67 (IsStarProjection.map_representation selectedAtomicRepresentation 68 (isStarProjection_transportedFlag family i n))).choose 69 70theorem selectedAtomicRepresentation_transportedFlag_eq_starProjection 71 (family : RepresentativeShellFamily) (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (n : ℕ) : 72 selectedAtomicRepresentation (transportedFlag family i n) = 73 (representedInitialFlag family i n).starProjection := 74 (isStarProjection_iff_eq_starProjection_range.mp 75 (IsStarProjection.map_representation selectedAtomicRepresentation 76 (isStarProjection_transportedFlag family i n))).choose_spec 77 78noncomputable instance instHasOrthogonalProjectionRepresentedRootFlag (n : ℕ) : 79 (representedRootFlag n).HasOrthogonalProjection := 80 (isStarProjection_iff_eq_starProjection_range.mp 81 (IsStarProjection.map_representation selectedAtomicRepresentation 82 (isStarProjection_rootFlag n))).choose 83 84theorem selectedAtomicRepresentation_rootFlag_eq_starProjection (n : ℕ) : 85 selectedAtomicRepresentation (rootFlag n) = 86 (representedRootFlag n).starProjection := 87 (isStarProjection_iff_eq_starProjection_range.mp 88 (IsStarProjection.map_representation selectedAtomicRepresentation 89 (isStarProjection_rootFlag n))).choose_spec 90 91/-- A named final flag family. Its state index is deliberately retained so 92the generic arbitrary-index construction can use it without changing the 93common completed-CAR root flag. -/ 94noncomputable def representedFinalFlag (_family : RepresentativeShellFamily) 95 (_i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (n : ℕ) : 96 Submodule ℂ (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState) := 97 representedRootFlag n 98 99noncomputable instance instHasOrthogonalProjectionRepresentedFinalFlag 100 (family : RepresentativeShellFamily) (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (n : ℕ) : 101 (representedFinalFlag family i n).HasOrthogonalProjection := by 102 change (representedRootFlag n).HasOrthogonalProjection 103 infer_instance 104 105noncomputable instance instHasOrthogonalProjectionIInfRepresentedInitialFlag 106 (family : RepresentativeShellFamily) (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : 107 (⨅ n, representedInitialFlag family i n).HasOrthogonalProjection := by 108 have hspan : 109 (⨅ n, representedInitialFlag family i n) = 110 ℂ ∙ MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i 111 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i) := by 112 simpa [representedInitialFlag, selectedAtomicRepresentation] using 113 (iInf_range_atomic_transportedFlag_eq_span family i) 114 rw [hspan] 115 infer_instance 116 117noncomputable instance instHasOrthogonalProjectionIInfRepresentedFinalFlag 118 (family : RepresentativeShellFamily) (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : 119 (⨅ n, representedFinalFlag family i n).HasOrthogonalProjection := by 120 have hspan : 121 (⨅ n, representedFinalFlag family i n) = 122 ℂ ∙ MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState 123 completedRootPureState.classOf 124 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState 125 completedRootPureState.classOf) := by 126 simpa [representedFinalFlag, representedRootFlag, 127 selectedAtomicRepresentation] using 128 (iInf_range_atomic_transportedFlag_eq_span family 129 completedRootPureState.classOf) 130 rw [hspan] 131 infer_instance 132 133/-- The represented algebraic link between one transported difference shell 134and the corresponding root difference shell. -/ 135noncomputable def representedShellLink (family : RepresentativeShellFamily) 136 (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (n : ℕ) : 137 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] 138 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState := 139 selectedAtomicRepresentation ((representativeShellData family i).link n) 140 141/-- Actual completed-CAR source data produces a faithful irreducible concrete 142atomic model. All projection flags, support identities, and rank-one limiting 143defects are supplied by proved CAR/GNS facts. At the distinguished root the 144constructed generator is proved to be the identity from its action on every 145difference shell and on the rank-one limiting defect. -/ 146theorem exists_completedAtomicShellModel (family : RepresentativeShellFamily) : 147 ∃ L : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit → 148 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] 149 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState, 150 (∀ i, L i ∈ unitary 151 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] 152 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)) ∧ 153 (∀ i, L i (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i 154 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) = 155 MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState 156 completedRootPureState.classOf 157 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState 158 completedRootPureState.classOf)) ∧ 159 (∀ i n, (L i).comp (selectedAtomicRepresentation 160 (transportedFlag family i n - transportedFlag family i (n + 1))) = 161 representedShellLink family i n) ∧ 162 L completedRootPureState.classOf = 1 ∧ 163 Function.Injective 164 (MathlibAnnex.CStarAlgebra.AtomicConstruction.sourceHom selectedAtomicRepresentation L) ∧ 165 Representation.IsIrreducible 166 (MathlibAnnex.CStarAlgebra.AtomicConstruction.ambientInclusion selectedAtomicRepresentation L) := by 167 classical 168 let U := representedInitialFlag family 169 let V := representedFinalFlag family 170 let W := representedShellLink family 171 have hUproj (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (n : ℕ) : 172 selectedAtomicRepresentation (transportedFlag family i n) = 173 (U i n).starProjection := by 174 exact selectedAtomicRepresentation_transportedFlag_eq_starProjection family i n 175 have hVproj (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (n : ℕ) : 176 selectedAtomicRepresentation (rootFlag n) = (V i n).starProjection := 177 by simpa [V, representedFinalFlag] using 178 selectedAtomicRepresentation_rootFlag_eq_starProjection n 179 have hUspan (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : 180 (⨅ n, U i n) = 181 ℂ ∙ MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i 182 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i) := by 183 simpa [U, representedInitialFlag, selectedAtomicRepresentation] using 184 (iInf_range_atomic_transportedFlag_eq_span family i) 185 have hVspan (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : 186 (⨅ n, V i n) = 187 ℂ ∙ MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState 188 completedRootPureState.classOf 189 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState 190 completedRootPureState.classOf) := by 191 simpa [V, representedFinalFlag, representedRootFlag, 192 selectedAtomicRepresentation] using 193 (iInf_range_atomic_transportedFlag_eq_span family 194 completedRootPureState.classOf) 195 have hU : ∀ i, Antitone (U i) := by 196 intro i m n hmn 197 rintro x ⟨y, rfl⟩ 198 refine ⟨selectedAtomicRepresentation (transportedFlag family i n) y, ?_⟩ 199 have heq : 200 selectedAtomicRepresentation (transportedFlag family i m) * 201 selectedAtomicRepresentation (transportedFlag family i n) = 202 selectedAtomicRepresentation (transportedFlag family i n) := by 203 rw [← map_mul, transportedFlag_mul_of_le family i hmn] 204 exact congrArg 205 (fun T : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] 206 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState ↦ T y) heq 207 have hV : ∀ i, Antitone (V i) := by 208 intro i m n hmn 209 rintro x ⟨y, rfl⟩ 210 refine ⟨selectedAtomicRepresentation (rootFlag n) y, ?_⟩ 211 have heq : selectedAtomicRepresentation (rootFlag m) * 212 selectedAtomicRepresentation (rootFlag n) = 213 selectedAtomicRepresentation (rootFlag n) := by 214 rw [← map_mul, rootFlag_mul_of_le hmn] 215 exact congrArg 216 (fun T : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] 217 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState ↦ T y) heq 218 have hU0 : ∀ i, U i 0 = ⊤ := by 219 intro i 220 rw [← Submodule.range_starProjection (U i 0), ← hUproj i 0, 221 transportedFlag_zero, map_one] 222 exact LinearMap.range_eq_top.mpr fun x ↦ ⟨x, rfl⟩ 223 have hV0 : ∀ i, V i 0 = ⊤ := by 224 intro i 225 rw [← Submodule.range_starProjection (V i 0), ← hVproj i 0, 226 rootFlag_zero, map_one] 227 exact LinearMap.range_eq_top.mpr fun x ↦ ⟨x, rfl⟩ 228 have hInitial : ∀ i n, ((W i n)†).comp (W i n) = 229 Submodule.projectionShell (U i) n := by 230 intro i n 231 change star (selectedAtomicRepresentation 232 ((representativeShellData family i).link n)) * 233 selectedAtomicRepresentation ((representativeShellData family i).link n) = _ 234 rw [← map_star, ← map_mul, representativeLink_initial, map_sub, 235 hUproj i n, hUproj i (n + 1)] 236 rfl 237 have hFinal : ∀ i n, (W i n).comp ((W i n)†) = 238 Submodule.projectionShell (V i) n := by 239 intro i n 240 change selectedAtomicRepresentation 241 ((representativeShellData family i).link n) * 242 star (selectedAtomicRepresentation 243 ((representativeShellData family i).link n)) = _ 244 rw [← map_star, ← map_mul, representativeLink_final, map_sub, 245 hVproj i n, hVproj i (n + 1)] 246 rfl 247 have hUShell : ∀ i n, 248 selectedAtomicRepresentation 249 (transportedFlag family i n - transportedFlag family i (n + 1)) = 250 Submodule.projectionShell (U i) n := by 251 intro i n 252 rw [map_sub, hUproj i n, hUproj i (n + 1)] 253 rfl 254 have hUinf : ∀ i, (⨅ n, U i n).starProjection = 255 InnerProductSpace.rankOne ℂ 256 (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i 257 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) 258 (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i 259 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) := by 260 intro i 261 apply starProjection_eq_rankOne_of_eq_span 262 (⨅ n, U i n) 263 (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i 264 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) 265 simpa [MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding, norm_coordinateEmbedding] using 266 MathlibAnnex.CStarAlgebra.PureState.norm_selectedVector completedRootPureState i 267 exact hUspan i 268 have hVinf : ∀ i, (⨅ n, V i n).starProjection = 269 InnerProductSpace.rankOne ℂ 270 (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState 271 completedRootPureState.classOf 272 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState 273 completedRootPureState.classOf)) 274 (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState 275 completedRootPureState.classOf 276 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState 277 completedRootPureState.classOf)) := by 278 intro i 279 apply starProjection_eq_rankOne_of_eq_span 280 (⨅ n, V i n) 281 (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState 282 completedRootPureState.classOf 283 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState 284 completedRootPureState.classOf)) 285 simpa [MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding, norm_coordinateEmbedding] using 286 MathlibAnnex.CStarAlgebra.PureState.norm_selectedVector completedRootPureState 287 completedRootPureState.classOf 288 exact hVspan i 289 obtain ⟨L, hLunit, hLmap, hLterm, hLirr⟩ := 290 MathlibAnnex.CStarAlgebra.AtomicConstruction.exists_irreducible_pureAtomicShellModel 291 completedRootPureState W U V hU hV hU0 hV0 hInitial hFinal hUinf hVinf 292 have hLsource (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (n : ℕ) : 293 (L i).comp (selectedAtomicRepresentation 294 (transportedFlag family i n - transportedFlag family i (n + 1))) = 295 representedShellLink family i n := by 296 rw [hUShell i n] 297 exact hLterm i n 298 have hRootShell (n : ℕ) : 299 representedShellLink family completedRootPureState.classOf n = 300 Submodule.projectionShell (U completedRootPureState.classOf) n := by 301 rw [Submodule.projectionShell, ← hUproj, ← hUproj] 302 simp [W, U, representedShellLink, rootShell, map_sub] 303 have hLroot : L completedRootPureState.classOf = 1 := by 304 apply ContinuousLinearMap.eq_one_of_comp_projectionShell_eq_self_of_rankOne_iInf 305 (L completedRootPureState.classOf) (U completedRootPureState.classOf) 306 (hU completedRootPureState.classOf) (hU0 completedRootPureState.classOf) 307 (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState 308 completedRootPureState.classOf 309 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState 310 completedRootPureState.classOf)) 311 · simpa [MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding, norm_coordinateEmbedding] using 312 MathlibAnnex.CStarAlgebra.PureState.norm_selectedVector completedRootPureState 313 completedRootPureState.classOf 314 · exact hUinf completedRootPureState.classOf 315 · intro n 316 rw [hLterm] 317 change representedShellLink family completedRootPureState.classOf n = 318 Submodule.projectionShell (U completedRootPureState.classOf) n 319 exact hRootShell n 320 · exact hLmap completedRootPureState.classOf 321 exact ⟨L, hLunit, hLmap, hLsource, hLroot, 322 MathlibAnnex.CStarAlgebra.AtomicConstruction.sourceHom_injective selectedAtomicRepresentation L 323 selectedAtomicRepresentation_injective, 324 hLirr⟩ 325 326end MathlibAnnex.CStarAlgebra.CAR