Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/CaptureRange.lean
Pinned GitHub source · Raw UTF-8 source
Back to Every irreducible representation is unitarily equivalent to the inclusion · Back to Assembling selected GNS cyclic subspaces into an isometric source representation · Back to The cyclic sum fills every irreducible target representation · Back to A common root vector realizes every selected state through the generators
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.CyclicCapture2import MathlibAnnex.Analysis.CStarAlgebra.AtomicConstruction.GeneratedReduction3import MathlibAnnex.Analysis.InnerProductSpace.Reduction45/-!6# Surjectivity of the selected cyclic sum in an irreducible target78The selected pure-state cyclic pieces form a closed source-reducing subspace.9The represented completed-CAR shell reconstruction shows that this subspace10also reduces every additional target generator: the strong shell part reduces11it termwise, while the limiting corner is controlled by its initial and root12one-dimensional fixed lines. Irreducibility of the arbitrary target13representation then forces the cyclic sum to be the whole target Hilbert14space.15-/1617set_option autoImplicit false18set_option maxHeartbeats 16000001920noncomputable section2122open Filter Topology23open scoped ComplexOrder ENNReal lp InnerProduct2425namespace MathlibAnnex.CStarAlgebra.CAR2627open MathlibAnnex.Analysis.CStarAlgebra28open MathlibAnnex.Analysis.InnerProductSpace2930universe v3132/-- The arbitrary-index sum of the selected pure GNS cyclic copies is33surjective in every nonzero irreducible representation of the actual target.34The returned map still records its source intertwining law and its action on35all selected cyclic vectors. -/36theorem exists_surjective_selectedAtomicCyclicIsometry37 (family : RepresentativeShellFamily)38 (L : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit →39 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]40 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)41 (hLunit : ∀ i, L i ∈ unitary42 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]43 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState))44 (hLsource : ∀ i n, (L i).comp (selectedAtomicRepresentation45 (transportedFlag family i n - transportedFlag family i (n + 1))) =46 representedShellLink family i n)47 (hLroot : L completedRootPureState.classOf = 1)48 {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K]49 [CompleteSpace K] (rho : Representation (AtomicTarget L) K)50 (hrho : rho.IsIrreducible) :51 ∃ (eta_o : K) (eta : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit → K)52 (W : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →ₗᵢ[ℂ] K),53 Function.Surjective W ∧54 ‖eta_o‖ = 1 ∧55 (∀ i, ‖eta i‖ = 1) ∧56 (∀ i, W (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i57 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) = eta i) ∧58 (∀ i, (Unitary.linearIsometryEquiv59 (representedGeneratorUnitary L hLunit rho i) : K ≃ₗᵢ[ℂ] K)60 (eta i) = eta_o) ∧61 ∀ a,62 W.toContinuousLinearMap.comp (selectedAtomicRepresentation a) =63 ((restrictedRepresentation L rho) a).comp64 W.toContinuousLinearMap := by65 classical66 let sigma := restrictedRepresentation L rho67 obtain ⟨eta_o, eta, heta_o_norm, heta_o_fixed, heta_o_state, heta⟩ :=68 exists_targetDefectVectorFamily family L hLunit hLsource rho hrho69 have heta_norm : ∀ i, ‖eta i‖ = 1 := fun i ↦ (heta i).170 have heta_state : ∀ i, Representation.vectorFunctional sigma (eta i) =71 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1 :=72 fun i ↦ (heta i).2.2.273 have heta_gen : ∀ i, (Unitary.linearIsometryEquiv74 (representedGeneratorUnitary L hLunit rho i) : K ≃ₗᵢ[ℂ] K)75 (eta i) = eta_o := fun i ↦ (heta i).2.2.176 obtain ⟨W, hWcyclic, hWpoint, hWfixedSpan, hWsource⟩ :=77 exists_selectedAtomicCyclicIsometry family sigma eta heta_norm heta_state78 let M : Submodule ℂ K := LinearMap.range W.toLinearMap79 have hMclosed : IsClosed (M : Set K) := by80 change IsClosed (Set.range W)81 exact W.isometry.isClosedEmbedding.isClosed_range82 have hsourceReduces (a : Limit) : M.Reduces (sigma a) := by83 constructor84 · rintro _ ⟨x, rfl⟩85 refine ⟨selectedAtomicRepresentation a x, ?_⟩86 have h := congrArg87 (fun T : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K ↦88 T x) (hWsource a)89 simpa [ContinuousLinearMap.comp_apply] using h90 · rintro _ ⟨x, rfl⟩91 refine ⟨selectedAtomicRepresentation (star a) x, ?_⟩92 have h := congrArg93 (fun T : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K ↦94 T x) (hWsource (star a))95 simpa [ContinuousLinearMap.comp_apply, map_star,96 ContinuousLinearMap.star_eq_adjoint] using h97 have htargetRoot : MathlibAnnex.CStarAlgebra.AtomicConstruction.generator selectedAtomicRepresentation L98 completedRootPureState.classOf =99 MathlibAnnex.CStarAlgebra.AtomicConstruction.sourceHom selectedAtomicRepresentation L 1 := by100 apply Subtype.ext101 simpa using hLroot102 have hrootGenerator :103 ((Unitary.linearIsometryEquiv104 (representedGeneratorUnitary L hLunit rho105 completedRootPureState.classOf) : K ≃ₗᵢ[ℂ] K) : K →L[ℂ] K) = 1 := by106 change rho (MathlibAnnex.CStarAlgebra.AtomicConstruction.generator selectedAtomicRepresentation L107 completedRootPureState.classOf) = 1108 rw [htargetRoot, map_one]109 exact map_one rho110 have heta_root : eta completedRootPureState.classOf = eta_o := by111 have h := heta_gen completedRootPureState.classOf112 change (((Unitary.linearIsometryEquiv113 (representedGeneratorUnitary L hLunit rho114 completedRootPureState.classOf) : K ≃ₗᵢ[ℂ] K) : K →L[ℂ] K)115 (eta completedRootPureState.classOf)) = eta_o at h116 rw [hrootGenerator] at h117 simpa using h118 have hline_mem (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) {y : K}119 (hy : y ∈ (ℂ ∙ eta i : Submodule ℂ K)) : y ∈ M := by120 obtain ⟨c, hc⟩ := Submodule.mem_span_singleton.mp hy121 refine ⟨c • MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i122 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i), ?_⟩123 change W (c • MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i124 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) = y125 rw [map_smul, hWpoint]126 exact hc127 have hgeneratorReduces (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) :128 M.Reduces (rho (MathlibAnnex.CStarAlgebra.AtomicConstruction.generator selectedAtomicRepresentation L i)) := by129 obtain ⟨S, T, P, Q, R, hS, hT, -, -, hAdj, hPproj, hPrange,130 hQproj, hQrange, -, -, hgeneratorEq, hR, hRinitial, hRfinal,131 hRsupport, -⟩ :=132 exists_targetShellReconstruction family L hLunit hLsource rho i133 have hSreduces : M.Reduces S := by134 apply Submodule.Reduces.of_stronglyConverges_partialSum hMclosed135 (W := fun n ↦ sigma ((representativeShellData family i).link n))136 (T := T)137 · intro n138 exact hsourceReduces ((representativeShellData family i).link n)139 · exact hS140 · exact hT141 · exact hAdj142 have hPeq : P = commonFixedProjection143 (fun n ↦ sigma (transportedFlag family i n)) := by144 exact starProjection_eq_commonFixedProjection_of_range_iInf sigma145 (transportedFlag family i) (isStarProjection_transportedFlag family i)146 P hPproj hPrange147 have hQeq : Q = commonFixedProjection148 (fun n ↦ sigma (rootFlag n)) := by149 exact starProjection_eq_commonFixedProjection_of_range_iInf sigma150 rootFlag isStarProjection_rootFlag Q hQproj hQrange151 have hPinv : M.IsInvariantUnder P := by152 rintro _ ⟨x, rfl⟩153 rw [hPeq]154 exact hline_mem i (hWfixedSpan i x)155 have hQinv : M.IsInvariantUnder Q := by156 rintro _ ⟨x, rfl⟩157 rw [hQeq]158 have hspan : commonFixedProjection (fun n ↦ sigma (rootFlag n)) (W x) ∈159 (ℂ ∙ eta completedRootPureState.classOf : Submodule ℂ K) := by160 simpa using hWfixedSpan completedRootPureState.classOf x161 rw [heta_root] at hspan162 exact hline_mem completedRootPureState.classOf (by simpa [heta_root] using hspan)163 have hPfix (n : ℕ) : sigma (transportedFlag family i n) (eta i) = eta i :=164 (heta i).2.1 n165 have hPeta : P (eta i) = eta i := by166 rw [hPeq]167 exact (commonFixedProjection_eq_self_iff _ _).2168 ((mem_commonFixedSubspace_iff _ _).2 hPfix)169 have hQeta : Q eta_o = eta_o := by170 rw [hQeq]171 exact (commonFixedProjection_eq_self_iff _ _).2172 ((mem_commonFixedSubspace_iff _ _).2 heta_o_fixed)173 have hReta : R (eta i) = eta_o := by174 rw [hR]175 change (Unitary.linearIsometryEquiv176 (representedGeneratorUnitary L hLunit rho i) : K ≃ₗᵢ[ℂ] K)177 (P (eta i)) = eta_o178 rw [hPeta]179 exact heta_gen i180 have hRadjeta : (R†) eta_o = eta i := by181 have h := congrArg (fun A : K →L[ℂ] K ↦ A (eta i)) hRinitial182 change (R†) (R (eta i)) = P (eta i) at h183 simpa [hReta, hPeta] using h184 have hRinv : M.IsInvariantUnder R := by185 rintro _ ⟨x, rfl⟩186 change R (W x) ∈ M187 rw [hR, ContinuousLinearMap.comp_apply, hPeq]188 obtain ⟨c, hc⟩ := Submodule.mem_span_singleton.mp (hWfixedSpan i x)189 have hgen_i :190 (((Unitary.linearIsometryEquiv191 (representedGeneratorUnitary L hLunit rho i) : K ≃ₗᵢ[ℂ] K) :192 K →L[ℂ] K) (eta i)) = eta_o := heta_gen i193 rw [← hc, map_smul, hgen_i]194 have hrootMem : eta_o ∈ M := by195 rw [← heta_root]196 exact hline_mem completedRootPureState.classOf197 (Submodule.mem_span_singleton_self _)198 exact M.smul_mem c hrootMem199 have hRadjSupport : R† = (P.comp (R†)).comp Q := by200 have h := congrArg (fun A : K →L[ℂ] K ↦ A†) hRsupport201 have hPadj : P† = P := by202 simpa [ContinuousLinearMap.star_eq_adjoint] using203 hPproj.isSelfAdjoint.star_eq204 have hQadj : Q† = Q := by205 simpa [ContinuousLinearMap.star_eq_adjoint] using206 hQproj.isSelfAdjoint.star_eq207 have h' : R† = P.comp ((R†).comp Q) := by208 simpa [ContinuousLinearMap.adjoint_comp, hPadj, hQadj] using h209 exact h'.trans (ContinuousLinearMap.comp_assoc P (R†) Q).symm210 have hRadjinv : M.IsInvariantUnder (R†) := by211 rintro _ ⟨x, rfl⟩212 change (R†) (W x) ∈ M213 rw [hRadjSupport, ContinuousLinearMap.comp_apply,214 ContinuousLinearMap.comp_apply, hQeq]215 have hspan : commonFixedProjection (fun n ↦ sigma (rootFlag n)) (W x) ∈216 (ℂ ∙ eta completedRootPureState.classOf : Submodule ℂ K) := by217 simpa using hWfixedSpan completedRootPureState.classOf x218 obtain ⟨c, hc⟩ := Submodule.mem_span_singleton.mp hspan219 rw [heta_root] at hc220 rw [← hc, map_smul, hRadjeta, map_smul, hPeta]221 exact hline_mem i (Submodule.smul_mem _ c222 (Submodule.mem_span_singleton_self (eta i)))223 have hRreduces : M.Reduces R := ⟨hRinv, hRadjinv⟩224 have hsumReduces : M.Reduces (S + R) := by225 constructor226 · intro x hx227 exact M.add_mem (hSreduces.1 hx) (hRreduces.1 hx)228 · intro x hx229 have hadd := M.add_mem (hSreduces.2 hx) (hRreduces.2 hx)230 simpa only [map_add ContinuousLinearMap.adjoint, add_apply] using hadd231 change M.Reduces232 (((representedGeneratorUnitary L hLunit rho i : unitary (K →L[ℂ] K)) :233 K →L[ℂ] K))234 rw [show (((representedGeneratorUnitary L hLunit rho i :235 unitary (K →L[ℂ] K)) : K →L[ℂ] K)) = S + R by236 simpa using hgeneratorEq]237 exact hsumReduces238 have hall : ∀ x : AtomicTarget L, M.Reduces (rho x) :=239 MathlibAnnex.CStarAlgebra.AtomicConstruction.reduces_concreteTarget_of_generators240 selectedAtomicRepresentation L rho M hMclosed241 (fun a ↦ hsourceReduces a) hgeneratorReduces242 have hMrepresentation : rho.Reduces M := by243 refine ⟨hMclosed, ?_⟩244 intro a x hx245 exact ⟨(hall a).1 hx, (hall a).2 hx⟩246 have hMne : M ≠ ⊥ := by247 intro hbot248 have hmem : eta_o ∈ M := by249 rw [← heta_root]250 exact hline_mem completedRootPureState.classOf251 (Submodule.mem_span_singleton_self _)252 rw [hbot, Submodule.mem_bot] at hmem253 have hnorm := congrArg norm hmem254 simpa [heta_o_norm] using hnorm255 have hMtop : M = ⊤ := (hrho.2 M hMrepresentation).resolve_left hMne256 have hWsurj : Function.Surjective W := by257 intro y258 have hy : y ∈ M := by rw [hMtop]; exact Submodule.mem_top259 exact hy260 exact ⟨eta_o, eta, W, hWsurj, heta_o_norm, heta_norm, hWpoint,261 heta_gen, hWsource⟩262263/-- Consequently, the actual completed-CAR source restriction of every264irreducible target representation is unitarily equivalent to the displayed265arbitrary-index selected pure-GNS sum. -/266theorem selectedAtomicRepresentation_unitaryEquivalent_restricted267 (family : RepresentativeShellFamily)268 (L : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit →269 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]270 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)271 (hLunit : ∀ i, L i ∈ unitary272 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]273 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState))274 (hLsource : ∀ i n, (L i).comp (selectedAtomicRepresentation275 (transportedFlag family i n - transportedFlag family i (n + 1))) =276 representedShellLink family i n)277 (hLroot : L completedRootPureState.classOf = 1)278 {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K]279 [CompleteSpace K] (rho : Representation (AtomicTarget L) K)280 (hrho : rho.IsIrreducible) :281 selectedAtomicRepresentation.UnitaryEquivalent282 (restrictedRepresentation L rho) := by283 obtain ⟨eta_o, eta, W, hWsurj, -, -, -, -, hW⟩ :=284 exists_surjective_selectedAtomicCyclicIsometry285 family L hLunit hLsource hLroot rho hrho286 let E : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState ≃ₗᵢ[ℂ] K :=287 LinearIsometryEquiv.ofSurjective W hWsurj288 refine ⟨E, ?_⟩289 intro a x290 have h := congrArg291 (fun T : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K ↦292 T x) (hW a)293 simpa [E, ContinuousLinearMap.comp_apply] using h294295end MathlibAnnex.CStarAlgebra.CAR