Exact source view. Private integrated preview.
Exact declaration: MathlibAnnex.CStarAlgebra.CAR.ShellFamilyTarget
MathlibAnnex/Analysis/CStarAlgebra/CAR/AtomicEndpoint.lean · lines 62–64
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.Capture 2import MathlibAnnex.Analysis.CStarAlgebra.Representation.UniqueModelConsequences 3import MathlibAnnex.Analysis.CStarAlgebra.Representation.NonUnital 4 5/-! 6# Shell-family atomic endpoint 7 8The completed-CAR shell family is chosen once, independently of every later 9target Hilbert-space universe. All ordinary consequences below refer to 10that same concrete generated C-star algebra. 11-/ 12 13set_option autoImplicit false 14 15noncomputable section 16 17open Set 18open scoped ComplexOrder InnerProduct 19 20namespace MathlibAnnex.CStarAlgebra.CAR 21 22open MathlibAnnex.Analysis.CStarAlgebra 23 24universe v 25 26/-- The one completed-CAR link family selected from the actual shell-model 27construction. Its definition has no target Hilbert-space universe 28parameter. -/ 29noncomputable def shellFamilyLinks (family : RepresentativeShellFamily) : 30 MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit → 31 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] 32 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState := 33 Classical.choose (exists_completedAtomicShellModel family) 34 35theorem shellFamilyLinks_unitary (family : RepresentativeShellFamily) : 36 ∀ i, shellFamilyLinks family i ∈ unitary 37 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] 38 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState) := 39 (Classical.choose_spec (exists_completedAtomicShellModel family)).1 40 41theorem shellFamilyLinks_map_selectedVector (family : RepresentativeShellFamily) : 42 ∀ i, shellFamilyLinks family i 43 (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i 44 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) = 45 MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState 46 completedRootPureState.classOf 47 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState 48 completedRootPureState.classOf) := 49 (Classical.choose_spec (exists_completedAtomicShellModel family)).2.1 50 51theorem shellFamilyLinks_sourceShell (family : RepresentativeShellFamily) : 52 ∀ i n, (shellFamilyLinks family i).comp 53 (selectedAtomicRepresentation 54 (transportedFlag family i n - transportedFlag family i (n + 1))) = 55 representedShellLink family i n := 56 (Classical.choose_spec (exists_completedAtomicShellModel family)).2.2.1 57 58theorem shellFamilyLinks_root (family : RepresentativeShellFamily) : 59 shellFamilyLinks family completedRootPureState.classOf = 1 := 60 (Classical.choose_spec (exists_completedAtomicShellModel family)).2.2.2.1 61 62/-- The single actual target used by every endpoint property. -/ 63abbrev ShellFamilyTarget (family : RepresentativeShellFamily) := 64 AtomicTarget (shellFamilyLinks family) 65 66/-- The actual completed CAR embeds unitally into the fixed target. -/ 67noncomputable def shellFamilySourceHom (family : RepresentativeShellFamily) : 68 Limit →⋆ₐ[ℂ] ShellFamilyTarget family := 69 MathlibAnnex.CStarAlgebra.AtomicConstruction.sourceHom selectedAtomicRepresentation (shellFamilyLinks family) 70 71/-- The fixed target's literal inclusion into its ambient operator algebra. -/ 72noncomputable def shellFamilyInclusion (family : RepresentativeShellFamily) : 73 Representation (ShellFamilyTarget family) 74 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState) := 75 MathlibAnnex.CStarAlgebra.AtomicConstruction.ambientInclusion selectedAtomicRepresentation 76 (shellFamilyLinks family) 77 78theorem shellFamilySourceHom_injective (family : RepresentativeShellFamily) : 79 Function.Injective (shellFamilySourceHom family) := by 80 exact 81 (Classical.choose_spec 82 (exists_completedAtomicShellModel family)).2.2.2.2.1 83 84noncomputable instance shellFamilyTargetNontrivial 85 (family : RepresentativeShellFamily) : Nontrivial (ShellFamilyTarget family) := 86 (shellFamilySourceHom_injective family).nontrivial 87 88noncomputable instance shellFamilyTargetPartialOrder 89 (family : RepresentativeShellFamily) : PartialOrder (ShellFamilyTarget family) := 90 CStarAlgebra.spectralOrder (ShellFamilyTarget family) 91 92noncomputable instance shellFamilyTargetStarOrderedRing 93 (family : RepresentativeShellFamily) : StarOrderedRing (ShellFamilyTarget family) := 94 CStarAlgebra.spectralOrderedRing (ShellFamilyTarget family) 95 96theorem isClosed_shellFamilyTarget (family : RepresentativeShellFamily) : 97 IsClosed 98 (ShellFamilyTarget family : Set 99 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] 100 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)) := by 101 infer_instance 102 103theorem shellFamilySourceHom_map_one (family : RepresentativeShellFamily) : 104 shellFamilySourceHom family 1 = 1 := 105 map_one (shellFamilySourceHom family) 106 107theorem shellFamilyInclusion_injective (family : RepresentativeShellFamily) : 108 Function.Injective (shellFamilyInclusion family) := by 109 exact MathlibAnnex.CStarAlgebra.AtomicConstruction.ambientInclusion_injective selectedAtomicRepresentation 110 (shellFamilyLinks family) 111 112theorem isIrreducible_shellFamilyInclusion (family : RepresentativeShellFamily) : 113 Representation.IsIrreducible (shellFamilyInclusion family) := by 114 exact 115 (Classical.choose_spec 116 (exists_completedAtomicShellModel family)).2.2.2.2.2 117 118/-- The fixed target is infinite-dimensional because it contains an 119injective unital copy of the infinite-dimensional completed CAR algebra. -/ 120theorem not_finiteDimensional_shellFamilyTarget 121 (family : RepresentativeShellFamily) : 122 ¬ FiniteDimensional ℂ (ShellFamilyTarget family) := by 123 intro hfinite 124 letI : FiniteDimensional ℂ (ShellFamilyTarget family) := hfinite 125 exact not_finiteDimensional 126 (FiniteDimensional.of_injective 127 (LinearMapClass.linearMap (shellFamilySourceHom family)) 128 (shellFamilySourceHom_injective family)) 129 130/-- Every unital irreducible representation on an arbitrary independent 131Hilbert universe is equivalent to the fixed ambient inclusion. -/ 132theorem isUniqueIrreducibleModel_shellFamilyInclusion 133 (family : RepresentativeShellFamily) : 134 Representation.IsUniqueIrreducibleModel.{0, 0, v} 135 (shellFamilyInclusion family) := by 136 refine ⟨shellFamilyInclusion_injective family, 137 isIrreducible_shellFamilyInclusion family, ?_⟩ 138 intro K _ _ _ rho hrho 139 exact ambientInclusion_unitaryEquivalent family 140 (shellFamilyLinks family) 141 (shellFamilyLinks_unitary family) 142 (shellFamilyLinks_map_selectedVector family) 143 (shellFamilyLinks_sourceShell family) 144 (shellFamilyLinks_root family) rho hrho 145 146/-- The same fixed model captures ordinary nonzero irreducible 147representations even when their input bundle does not assume preservation of 148the unit. -/ 149theorem isUniqueIrreducibleModelAmongNonUnital_shellFamilyInclusion 150 (family : RepresentativeShellFamily) : 151 Representation.IsUniqueIrreducibleModelAmongNonUnital.{0, 0, v} 152 (shellFamilyInclusion family) := 153 (isUniqueIrreducibleModel_shellFamilyInclusion.{v} family).isUniqueIrreducibleModelAmongNonUnital 154 155/-- Expanded ordinary capture statement. The intertwining equation uses the 156original possibly nonunital representation, not merely its bundled 157`toUnital` view. -/ 158theorem shellFamilyInclusion_unitaryEquivalent_nonUnital 159 (family : RepresentativeShellFamily) 160 {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] 161 [CompleteSpace K] 162 (rho : NonUnitalRepresentation 163 (A := ShellFamilyTarget family) (H := K)) 164 (hrho : rho.IsIrreducible) : 165 ∃ U : 166 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState ≃ₗᵢ[ℂ] K, 167 ∀ (a : ShellFamilyTarget family) 168 (x : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState), 169 U (shellFamilyInclusion family a x) = rho a (U x) := by 170 obtain ⟨U, hU⟩ := 171 (isUniqueIrreducibleModelAmongNonUnital_shellFamilyInclusion.{v} family).2.2 172 K rho hrho 173 exact ⟨U, fun a x ↦ by simpa using hU a x⟩ 174 175/-- Closed two-sided ideals of the same fixed target are trivial. -/ 176theorem isSimpleCStarAlgebra_shellFamilyTarget (family : RepresentativeShellFamily) : 177 MathlibAnnex.CStarAlgebra.IsSimpleCStarAlgebra (ShellFamilyTarget family) := by 178 exact MathlibAnnex.CStarAlgebra.isSimpleCStarAlgebra_of_uniqueIrreducibleModel 179 (shellFamilyInclusion family) 180 (isUniqueIrreducibleModel_shellFamilyInclusion.{0} family) 181 182/-- The same target is not an exact algebraic model of all compact operators 183on any Hilbert space. -/ 184theorem not_isCompactOperatorModel_shellFamilyTarget 185 (family : RepresentativeShellFamily) 186 {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] 187 [CompleteSpace K] 188 (e : ShellFamilyTarget family →⋆ₙₐ[ℂ] (K →L[ℂ] K)) : 189 ¬ IsCompactOperatorModel e := 190 not_isCompactOperatorModel_of_infiniteDimensional 191 (not_finiteDimensional_shellFamilyTarget family) e 192 193/-- Fully expanded ordinary endpoint for the one fixed actual target. -/ 194structure ShellFamilyEndpoint (family : RepresentativeShellFamily) : Prop where 195 nontrivial_target : Nontrivial (ShellFamilyTarget family) 196 isClosed_target : 197 IsClosed 198 (ShellFamilyTarget family : Set 199 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ] 200 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)) 201 source_injective : Function.Injective (shellFamilySourceHom family) 202 source_unital : shellFamilySourceHom family 1 = 1 203 not_finiteDimensional_target : 204 ¬ FiniteDimensional ℂ (ShellFamilyTarget family) 205 ambient_injective : Function.Injective (shellFamilyInclusion family) 206 isIrreducible_ambient : 207 Representation.IsIrreducible (shellFamilyInclusion family) 208 captures_nonunital : 209 ∀ (K : Type v) [NormedAddCommGroup K] [InnerProductSpace ℂ K] 210 [CompleteSpace K] 211 (rho : NonUnitalRepresentation 212 (A := ShellFamilyTarget family) (H := K)), 213 rho.IsIrreducible → 214 ∃ U : 215 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState ≃ₗᵢ[ℂ] K, 216 ∀ (a : ShellFamilyTarget family) 217 (x : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState), 218 U (shellFamilyInclusion family a x) = rho a (U x) 219 closedIdeal_dichotomy : 220 ∀ I : TwoSidedIdeal (ShellFamilyTarget family), 221 IsClosed (I : Set (ShellFamilyTarget family)) → I = ⊥ ∨ I = ⊤ 222 not_compactOperatorModel : 223 ∀ (K : Type v) [NormedAddCommGroup K] [InnerProductSpace ℂ K] 224 [CompleteSpace K] 225 (e : ShellFamilyTarget family →⋆ₙₐ[ℂ] (K →L[ℂ] K)), 226 ¬ (Function.Injective e ∧ 227 (∀ a : ShellFamilyTarget family, IsCompactOperator (e a)) ∧ 228 ∀ T : K →L[ℂ] K, IsCompactOperator T → 229 ∃ a : ShellFamilyTarget family, e a = T) 230 231/-- The fixed target is nontrivial, in exactly the form used by the endpoint 232record. -/ 233theorem nontrivial_shellFamilyTarget (family : RepresentativeShellFamily) : 234 Nontrivial (ShellFamilyTarget family) := by 235 infer_instance 236 237/-- The ordinary nonunital capture theorem with the endpoint's explicit 238Hilbert-space binder. -/ 239theorem shellFamily_captures_nonunital (family : RepresentativeShellFamily) : 240 ∀ (K : Type v) [NormedAddCommGroup K] [InnerProductSpace ℂ K] 241 [CompleteSpace K] 242 (rho : NonUnitalRepresentation 243 (A := ShellFamilyTarget family) (H := K)), 244 rho.IsIrreducible → 245 ∃ U : 246 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState ≃ₗᵢ[ℂ] K, 247 ∀ (a : ShellFamilyTarget family) 248 (x : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState), 249 U (shellFamilyInclusion family a x) = rho a (U x) := by 250 intro K _ _ _ rho hrho 251 exact shellFamilyInclusion_unitaryEquivalent_nonUnital family rho hrho 252 253/-- The simplicity consequence in exactly the form stored by the endpoint. -/ 254theorem shellFamilyTarget_closedIdeal_dichotomy 255 (family : RepresentativeShellFamily) : 256 ∀ I : TwoSidedIdeal (ShellFamilyTarget family), 257 IsClosed (I : Set (ShellFamilyTarget family)) → I = ⊥ ∨ I = ⊤ := 258 (isSimpleCStarAlgebra_shellFamilyTarget family).2 259 260/-- The non-compact-model result in the endpoint's expanded surface form. 261The source theorem has this type definitionally, so no propositional transport 262is needed. -/ 263theorem shellFamilyTarget_not_compactOperatorModel 264 (family : RepresentativeShellFamily) : 265 ∀ (K : Type v) [NormedAddCommGroup K] [InnerProductSpace ℂ K] 266 [CompleteSpace K] 267 (e : ShellFamilyTarget family →⋆ₙₐ[ℂ] (K →L[ℂ] K)), 268 ¬ (Function.Injective e ∧ 269 (∀ a : ShellFamilyTarget family, IsCompactOperator (e a)) ∧ 270 ∀ T : K →L[ℂ] K, IsCompactOperator T → 271 ∃ a : ShellFamilyTarget family, e a = T) := by 272 intro K _ _ _ e 273 exact not_isCompactOperatorModel_shellFamilyTarget family e 274 275/-- Ordinary family-parametric main. Shell matching is the only input; 276source faithfulness, capture, ideal simplicity, and noncompactness are proved 277in the core tree rather than stored in the family. -/ 278theorem shellFamilyEndpoint (family : RepresentativeShellFamily) : 279 ShellFamilyEndpoint.{v} family := by 280 refine 281 { nontrivial_target := nontrivial_shellFamilyTarget family 282 isClosed_target := isClosed_shellFamilyTarget family 283 source_injective := shellFamilySourceHom_injective family 284 source_unital := shellFamilySourceHom_map_one family 285 not_finiteDimensional_target := 286 not_finiteDimensional_shellFamilyTarget family 287 ambient_injective := shellFamilyInclusion_injective family 288 isIrreducible_ambient := isIrreducible_shellFamilyInclusion family 289 captures_nonunital := shellFamily_captures_nonunital family 290 closedIdeal_dichotomy := shellFamilyTarget_closedIdeal_dichotomy family 291 not_compactOperatorModel := 292 shellFamilyTarget_not_compactOperatorModel family } 293 294/-! ## Historical KOS-facing compatibility endpoint -/ 295 296/-- The original conditional target, now a transparent specialization of the 297family-parametric successor. -/ 298abbrev CompletedAtomicTarget (hKOS : MathlibAnnex.CStarAlgebra.KishimotoOzawaSakaiProperty.{0}) := 299 ShellFamilyTarget (representativeShellFamilyOfKishimotoOzawaSakai hKOS) 300 301/-- Historical source hom, retained as a transparent compatibility wrapper. -/ 302noncomputable def completedAtomicSourceHom (hKOS : MathlibAnnex.CStarAlgebra.KishimotoOzawaSakaiProperty.{0}) : 303 Limit →⋆ₐ[ℂ] CompletedAtomicTarget hKOS := 304 shellFamilySourceHom (representativeShellFamilyOfKishimotoOzawaSakai hKOS) 305 306/-- Historical ambient inclusion, retained as a transparent compatibility 307wrapper. -/ 308noncomputable def completedAtomicInclusion (hKOS : MathlibAnnex.CStarAlgebra.KishimotoOzawaSakaiProperty.{0}) : 309 Representation (CompletedAtomicTarget hKOS) 310 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState) := 311 shellFamilyInclusion (representativeShellFamilyOfKishimotoOzawaSakai hKOS) 312 313/-- The original endpoint proposition is the family successor specialized to 314the family supplied by the original generic KOS premise. -/ 315abbrev CompletedAtomicEndpoint (hKOS : MathlibAnnex.CStarAlgebra.KishimotoOzawaSakaiProperty.{0}) : Prop := 316 ShellFamilyEndpoint.{v} (representativeShellFamilyOfKishimotoOzawaSakai hKOS) 317 318/-- Historical conditional main, proved through the family-parametric tree. -/ 319theorem completedAtomicEndpoint (hKOS : MathlibAnnex.CStarAlgebra.KishimotoOzawaSakaiProperty.{0}) : 320 CompletedAtomicEndpoint.{v} hKOS := 321 shellFamilyEndpoint (representativeShellFamilyOfKishimotoOzawaSakai hKOS) 322 323end MathlibAnnex.CStarAlgebra.CAR