Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/CaptureRange.lean, lines 32–261.
Back to Every irreducible representation is unitarily equivalent to the inclusion · Back to The cyclic sum fills every irreducible target representation · Back to A common root vector realizes every selected state through the generators · Back to Assembling selected GNS cyclic subspaces into an isometric source representation
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.CyclicCapture 2import MathlibAnnex.Analysis.CStarAlgebra.AtomicConstruction.GeneratedReduction 3import MathlibAnnex.Analysis.InnerProductSpace.Reduction 4 5/-! 6# Surjectivity of the selected cyclic sum in an irreducible target 7 8The selected pure-state cyclic pieces form a closed source-reducing subspace. 9The represented completed-CAR shell reconstruction shows that this subspace 10also reduces every additional target generator: the strong shell part reduces 11it termwise, while the limiting corner is controlled by its initial and root 12one-dimensional fixed lines. Irreducibility of the arbitrary target 13representation then forces the cyclic sum to be the whole target Hilbert 14space. 15-/ 16 17set_option autoImplicit false 18set_option maxHeartbeats 1600000 19 20noncomputable section 21 22open Filter Topology 23open scoped ComplexOrder ENNReal lp InnerProduct 24 25namespace MathlibAnnex.CStarAlgebra.CAR 26 27open MathlibAnnex.Analysis.CStarAlgebra 28open MathlibAnnex.Analysis.InnerProductSpace 29 30universe v 31 32/-- The arbitrary-index sum of the selected pure GNS cyclic copies is 33surjective in every nonzero irreducible representation of the actual target. 34The returned map still records its source intertwining law and its action on 35all selected cyclic vectors. -/ 36theorem exists_surjective_selectedAtomicCyclicIsometry 37 (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 ∈ unitary 42 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] 43 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)) 44 (hLsource : ∀ i n, (L i).comp (selectedAtomicRepresentation 45 (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 i 57 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) = eta i) ∧ 58 (∀ i, (Unitary.linearIsometryEquiv 59 (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).comp 64 W.toContinuousLinearMap := by 65 classical 66 let sigma := restrictedRepresentation L rho 67 obtain ⟨eta_o, eta, heta_o_norm, heta_o_fixed, heta_o_state, heta⟩ := 68 exists_targetDefectVectorFamily family L hLunit hLsource rho hrho 69 have heta_norm : ∀ i, ‖eta i‖ = 1 := fun i ↦ (heta i).1 70 have heta_state : ∀ i, Representation.vectorFunctional sigma (eta i) = 71 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1 := 72 fun i ↦ (heta i).2.2.2 73 have heta_gen : ∀ i, (Unitary.linearIsometryEquiv 74 (representedGeneratorUnitary L hLunit rho i) : K ≃ₗᵢ[ℂ] K) 75 (eta i) = eta_o := fun i ↦ (heta i).2.2.1 76 obtain ⟨W, hWcyclic, hWpoint, hWfixedSpan, hWsource⟩ := 77 exists_selectedAtomicCyclicIsometry family sigma eta heta_norm heta_state 78 let M : Submodule ℂ K := LinearMap.range W.toLinearMap 79 have hMclosed : IsClosed (M : Set K) := by 80 change IsClosed (Set.range W) 81 exact W.isometry.isClosedEmbedding.isClosed_range 82 have hsourceReduces (a : Limit) : M.Reduces (sigma a) := by 83 constructor 84 · rintro _ ⟨x, rfl⟩ 85 refine ⟨selectedAtomicRepresentation a x, ?_⟩ 86 have h := congrArg 87 (fun T : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K ↦ 88 T x) (hWsource a) 89 simpa [ContinuousLinearMap.comp_apply] using h 90 · rintro _ ⟨x, rfl⟩ 91 refine ⟨selectedAtomicRepresentation (star a) x, ?_⟩ 92 have h := congrArg 93 (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 h 97 have htargetRoot : MathlibAnnex.CStarAlgebra.AtomicConstruction.generator selectedAtomicRepresentation L 98 completedRootPureState.classOf = 99 MathlibAnnex.CStarAlgebra.AtomicConstruction.sourceHom selectedAtomicRepresentation L 1 := by 100 apply Subtype.ext 101 simpa using hLroot 102 have hrootGenerator : 103 ((Unitary.linearIsometryEquiv 104 (representedGeneratorUnitary L hLunit rho 105 completedRootPureState.classOf) : K ≃ₗᵢ[ℂ] K) : K →L[ℂ] K) = 1 := by 106 change rho (MathlibAnnex.CStarAlgebra.AtomicConstruction.generator selectedAtomicRepresentation L 107 completedRootPureState.classOf) = 1 108 rw [htargetRoot, map_one] 109 exact map_one rho 110 have heta_root : eta completedRootPureState.classOf = eta_o := by 111 have h := heta_gen completedRootPureState.classOf 112 change (((Unitary.linearIsometryEquiv 113 (representedGeneratorUnitary L hLunit rho 114 completedRootPureState.classOf) : K ≃ₗᵢ[ℂ] K) : K →L[ℂ] K) 115 (eta completedRootPureState.classOf)) = eta_o at h 116 rw [hrootGenerator] at h 117 simpa using h 118 have hline_mem (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) {y : K} 119 (hy : y ∈ (ℂ ∙ eta i : Submodule ℂ K)) : y ∈ M := by 120 obtain ⟨c, hc⟩ := Submodule.mem_span_singleton.mp hy 121 refine ⟨c • MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i 122 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i), ?_⟩ 123 change W (c • MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i 124 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) = y 125 rw [map_smul, hWpoint] 126 exact hc 127 have hgeneratorReduces (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : 128 M.Reduces (rho (MathlibAnnex.CStarAlgebra.AtomicConstruction.generator selectedAtomicRepresentation L i)) := by 129 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 i 133 have hSreduces : M.Reduces S := by 134 apply Submodule.Reduces.of_stronglyConverges_partialSum hMclosed 135 (W := fun n ↦ sigma ((representativeShellData family i).link n)) 136 (T := T) 137 · intro n 138 exact hsourceReduces ((representativeShellData family i).link n) 139 · exact hS 140 · exact hT 141 · exact hAdj 142 have hPeq : P = commonFixedProjection 143 (fun n ↦ sigma (transportedFlag family i n)) := by 144 exact starProjection_eq_commonFixedProjection_of_range_iInf sigma 145 (transportedFlag family i) (isStarProjection_transportedFlag family i) 146 P hPproj hPrange 147 have hQeq : Q = commonFixedProjection 148 (fun n ↦ sigma (rootFlag n)) := by 149 exact starProjection_eq_commonFixedProjection_of_range_iInf sigma 150 rootFlag isStarProjection_rootFlag Q hQproj hQrange 151 have hPinv : M.IsInvariantUnder P := by 152 rintro _ ⟨x, rfl⟩ 153 rw [hPeq] 154 exact hline_mem i (hWfixedSpan i x) 155 have hQinv : M.IsInvariantUnder Q := by 156 rintro _ ⟨x, rfl⟩ 157 rw [hQeq] 158 have hspan : commonFixedProjection (fun n ↦ sigma (rootFlag n)) (W x) ∈ 159 (ℂ ∙ eta completedRootPureState.classOf : Submodule ℂ K) := by 160 simpa using hWfixedSpan completedRootPureState.classOf x 161 rw [heta_root] at hspan 162 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 n 165 have hPeta : P (eta i) = eta i := by 166 rw [hPeq] 167 exact (commonFixedProjection_eq_self_iff _ _).2 168 ((mem_commonFixedSubspace_iff _ _).2 hPfix) 169 have hQeta : Q eta_o = eta_o := by 170 rw [hQeq] 171 exact (commonFixedProjection_eq_self_iff _ _).2 172 ((mem_commonFixedSubspace_iff _ _).2 heta_o_fixed) 173 have hReta : R (eta i) = eta_o := by 174 rw [hR] 175 change (Unitary.linearIsometryEquiv 176 (representedGeneratorUnitary L hLunit rho i) : K ≃ₗᵢ[ℂ] K) 177 (P (eta i)) = eta_o 178 rw [hPeta] 179 exact heta_gen i 180 have hRadjeta : (R†) eta_o = eta i := by 181 have h := congrArg (fun A : K →L[ℂ] K ↦ A (eta i)) hRinitial 182 change (R†) (R (eta i)) = P (eta i) at h 183 simpa [hReta, hPeta] using h 184 have hRinv : M.IsInvariantUnder R := by 185 rintro _ ⟨x, rfl⟩ 186 change R (W x) ∈ M 187 rw [hR, ContinuousLinearMap.comp_apply, hPeq] 188 obtain ⟨c, hc⟩ := Submodule.mem_span_singleton.mp (hWfixedSpan i x) 189 have hgen_i : 190 (((Unitary.linearIsometryEquiv 191 (representedGeneratorUnitary L hLunit rho i) : K ≃ₗᵢ[ℂ] K) : 192 K →L[ℂ] K) (eta i)) = eta_o := heta_gen i 193 rw [← hc, map_smul, hgen_i] 194 have hrootMem : eta_o ∈ M := by 195 rw [← heta_root] 196 exact hline_mem completedRootPureState.classOf 197 (Submodule.mem_span_singleton_self _) 198 exact M.smul_mem c hrootMem 199 have hRadjSupport : R† = (P.comp (R†)).comp Q := by 200 have h := congrArg (fun A : K →L[ℂ] K ↦ A†) hRsupport 201 have hPadj : P† = P := by 202 simpa [ContinuousLinearMap.star_eq_adjoint] using 203 hPproj.isSelfAdjoint.star_eq 204 have hQadj : Q† = Q := by 205 simpa [ContinuousLinearMap.star_eq_adjoint] using 206 hQproj.isSelfAdjoint.star_eq 207 have h' : R† = P.comp ((R†).comp Q) := by 208 simpa [ContinuousLinearMap.adjoint_comp, hPadj, hQadj] using h 209 exact h'.trans (ContinuousLinearMap.comp_assoc P (R†) Q).symm 210 have hRadjinv : M.IsInvariantUnder (R†) := by 211 rintro _ ⟨x, rfl⟩ 212 change (R†) (W x) ∈ M 213 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) := by 217 simpa using hWfixedSpan completedRootPureState.classOf x 218 obtain ⟨c, hc⟩ := Submodule.mem_span_singleton.mp hspan 219 rw [heta_root] at hc 220 rw [← hc, map_smul, hRadjeta, map_smul, hPeta] 221 exact hline_mem i (Submodule.smul_mem _ c 222 (Submodule.mem_span_singleton_self (eta i))) 223 have hRreduces : M.Reduces R := ⟨hRinv, hRadjinv⟩ 224 have hsumReduces : M.Reduces (S + R) := by 225 constructor 226 · intro x hx 227 exact M.add_mem (hSreduces.1 hx) (hRreduces.1 hx) 228 · intro x hx 229 have hadd := M.add_mem (hSreduces.2 hx) (hRreduces.2 hx) 230 simpa only [map_add ContinuousLinearMap.adjoint, add_apply] using hadd 231 change M.Reduces 232 (((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 by 236 simpa using hgeneratorEq] 237 exact hsumReduces 238 have hall : ∀ x : AtomicTarget L, M.Reduces (rho x) := 239 MathlibAnnex.CStarAlgebra.AtomicConstruction.reduces_concreteTarget_of_generators 240 selectedAtomicRepresentation L rho M hMclosed 241 (fun a ↦ hsourceReduces a) hgeneratorReduces 242 have hMrepresentation : rho.Reduces M := by 243 refine ⟨hMclosed, ?_⟩ 244 intro a x hx 245 exact ⟨(hall a).1 hx, (hall a).2 hx⟩ 246 have hMne : M ≠ ⊥ := by 247 intro hbot 248 have hmem : eta_o ∈ M := by 249 rw [← heta_root] 250 exact hline_mem completedRootPureState.classOf 251 (Submodule.mem_span_singleton_self _) 252 rw [hbot, Submodule.mem_bot] at hmem 253 have hnorm := congrArg norm hmem 254 simpa [heta_o_norm] using hnorm 255 have hMtop : M = ⊤ := (hrho.2 M hMrepresentation).resolve_left hMne 256 have hWsurj : Function.Surjective W := by 257 intro y 258 have hy : y ∈ M := by rw [hMtop]; exact Submodule.mem_top 259 exact hy 260 exact ⟨eta_o, eta, W, hWsurj, heta_o_norm, heta_norm, hWpoint, 261 heta_gen, hWsource⟩ 262 263/-- Consequently, the actual completed-CAR source restriction of every 264irreducible target representation is unitarily equivalent to the displayed 265arbitrary-index selected pure-GNS sum. -/ 266theorem selectedAtomicRepresentation_unitaryEquivalent_restricted 267 (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 ∈ unitary 272 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] 273 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)) 274 (hLsource : ∀ i n, (L i).comp (selectedAtomicRepresentation 275 (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.UnitaryEquivalent 282 (restrictedRepresentation L rho) := by 283 obtain ⟨eta_o, eta, W, hWsurj, -, -, -, -, hW⟩ := 284 exists_surjective_selectedAtomicCyclicIsometry 285 family L hLunit hLsource hLroot rho hrho 286 let E : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState ≃ₗᵢ[ℂ] K := 287 LinearIsometryEquiv.ofSurjective W hWsurj 288 refine ⟨E, ?_⟩ 289 intro a x 290 have h := congrArg 291 (fun T : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] K ↦ 292 T x) (hW a) 293 simpa [E, ContinuousLinearMap.comp_apply] using h 294 295end MathlibAnnex.CStarAlgebra.CAR