Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/AtomicModel.lean
Pinned GitHub source · Raw UTF-8 source
Back to Realizing a shell family by a faithful irreducible operator algebra
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.AtomicSource2import MathlibAnnex.Analysis.CStarAlgebra.Representation.ShellReconstruction34/-!5# The completed CAR atomic shell model67This file discharges the representation-local shell hypotheses of the generic8atomic construction using the actual completed CAR algebra. The only9remaining input is `KishimotoOzawaSakaiProperty`; in particular, rank-one limiting defects and10capture conclusions are not fields of a source-data structure.11-/1213set_option autoImplicit false14set_option maxHeartbeats 12000001516noncomputable section1718open Filter Topology19open scoped ComplexOrder ENNReal lp InnerProduct2021namespace MathlibAnnex.CStarAlgebra.CAR2223open MathlibAnnex.Analysis.CStarAlgebra24open MathlibAnnex.Analysis.InnerProductSpace2526/-- The displayed arbitrary-index direct sum of all selected pure GNS27representations of the completed CAR algebra. -/28noncomputable def selectedAtomicRepresentation :29 Representation Limit30 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState) :=31 atomicRepresentation32 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState)3334/-- The literal root summand is faithful; this is inherited from the actual35completed CAR root GNS representation, not from simplicity of a future36target. -/37theorem selectedRootRepresentation_injective :38 Function.Injective39 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState40 completedRootPureState.classOf) := by41 exact (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState42 completedRootPureState.classOf).toRingHom.injective4344/-- The displayed atomic source representation is faithful because it45contains the faithful literal root summand. -/46theorem selectedAtomicRepresentation_injective :47 Function.Injective selectedAtomicRepresentation := by48 exact atomicRepresentation_injective_of_component49 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState)50 completedRootPureState.classOf selectedRootRepresentation_injective5152/-- 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)).range5758/-- The common represented final (root) flag. -/59noncomputable def representedRootFlag (n : ℕ) :60 Submodule ℂ (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState) :=61 (selectedAtomicRepresentation (rootFlag n)).range6263noncomputable instance instHasOrthogonalProjectionRepresentedInitialFlag64 (family : RepresentativeShellFamily) (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (n : ℕ) :65 (representedInitialFlag family i n).HasOrthogonalProjection :=66 (isStarProjection_iff_eq_starProjection_range.mp67 (IsStarProjection.map_representation selectedAtomicRepresentation68 (isStarProjection_transportedFlag family i n))).choose6970theorem selectedAtomicRepresentation_transportedFlag_eq_starProjection71 (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.mp75 (IsStarProjection.map_representation selectedAtomicRepresentation76 (isStarProjection_transportedFlag family i n))).choose_spec7778noncomputable instance instHasOrthogonalProjectionRepresentedRootFlag (n : ℕ) :79 (representedRootFlag n).HasOrthogonalProjection :=80 (isStarProjection_iff_eq_starProjection_range.mp81 (IsStarProjection.map_representation selectedAtomicRepresentation82 (isStarProjection_rootFlag n))).choose8384theorem selectedAtomicRepresentation_rootFlag_eq_starProjection (n : ℕ) :85 selectedAtomicRepresentation (rootFlag n) =86 (representedRootFlag n).starProjection :=87 (isStarProjection_iff_eq_starProjection_range.mp88 (IsStarProjection.map_representation selectedAtomicRepresentation89 (isStarProjection_rootFlag n))).choose_spec9091/-- A named final flag family. Its state index is deliberately retained so92the generic arbitrary-index construction can use it without changing the93common 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 n9899noncomputable instance instHasOrthogonalProjectionRepresentedFinalFlag100 (family : RepresentativeShellFamily) (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (n : ℕ) :101 (representedFinalFlag family i n).HasOrthogonalProjection := by102 change (representedRootFlag n).HasOrthogonalProjection103 infer_instance104105noncomputable instance instHasOrthogonalProjectionIInfRepresentedInitialFlag106 (family : RepresentativeShellFamily) (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) :107 (⨅ n, representedInitialFlag family i n).HasOrthogonalProjection := by108 have hspan :109 (⨅ n, representedInitialFlag family i n) =110 ℂ ∙ MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i111 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i) := by112 simpa [representedInitialFlag, selectedAtomicRepresentation] using113 (iInf_range_atomic_transportedFlag_eq_span family i)114 rw [hspan]115 infer_instance116117noncomputable instance instHasOrthogonalProjectionIInfRepresentedFinalFlag118 (family : RepresentativeShellFamily) (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) :119 (⨅ n, representedFinalFlag family i n).HasOrthogonalProjection := by120 have hspan :121 (⨅ n, representedFinalFlag family i n) =122 ℂ ∙ MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState123 completedRootPureState.classOf124 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState125 completedRootPureState.classOf) := by126 simpa [representedFinalFlag, representedRootFlag,127 selectedAtomicRepresentation] using128 (iInf_range_atomic_transportedFlag_eq_span family129 completedRootPureState.classOf)130 rw [hspan]131 infer_instance132133/-- The represented algebraic link between one transported difference shell134and 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)140141/-- Actual completed-CAR source data produces a faithful irreducible concrete142atomic model. All projection flags, support identities, and rank-one limiting143defects are supplied by proved CAR/GNS facts. At the distinguished root the144constructed generator is proved to be the identity from its action on every145difference 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 ∈ unitary151 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]152 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)) ∧153 (∀ i, L i (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i154 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) =155 MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState156 completedRootPureState.classOf157 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState158 completedRootPureState.classOf)) ∧159 (∀ i n, (L i).comp (selectedAtomicRepresentation160 (transportedFlag family i n - transportedFlag family i (n + 1))) =161 representedShellLink family i n) ∧162 L completedRootPureState.classOf = 1 ∧163 Function.Injective164 (MathlibAnnex.CStarAlgebra.AtomicConstruction.sourceHom selectedAtomicRepresentation L) ∧165 Representation.IsIrreducible166 (MathlibAnnex.CStarAlgebra.AtomicConstruction.ambientInclusion selectedAtomicRepresentation L) := by167 classical168 let U := representedInitialFlag family169 let V := representedFinalFlag family170 let W := representedShellLink family171 have hUproj (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (n : ℕ) :172 selectedAtomicRepresentation (transportedFlag family i n) =173 (U i n).starProjection := by174 exact selectedAtomicRepresentation_transportedFlag_eq_starProjection family i n175 have hVproj (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (n : ℕ) :176 selectedAtomicRepresentation (rootFlag n) = (V i n).starProjection :=177 by simpa [V, representedFinalFlag] using178 selectedAtomicRepresentation_rootFlag_eq_starProjection n179 have hUspan (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) :180 (⨅ n, U i n) =181 ℂ ∙ MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i182 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i) := by183 simpa [U, representedInitialFlag, selectedAtomicRepresentation] using184 (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 completedRootPureState188 completedRootPureState.classOf189 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState190 completedRootPureState.classOf) := by191 simpa [V, representedFinalFlag, representedRootFlag,192 selectedAtomicRepresentation] using193 (iInf_range_atomic_transportedFlag_eq_span family194 completedRootPureState.classOf)195 have hU : ∀ i, Antitone (U i) := by196 intro i m n hmn197 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) := by203 rw [← map_mul, transportedFlag_mul_of_le family i hmn]204 exact congrArg205 (fun T : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]206 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState ↦ T y) heq207 have hV : ∀ i, Antitone (V i) := by208 intro i m n hmn209 rintro x ⟨y, rfl⟩210 refine ⟨selectedAtomicRepresentation (rootFlag n) y, ?_⟩211 have heq : selectedAtomicRepresentation (rootFlag m) *212 selectedAtomicRepresentation (rootFlag n) =213 selectedAtomicRepresentation (rootFlag n) := by214 rw [← map_mul, rootFlag_mul_of_le hmn]215 exact congrArg216 (fun T : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]217 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState ↦ T y) heq218 have hU0 : ∀ i, U i 0 = ⊤ := by219 intro i220 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 = ⊤ := by224 intro i225 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 := by230 intro i n231 change star (selectedAtomicRepresentation232 ((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 rfl237 have hFinal : ∀ i n, (W i n).comp ((W i n)†) =238 Submodule.projectionShell (V i) n := by239 intro i n240 change selectedAtomicRepresentation241 ((representativeShellData family i).link n) *242 star (selectedAtomicRepresentation243 ((representativeShellData family i).link n)) = _244 rw [← map_star, ← map_mul, representativeLink_final, map_sub,245 hVproj i n, hVproj i (n + 1)]246 rfl247 have hUShell : ∀ i n,248 selectedAtomicRepresentation249 (transportedFlag family i n - transportedFlag family i (n + 1)) =250 Submodule.projectionShell (U i) n := by251 intro i n252 rw [map_sub, hUproj i n, hUproj i (n + 1)]253 rfl254 have hUinf : ∀ i, (⨅ n, U i n).starProjection =255 InnerProductSpace.rankOne ℂ256 (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i257 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i))258 (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i259 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) := by260 intro i261 apply starProjection_eq_rankOne_of_eq_span262 (⨅ n, U i n)263 (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i264 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i))265 simpa [MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding, norm_coordinateEmbedding] using266 MathlibAnnex.CStarAlgebra.PureState.norm_selectedVector completedRootPureState i267 exact hUspan i268 have hVinf : ∀ i, (⨅ n, V i n).starProjection =269 InnerProductSpace.rankOne ℂ270 (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState271 completedRootPureState.classOf272 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState273 completedRootPureState.classOf))274 (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState275 completedRootPureState.classOf276 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState277 completedRootPureState.classOf)) := by278 intro i279 apply starProjection_eq_rankOne_of_eq_span280 (⨅ n, V i n)281 (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState282 completedRootPureState.classOf283 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState284 completedRootPureState.classOf))285 simpa [MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding, norm_coordinateEmbedding] using286 MathlibAnnex.CStarAlgebra.PureState.norm_selectedVector completedRootPureState287 completedRootPureState.classOf288 exact hVspan i289 obtain ⟨L, hLunit, hLmap, hLterm, hLirr⟩ :=290 MathlibAnnex.CStarAlgebra.AtomicConstruction.exists_irreducible_pureAtomicShellModel291 completedRootPureState W U V hU hV hU0 hV0 hInitial hFinal hUinf hVinf292 have hLsource (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (n : ℕ) :293 (L i).comp (selectedAtomicRepresentation294 (transportedFlag family i n - transportedFlag family i (n + 1))) =295 representedShellLink family i n := by296 rw [hUShell i n]297 exact hLterm i n298 have hRootShell (n : ℕ) :299 representedShellLink family completedRootPureState.classOf n =300 Submodule.projectionShell (U completedRootPureState.classOf) n := by301 rw [Submodule.projectionShell, ← hUproj, ← hUproj]302 simp [W, U, representedShellLink, rootShell, map_sub]303 have hLroot : L completedRootPureState.classOf = 1 := by304 apply ContinuousLinearMap.eq_one_of_comp_projectionShell_eq_self_of_rankOne_iInf305 (L completedRootPureState.classOf) (U completedRootPureState.classOf)306 (hU completedRootPureState.classOf) (hU0 completedRootPureState.classOf)307 (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState308 completedRootPureState.classOf309 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState310 completedRootPureState.classOf))311 · simpa [MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding, norm_coordinateEmbedding] using312 MathlibAnnex.CStarAlgebra.PureState.norm_selectedVector completedRootPureState313 completedRootPureState.classOf314 · exact hUinf completedRootPureState.classOf315 · intro n316 rw [hLterm]317 change representedShellLink family completedRootPureState.classOf n =318 Submodule.projectionShell (U completedRootPureState.classOf) n319 exact hRootShell n320 · exact hLmap completedRootPureState.classOf321 exact ⟨L, hLunit, hLmap, hLsource, hLroot,322 MathlibAnnex.CStarAlgebra.AtomicConstruction.sourceHom_injective selectedAtomicRepresentation L323 selectedAtomicRepresentation_injective,324 hLirr⟩325326end MathlibAnnex.CStarAlgebra.CAR