Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/AtomicSource.lean, lines 39–46.
Back to The atomic common range is one embedded GNS line · Back to Choosing the CAR shell family from proved homogeneity · Back to The matching GNS fiber retains exactly its cyclic line · Back to The shell-generated algebra is not an algebra of all compact operators · Back to Structural properties of one shell-generated C*-algebra · Back to Every irreducible representation is unitarily equivalent to the inclusion · Back to Realizing a shell family by a faithful irreducible operator algebra · Back to The CAR source map into the fixed shell-family target · Back to Shell matching fixes the trace of transported flags · Back to Transported flags vanish on vectors generated by a trace vector · Back to Closed-ideal simplicity of the shell-generated algebra · Back to An inequivalent GNS fiber has no residual common range · Back to An irreducible target representation has a surviving fixed space · Back to Reconstructing a represented unitary from its shells and residual corner · Back to A fixed representative family of CAR shell data · Back to Unitary equivalence without an initial unitality assumption · 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.DifferenceShell 2import MathlibAnnex.Analysis.CStarAlgebra.AtomicConstruction.PureAtomic 3import MathlibAnnex.Analysis.CStarAlgebra.Representation.CommonFixedSubspace 4 5/-! 6# Completed CAR data for the atomic shell model 7 8The downstream construction is parameterized by one family of shell data. 9The historical KOS-facing constructor remains as a compatibility provider; 10the closed CAR homogeneity theorem supplies a second provider in `Main`. 11-/ 12 13set_option autoImplicit false 14set_option maxHeartbeats 800000 15 16noncomputable section 17 18open Filter Topology 19open scoped ENNReal lp InnerProduct 20 21namespace MathlibAnnex.CStarAlgebra.CAR 22 23open MathlibAnnex.Analysis.CStarAlgebra 24open MathlibAnnex.Analysis.InnerProductSpace 25 26/-- Natural source data for one selected pure-state class. Its fields are 27only the automorphism and exact algebraic shell links obtained from KOS. -/ 28structure RepresentativeShellData (j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) where 29 alpha : Limit ≃⋆ₐ[ℂ] Limit 30 state_eq : ∀ a : Limit, 31 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState j).1 (alpha a) = 32 completedRootPureState.1 a 33 link : ℕ → Limit 34 initial_support : ∀ n, 35 star (link n) * link n = alpha (rootShell n) 36 final_support : ∀ n, 37 link n * star (link n) = rootShell n 38 39/-- A single fixed family of shell data. The distinguished root component is 40definitionally controlled by explicit identity/link equations; no rank-one, 41capture, simplicity, or compactness conclusion is stored in this input. -/ 42structure RepresentativeShellFamily where 43 data : ∀ j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit, RepresentativeShellData j 44 root_alpha : (data completedRootPureState.classOf).alpha = 45 StarAlgEquiv.refl ℂ Limit 46 root_link : ∀ n, (data completedRootPureState.classOf).link n = rootShell n 47 48/-- The component of a fixed representative shell family. -/ 49noncomputable def representativeShellData (family : RepresentativeShellFamily) 50 (j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : RepresentativeShellData j := 51 family.data j 52 53/-- Historical KOS provider for one component, retained only to build the 54compatibility family below. -/ 55noncomputable def representativeShellDataOfKishimotoOzawaSakai (hKOS : MathlibAnnex.CStarAlgebra.KishimotoOzawaSakaiProperty.{0}) 56 (j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : RepresentativeShellData j := by 57 classical 58 by_cases hj : j = completedRootPureState.classOf 59 · subst j 60 exact 61 { alpha := StarAlgEquiv.refl ℂ Limit 62 state_eq := rootShell_identity_family.1 63 link := rootShell 64 initial_support := fun n ↦ (rootShell_identity_family.2 n).1 65 final_support := fun n ↦ (rootShell_identity_family.2 n).2 } 66 · let hex := exists_representative_rootShell_family_of_kishimotoOzawaSakai hKOS j 67 let alpha := Classical.choose hex 68 have halpha := Classical.choose_spec hex 69 let w := Classical.choose halpha.2 70 have hw := Classical.choose_spec halpha.2 71 exact 72 { alpha := alpha 73 state_eq := halpha.1 74 link := w 75 initial_support := fun n ↦ (hw n).1 76 final_support := fun n ↦ (hw n).2 } 77 78/-- Historical all-simple-algebras KOS input produces the same natural family 79interface used by the successor construction. -/ 80noncomputable def representativeShellFamilyOfKishimotoOzawaSakai 81 (hKOS : MathlibAnnex.CStarAlgebra.KishimotoOzawaSakaiProperty.{0}) : RepresentativeShellFamily where 82 data := representativeShellDataOfKishimotoOzawaSakai hKOS 83 root_alpha := by simp [representativeShellDataOfKishimotoOzawaSakai] 84 root_link := by 85 intro n 86 simp [representativeShellDataOfKishimotoOzawaSakai] 87 88@[simp] 89theorem representativeShellData_root_alpha (family : RepresentativeShellFamily) : 90 (representativeShellData family completedRootPureState.classOf).alpha = 91 StarAlgEquiv.refl ℂ Limit := 92 family.root_alpha 93 94@[simp] 95theorem representativeShellData_root_link (family : RepresentativeShellFamily) 96 (n : ℕ) : 97 (representativeShellData family completedRootPureState.classOf).link n = 98 rootShell n := 99 family.root_link n 100 101/-- The transported decreasing flag associated with one selected state. -/ 102noncomputable def transportedFlag (family : RepresentativeShellFamily) 103 (j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (n : ℕ) : Limit := 104 (representativeShellData family j).alpha (rootFlag n) 105 106theorem isStarProjection_transportedFlag (family : RepresentativeShellFamily) 107 (j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (n : ℕ) : 108 IsStarProjection (transportedFlag family j n) := 109 (isStarProjection_rootFlag n).map (representativeShellData family j).alpha 110 111@[simp] 112theorem transportedFlag_root (family : RepresentativeShellFamily) (n : ℕ) : 113 transportedFlag family completedRootPureState.classOf n = rootFlag n := by 114 simp [transportedFlag] 115 116@[simp] 117theorem transportedFlag_zero (family : RepresentativeShellFamily) 118 (j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : transportedFlag family j 0 = 1 := by 119 simp [transportedFlag] 120 121theorem rootFlag_mul_of_le {m n : ℕ} (hmn : m ≤ n) : 122 rootFlag m * rootFlag n = rootFlag n := 123 ((isStarProjection_rootFlag n).le_iff_mul_eq_right 124 (isStarProjection_rootFlag m)).1 (antitone_rootFlag hmn) 125 126theorem transportedFlag_mul_of_le (family : RepresentativeShellFamily) 127 (j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) {m n : ℕ} (hmn : m ≤ n) : 128 transportedFlag family j m * transportedFlag family j n = 129 transportedFlag family j n := by 130 change (representativeShellData family j).alpha (rootFlag m) * 131 (representativeShellData family j).alpha (rootFlag n) = 132 (representativeShellData family j).alpha (rootFlag n) 133 rw [← map_mul, rootFlag_mul_of_le hmn] 134 135theorem representativeLink_initial (family : RepresentativeShellFamily) 136 (j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (n : ℕ) : 137 star ((representativeShellData family j).link n) * 138 (representativeShellData family j).link n = 139 transportedFlag family j n - transportedFlag family j (n + 1) := by 140 simpa [transportedFlag, rootShell] using 141 (representativeShellData family j).initial_support n 142 143theorem representativeLink_final (family : RepresentativeShellFamily) 144 (j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (n : ℕ) : 145 (representativeShellData family j).link n * 146 star ((representativeShellData family j).link n) = 147 rootFlag n - rootFlag (n + 1) := by 148 simpa [rootShell] using (representativeShellData family j).final_support n 149 150theorem tendsto_representative_transported_compression 151 (family : RepresentativeShellFamily) (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) 152 (b : Limit) : 153 Tendsto 154 (fun n ↦ transportedFlag family i n * b * transportedFlag family i n - 155 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1 b • 156 transportedFlag family i n) 157 atTop (nhds 0) := by 158 exact tendsto_transported_compressionError 159 (representativeShellData family i).alpha 160 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1 161 (representativeShellData family i).state_eq b 162 163/-- Every transported flag fixes the canonical vector in its matching selected 164GNS fiber. -/ 165theorem selectedVector_fixed_transportedFlag (family : RepresentativeShellFamily) 166 (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (n : ℕ) : 167 MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i 168 (transportedFlag family i n) 169 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i) = 170 MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i := by 171 apply projection_apply_eq_self_of_vectorFunctional_eq_one 172 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i) 173 (transportedFlag family i n) (isStarProjection_transportedFlag family i n) 174 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i) 175 (MathlibAnnex.CStarAlgebra.PureState.norm_selectedVector completedRootPureState i) 176 calc 177 Representation.vectorFunctional 178 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i) 179 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i) 180 (transportedFlag family i n) = 181 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1 182 (transportedFlag family i n) := 183 DFunLike.congr_fun (MathlibAnnex.CStarAlgebra.PureState.selected_vectorFunctional 184 completedRootPureState i) _ 185 _ = rootState (rootFlag n) := 186 (representativeShellData family i).state_eq (rootFlag n) 187 _ = 1 := rootState_rootFlag n 188 189/-- In the matching selected fiber the common fixed projection is the 190rank-one projection onto its canonical GNS vector. -/ 191theorem selected_commonFixedProjection_eq_rankOne 192 (family : RepresentativeShellFamily) (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : 193 commonFixedProjection (fun n ↦ 194 MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i 195 (transportedFlag family i n)) = 196 InnerProductSpace.rankOne ℂ 197 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i) 198 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i) := by 199 apply commonFixedProjection_eq_rankOne_of_dense_orbit 200 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i) 201 (transportedFlag family i) 202 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1 203 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i) 204 · intro n 205 exact (isStarProjection_transportedFlag family i n).isSelfAdjoint.star_eq 206 · exact tendsto_representative_transported_compression family i 207 · exact selectedVector_fixed_transportedFlag family i 208 · intro b 209 exact (DFunLike.congr_fun (MathlibAnnex.CStarAlgebra.PureState.selected_vectorFunctional 210 completedRootPureState i) b).symm 211 · exact MathlibAnnex.CStarAlgebra.PureState.denseRange_representative_gns_orbit 212 completedRootPureState i 213 214/-- In every inequivalent selected fiber the same transported flag has zero 215common fixed projection. -/ 216theorem selected_commonFixedProjection_eq_zero 217 (family : RepresentativeShellFamily) {i j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit} 218 (hij : j ≠ i) : 219 commonFixedProjection (fun n ↦ 220 MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState j 221 (transportedFlag family i n)) = 0 := by 222 apply commonFixedProjection_eq_zero_of_no_unitary 223 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i) 224 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState j) 225 (transportedFlag family i) 226 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1 227 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i) 228 · intro n 229 exact (isStarProjection_transportedFlag family i n).isSelfAdjoint.star_eq 230 · exact tendsto_representative_transported_compression family i 231 · intro b 232 exact DFunLike.congr_fun (MathlibAnnex.CStarAlgebra.PureState.selected_vectorFunctional 233 completedRootPureState i) b 234 · exact MathlibAnnex.CStarAlgebra.PureState.denseRange_representative_gns_orbit 235 completedRootPureState i 236 · exact MathlibAnnex.CStarAlgebra.PureState.isIrreducible_selectedRepresentation 237 completedRootPureState j 238 · intro U 239 exact MathlibAnnex.CStarAlgebra.PureState.no_unitaryIntertwiner_selectedRepresentation 240 completedRootPureState hij.symm U 241 242/-- The transported flag has precisely one fixed coordinate in the displayed 243arbitrary-index atomic representation. -/ 244theorem iInf_range_atomic_transportedFlag_eq_span 245 (family : RepresentativeShellFamily) (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : 246 (⨅ n, (atomicRepresentation 247 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState) 248 (transportedFlag family i n)).range) = 249 ℂ ∙ MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i 250 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i) := by 251 classical 252 simpa [MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding] using 253 (iInf_range_atomicRepresentation_eq_span 254 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState) 255 (transportedFlag family i) 256 (isStarProjection_transportedFlag family i) i 257 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i) 258 (MathlibAnnex.CStarAlgebra.PureState.norm_selectedVector completedRootPureState i) 259 (selected_commonFixedProjection_eq_rankOne family i) 260 (fun j hji ↦ selected_commonFixedProjection_eq_zero family hji)) 261 262end MathlibAnnex.CStarAlgebra.CAR