Exact source: MathlibAnnex/Analysis/CStarAlgebra/AtomicConstruction/PureAtomic.lean
Pinned GitHub source · Raw UTF-8 source
Back to The atomic direct sum of the selected CAR representations
1import MathlibAnnex.Analysis.CStarAlgebra.PureStateGNS.IrreduciblePure2import MathlibAnnex.Analysis.CStarAlgebra.AtomicConstruction.AtomicShell34/-!5# The chosen pure-GNS family as atomic-model source data67This file specializes the generic arbitrary-index shell model to the literal8root-preserving representatives already selected in `MathlibAnnex.CStarAlgebra.SourceRepresentatives`.9The remaining flag and shell inputs are representation-local data; no target10capture statement is assumed.11-/1213set_option autoImplicit false14set_option maxHeartbeats 8000001516noncomputable section1718open Filter Topology19open scoped ComplexOrder ENNReal lp InnerProduct2021namespace MathlibAnnex.CStarAlgebra2223universe u2425variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]2627namespace PureState2829/-- The Hilbert fiber of one chosen pure-state GNS representative. -/30abbrev SelectedGNS (root : PureState A) (j : GNSClass A) :=31 (representative root j).positiveFunctional.GNS3233/-- The chosen irreducible source representation on one selected fiber. -/34noncomputable def selectedRepresentation (root : PureState A) (j : GNSClass A) :35 MathlibAnnex.Analysis.CStarAlgebra.Representation A (SelectedGNS root j) :=36 (representative root j).positiveFunctional.gnsStarAlgHom3738/-- The canonical selected unit vector in one chosen GNS fiber. -/39noncomputable def selectedVector (root : PureState A) (j : GNSClass A) :40 SelectedGNS root j :=41 (representative root j).positiveFunctional.gnsCyclicVector4243theorem norm_selectedVector (root : PureState A) (j : GNSClass A) :44 ‖selectedVector root j‖ = 1 :=45 norm_representative_gnsCyclicVector root j4647/-- The canonical vector in a selected GNS fiber realizes its selected pure48state exactly. -/49theorem selected_vectorFunctional (root : PureState A) (j : GNSClass A) :50 MathlibAnnex.Analysis.CStarAlgebra.Representation.vectorFunctional51 (selectedRepresentation root j) (selectedVector root j) =52 (representative root j).1 := by53 apply ContinuousLinearMap.ext54 intro a55 exact PositiveLinearMap.inner_gnsCyclicVector_gnsStarAlgHom56 (representative root j).positiveFunctional a5758noncomputable instance SelectedGNS.instNontrivial59 (root : PureState A) (j : GNSClass A) : Nontrivial (SelectedGNS root j) := by60 apply nontrivial_of_ne (selectedVector root j) 061 intro hzero62 have hnorm := congrArg norm hzero63 simpa [norm_selectedVector] using hnorm6465/-- Every chosen pure-GNS fiber is irreducible. -/66theorem isIrreducible_selectedRepresentation (root : PureState A) (j : GNSClass A) :67 StarAlgHom.IsIrreducible (selectedRepresentation root j) := by68 apply isIrreducible_starAlgHom_of_isPureState69 (selectedRepresentation root j) (selectedVector root j)70 (norm_selectedVector root j)71 (denseRange_representative_gns_orbit root j)72 rw [selected_vectorFunctional]73 exact (representative root j).27475/-- Distinct chosen classes admit no unitary intertwiner. -/76theorem no_unitaryIntertwiner_selectedRepresentation (root : PureState A)77 {i j : GNSClass A} (hij : i ≠ j) (e : SelectedGNS root i ≃ₗᵢ[ℂ] SelectedGNS root j) :78 ¬ StarAlgHom.Intertwines (selectedRepresentation root i)79 (selectedRepresentation root j)80 (e : SelectedGNS root i →L[ℂ] SelectedGNS root j) := by81 intro he82 apply hij83 apply representative_injective_on_classes root84 refine ⟨e, ?_⟩85 intro a x86 have hx := congrArg87 (fun T : SelectedGNS root i →L[ℂ] SelectedGNS root j ↦ T x) (he a)88 simpa [selectedRepresentation, ContinuousLinearMap.comp_apply] using hx8990/-- The arbitrary dependent sum of the literal chosen pure-GNS fibers. -/91abbrev SelectedAtomicHilbert (root : PureState A) :=92 MathlibAnnex.Analysis.InnerProductSpace.HilbertSum (SelectedGNS root)9394/-- Coordinate inclusion using a local classical equality decision. -/95noncomputable def selectedEmbedding (root : PureState A) (j : GNSClass A) :96 SelectedGNS root j →L[ℂ] SelectedAtomicHilbert root := by97 classical98 exact MathlibAnnex.Analysis.InnerProductSpace.coordinateEmbedding j99100end PureState101102namespace AtomicConstruction103104open MathlibAnnex.Analysis.CStarAlgebra105open MathlibAnnex.Analysis.InnerProductSpace106107/-- Natural projection-shell data on the chosen pure-GNS family yields the108actual irreducible atomic model with unitary inter-block generators. -/109theorem exists_irreducible_pureAtomicShellModel110 (root : PureState A)111 (W : PureState.GNSClass A → ℕ →112 PureState.SelectedAtomicHilbert root →L[ℂ]113 PureState.SelectedAtomicHilbert root)114 (U V : PureState.GNSClass A → ℕ →115 Submodule ℂ (PureState.SelectedAtomicHilbert root))116 [∀ i n, (U i n).HasOrthogonalProjection]117 [∀ i n, (V i n).HasOrthogonalProjection]118 [∀ i, (⨅ n, U i n).HasOrthogonalProjection]119 [∀ i, (⨅ n, V i n).HasOrthogonalProjection]120 (hU : ∀ i, Antitone (U i)) (hV : ∀ i, Antitone (V i))121 (hU0 : ∀ i, U i 0 = ⊤) (hV0 : ∀ i, V i 0 = ⊤)122 (hInitial : ∀ i n, ((W i n)†).comp (W i n) =123 Submodule.projectionShell (U i) n)124 (hFinal : ∀ i n, (W i n).comp ((W i n)†) =125 Submodule.projectionShell (V i) n)126 (hUinf : ∀ i, (⨅ n, U i n).starProjection =127 InnerProductSpace.rankOne ℂ128 (PureState.selectedEmbedding root i (PureState.selectedVector root i))129 (PureState.selectedEmbedding root i (PureState.selectedVector root i)))130 (hVinf : ∀ i, (⨅ n, V i n).starProjection =131 InnerProductSpace.rankOne ℂ132 (PureState.selectedEmbedding root root.classOf133 (PureState.selectedVector root root.classOf))134 (PureState.selectedEmbedding root root.classOf135 (PureState.selectedVector root root.classOf))) :136 ∃ L : PureState.GNSClass A →137 PureState.SelectedAtomicHilbert root →L[ℂ]138 PureState.SelectedAtomicHilbert root,139 (∀ i, L i ∈ unitary140 (PureState.SelectedAtomicHilbert root →L[ℂ]141 PureState.SelectedAtomicHilbert root)) ∧142 (∀ i, L i (PureState.selectedEmbedding root i143 (PureState.selectedVector root i)) =144 PureState.selectedEmbedding root root.classOf145 (PureState.selectedVector root root.classOf)) ∧146 (∀ i n, (L i).comp (Submodule.projectionShell (U i) n) = W i n) ∧147 Representation.IsIrreducible148 (ambientInclusion149 (atomicRepresentation (PureState.selectedRepresentation root)) L) := by150 classical151 simpa [PureState.selectedEmbedding] using152 (exists_irreducible_atomicShellModel153 (PureState.selectedRepresentation root)154 (PureState.isIrreducible_selectedRepresentation root)155 (fun {i j} hij e ↦156 PureState.no_unitaryIntertwiner_selectedRepresentation root hij e)157 root.classOf (PureState.selectedVector root)158 (PureState.norm_selectedVector root)159 W U V hU hV hU0 hV0 hInitial hFinal hUinf hVinf)160161end AtomicConstruction162163end MathlibAnnex.CStarAlgebra