Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/AtomicEndpoint.lean
Pinned GitHub source · Raw UTF-8 source
Back to A Naimark counterexample of continuum norm density · Back to Unitary equivalence without an initial unitality assumption
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.Capture2import MathlibAnnex.Analysis.CStarAlgebra.Representation.UniqueModelConsequences3import MathlibAnnex.Analysis.CStarAlgebra.Representation.NonUnital45/-!6# Shell-family atomic endpoint78The completed-CAR shell family is chosen once, independently of every later9target Hilbert-space universe. All ordinary consequences below refer to10that same concrete generated C-star algebra.11-/1213set_option autoImplicit false1415noncomputable section1617open Set18open scoped ComplexOrder InnerProduct1920namespace MathlibAnnex.CStarAlgebra.CAR2122open MathlibAnnex.Analysis.CStarAlgebra2324universe v2526/-- The one completed-CAR link family selected from the actual shell-model27construction. Its definition has no target Hilbert-space universe28parameter. -/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)3435theorem shellFamilyLinks_unitary (family : RepresentativeShellFamily) :36 ∀ i, shellFamilyLinks family i ∈ unitary37 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]38 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState) :=39 (Classical.choose_spec (exists_completedAtomicShellModel family)).14041theorem shellFamilyLinks_map_selectedVector (family : RepresentativeShellFamily) :42 ∀ i, shellFamilyLinks family i43 (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i44 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) =45 MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState46 completedRootPureState.classOf47 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState48 completedRootPureState.classOf) :=49 (Classical.choose_spec (exists_completedAtomicShellModel family)).2.15051theorem shellFamilyLinks_sourceShell (family : RepresentativeShellFamily) :52 ∀ i n, (shellFamilyLinks family i).comp53 (selectedAtomicRepresentation54 (transportedFlag family i n - transportedFlag family i (n + 1))) =55 representedShellLink family i n :=56 (Classical.choose_spec (exists_completedAtomicShellModel family)).2.2.15758theorem shellFamilyLinks_root (family : RepresentativeShellFamily) :59 shellFamilyLinks family completedRootPureState.classOf = 1 :=60 (Classical.choose_spec (exists_completedAtomicShellModel family)).2.2.2.16162/-- The single actual target used by every endpoint property. -/63abbrev ShellFamilyTarget (family : RepresentativeShellFamily) :=64 AtomicTarget (shellFamilyLinks family)6566/-- 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)7071/-- 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 selectedAtomicRepresentation76 (shellFamilyLinks family)7778theorem shellFamilySourceHom_injective (family : RepresentativeShellFamily) :79 Function.Injective (shellFamilySourceHom family) := by80 exact81 (Classical.choose_spec82 (exists_completedAtomicShellModel family)).2.2.2.2.18384noncomputable instance shellFamilyTargetNontrivial85 (family : RepresentativeShellFamily) : Nontrivial (ShellFamilyTarget family) :=86 (shellFamilySourceHom_injective family).nontrivial8788noncomputable instance shellFamilyTargetPartialOrder89 (family : RepresentativeShellFamily) : PartialOrder (ShellFamilyTarget family) :=90 CStarAlgebra.spectralOrder (ShellFamilyTarget family)9192noncomputable instance shellFamilyTargetStarOrderedRing93 (family : RepresentativeShellFamily) : StarOrderedRing (ShellFamilyTarget family) :=94 CStarAlgebra.spectralOrderedRing (ShellFamilyTarget family)9596theorem isClosed_shellFamilyTarget (family : RepresentativeShellFamily) :97 IsClosed98 (ShellFamilyTarget family : Set99 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]100 MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)) := by101 infer_instance102103theorem shellFamilySourceHom_map_one (family : RepresentativeShellFamily) :104 shellFamilySourceHom family 1 = 1 :=105 map_one (shellFamilySourceHom family)106107theorem shellFamilyInclusion_injective (family : RepresentativeShellFamily) :108 Function.Injective (shellFamilyInclusion family) := by109 exact MathlibAnnex.CStarAlgebra.AtomicConstruction.ambientInclusion_injective selectedAtomicRepresentation110 (shellFamilyLinks family)111112theorem isIrreducible_shellFamilyInclusion (family : RepresentativeShellFamily) :113 Representation.IsIrreducible (shellFamilyInclusion family) := by114 exact115 (Classical.choose_spec116 (exists_completedAtomicShellModel family)).2.2.2.2.2117118/-- The fixed target is infinite-dimensional because it contains an119injective unital copy of the infinite-dimensional completed CAR algebra. -/120theorem not_finiteDimensional_shellFamilyTarget121 (family : RepresentativeShellFamily) :122 ¬ FiniteDimensional ℂ (ShellFamilyTarget family) := by123 intro hfinite124 letI : FiniteDimensional ℂ (ShellFamilyTarget family) := hfinite125 exact not_finiteDimensional126 (FiniteDimensional.of_injective127 (LinearMapClass.linearMap (shellFamilySourceHom family))128 (shellFamilySourceHom_injective family))129130/-- Every unital irreducible representation on an arbitrary independent131Hilbert universe is equivalent to the fixed ambient inclusion. -/132theorem isUniqueIrreducibleModel_shellFamilyInclusion133 (family : RepresentativeShellFamily) :134 Representation.IsUniqueIrreducibleModel.{0, 0, v}135 (shellFamilyInclusion family) := by136 refine ⟨shellFamilyInclusion_injective family,137 isIrreducible_shellFamilyInclusion family, ?_⟩138 intro K _ _ _ rho hrho139 exact ambientInclusion_unitaryEquivalent family140 (shellFamilyLinks family)141 (shellFamilyLinks_unitary family)142 (shellFamilyLinks_map_selectedVector family)143 (shellFamilyLinks_sourceShell family)144 (shellFamilyLinks_root family) rho hrho145146/-- The same fixed model captures ordinary nonzero irreducible147representations even when their input bundle does not assume preservation of148the unit. -/149theorem isUniqueIrreducibleModelAmongNonUnital_shellFamilyInclusion150 (family : RepresentativeShellFamily) :151 Representation.IsUniqueIrreducibleModelAmongNonUnital.{0, 0, v}152 (shellFamilyInclusion family) :=153 (isUniqueIrreducibleModel_shellFamilyInclusion.{v} family).isUniqueIrreducibleModelAmongNonUnital154155/-- Expanded ordinary capture statement. The intertwining equation uses the156original possibly nonunital representation, not merely its bundled157`toUnital` view. -/158theorem shellFamilyInclusion_unitaryEquivalent_nonUnital159 (family : RepresentativeShellFamily)160 {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K]161 [CompleteSpace K]162 (rho : NonUnitalRepresentation163 (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) := by170 obtain ⟨U, hU⟩ :=171 (isUniqueIrreducibleModelAmongNonUnital_shellFamilyInclusion.{v} family).2.2172 K rho hrho173 exact ⟨U, fun a x ↦ by simpa using hU a x⟩174175/-- Closed two-sided ideals of the same fixed target are trivial. -/176theorem isSimpleCStarAlgebra_shellFamilyTarget (family : RepresentativeShellFamily) :177 MathlibAnnex.CStarAlgebra.IsSimpleCStarAlgebra (ShellFamilyTarget family) := by178 exact MathlibAnnex.CStarAlgebra.isSimpleCStarAlgebra_of_uniqueIrreducibleModel179 (shellFamilyInclusion family)180 (isUniqueIrreducibleModel_shellFamilyInclusion.{0} family)181182/-- The same target is not an exact algebraic model of all compact operators183on any Hilbert space. -/184theorem not_isCompactOperatorModel_shellFamilyTarget185 (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_infiniteDimensional191 (not_finiteDimensional_shellFamilyTarget family) e192193/-- Fully expanded ordinary endpoint for the one fixed actual target. -/194structure ShellFamilyEndpoint (family : RepresentativeShellFamily) : Prop where195 nontrivial_target : Nontrivial (ShellFamilyTarget family)196 isClosed_target :197 IsClosed198 (ShellFamilyTarget family : Set199 (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 = 1203 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 : NonUnitalRepresentation212 (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)230231/-- The fixed target is nontrivial, in exactly the form used by the endpoint232record. -/233theorem nontrivial_shellFamilyTarget (family : RepresentativeShellFamily) :234 Nontrivial (ShellFamilyTarget family) := by235 infer_instance236237/-- The ordinary nonunital capture theorem with the endpoint's explicit238Hilbert-space binder. -/239theorem shellFamily_captures_nonunital (family : RepresentativeShellFamily) :240 ∀ (K : Type v) [NormedAddCommGroup K] [InnerProductSpace ℂ K]241 [CompleteSpace K]242 (rho : NonUnitalRepresentation243 (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) := by250 intro K _ _ _ rho hrho251 exact shellFamilyInclusion_unitaryEquivalent_nonUnital family rho hrho252253/-- The simplicity consequence in exactly the form stored by the endpoint. -/254theorem shellFamilyTarget_closedIdeal_dichotomy255 (family : RepresentativeShellFamily) :256 ∀ I : TwoSidedIdeal (ShellFamilyTarget family),257 IsClosed (I : Set (ShellFamilyTarget family)) → I = ⊥ ∨ I = ⊤ :=258 (isSimpleCStarAlgebra_shellFamilyTarget family).2259260/-- The non-compact-model result in the endpoint's expanded surface form.261The source theorem has this type definitionally, so no propositional transport262is needed. -/263theorem shellFamilyTarget_not_compactOperatorModel264 (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) := by272 intro K _ _ _ e273 exact not_isCompactOperatorModel_shellFamilyTarget family e274275/-- Ordinary family-parametric main. Shell matching is the only input;276source faithfulness, capture, ideal simplicity, and noncompactness are proved277in the core tree rather than stored in the family. -/278theorem shellFamilyEndpoint (family : RepresentativeShellFamily) :279 ShellFamilyEndpoint.{v} family := by280 refine281 { nontrivial_target := nontrivial_shellFamilyTarget family282 isClosed_target := isClosed_shellFamilyTarget family283 source_injective := shellFamilySourceHom_injective family284 source_unital := shellFamilySourceHom_map_one family285 not_finiteDimensional_target :=286 not_finiteDimensional_shellFamilyTarget family287 ambient_injective := shellFamilyInclusion_injective family288 isIrreducible_ambient := isIrreducible_shellFamilyInclusion family289 captures_nonunital := shellFamily_captures_nonunital family290 closedIdeal_dichotomy := shellFamilyTarget_closedIdeal_dichotomy family291 not_compactOperatorModel :=292 shellFamilyTarget_not_compactOperatorModel family }293294/-! ## Historical KOS-facing compatibility endpoint -/295296/-- The original conditional target, now a transparent specialization of the297family-parametric successor. -/298abbrev CompletedAtomicTarget (hKOS : MathlibAnnex.CStarAlgebra.KishimotoOzawaSakaiProperty.{0}) :=299 ShellFamilyTarget (representativeShellFamilyOfKishimotoOzawaSakai hKOS)300301/-- 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)305306/-- Historical ambient inclusion, retained as a transparent compatibility307wrapper. -/308noncomputable def completedAtomicInclusion (hKOS : MathlibAnnex.CStarAlgebra.KishimotoOzawaSakaiProperty.{0}) :309 Representation (CompletedAtomicTarget hKOS)310 (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState) :=311 shellFamilyInclusion (representativeShellFamilyOfKishimotoOzawaSakai hKOS)312313/-- The original endpoint proposition is the family successor specialized to314the family supplied by the original generic KOS premise. -/315abbrev CompletedAtomicEndpoint (hKOS : MathlibAnnex.CStarAlgebra.KishimotoOzawaSakaiProperty.{0}) : Prop :=316 ShellFamilyEndpoint.{v} (representativeShellFamilyOfKishimotoOzawaSakai hKOS)317318/-- Historical conditional main, proved through the family-parametric tree. -/319theorem completedAtomicEndpoint (hKOS : MathlibAnnex.CStarAlgebra.KishimotoOzawaSakaiProperty.{0}) :320 CompletedAtomicEndpoint.{v} hKOS :=321 shellFamilyEndpoint (representativeShellFamilyOfKishimotoOzawaSakai hKOS)322323end MathlibAnnex.CStarAlgebra.CAR