Exact source: MathlibAnnex/Analysis/CStarAlgebra/AtomicConstruction/PureAtomic.lean, lines 75–88.
Back to Distinct GNS classes have no unitary intertwiner · Back to An inequivalent GNS fiber has no residual common range · Back to The atomic-shell construction on selected pure-GNS fibers
1import MathlibAnnex.Analysis.CStarAlgebra.PureStateGNS.IrreduciblePure 2import MathlibAnnex.Analysis.CStarAlgebra.AtomicConstruction.AtomicShell 3 4/-! 5# The chosen pure-GNS family as atomic-model source data 6 7This file specializes the generic arbitrary-index shell model to the literal 8root-preserving representatives already selected in `MathlibAnnex.CStarAlgebra.SourceRepresentatives`. 9The remaining flag and shell inputs are representation-local data; no target 10capture statement is assumed. 11-/ 12 13set_option autoImplicit false 14set_option maxHeartbeats 800000 15 16noncomputable section 17 18open Filter Topology 19open scoped ComplexOrder ENNReal lp InnerProduct 20 21namespace MathlibAnnex.CStarAlgebra 22 23universe u 24 25variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] 26 27namespace PureState 28 29/-- The Hilbert fiber of one chosen pure-state GNS representative. -/ 30abbrev SelectedGNS (root : PureState A) (j : GNSClass A) := 31 (representative root j).positiveFunctional.GNS 32 33/-- 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.gnsStarAlgHom 37 38/-- 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.gnsCyclicVector 42 43theorem norm_selectedVector (root : PureState A) (j : GNSClass A) : 44 ‖selectedVector root j‖ = 1 := 45 norm_representative_gnsCyclicVector root j 46 47/-- The canonical vector in a selected GNS fiber realizes its selected pure 48state exactly. -/ 49theorem selected_vectorFunctional (root : PureState A) (j : GNSClass A) : 50 MathlibAnnex.Analysis.CStarAlgebra.Representation.vectorFunctional 51 (selectedRepresentation root j) (selectedVector root j) = 52 (representative root j).1 := by 53 apply ContinuousLinearMap.ext 54 intro a 55 exact PositiveLinearMap.inner_gnsCyclicVector_gnsStarAlgHom 56 (representative root j).positiveFunctional a 57 58noncomputable instance SelectedGNS.instNontrivial 59 (root : PureState A) (j : GNSClass A) : Nontrivial (SelectedGNS root j) := by 60 apply nontrivial_of_ne (selectedVector root j) 0 61 intro hzero 62 have hnorm := congrArg norm hzero 63 simpa [norm_selectedVector] using hnorm 64 65/-- Every chosen pure-GNS fiber is irreducible. -/ 66theorem isIrreducible_selectedRepresentation (root : PureState A) (j : GNSClass A) : 67 StarAlgHom.IsIrreducible (selectedRepresentation root j) := by 68 apply isIrreducible_starAlgHom_of_isPureState 69 (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).2 74 75/-- 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) := by 81 intro he 82 apply hij 83 apply representative_injective_on_classes root 84 refine ⟨e, ?_⟩ 85 intro a x 86 have hx := congrArg 87 (fun T : SelectedGNS root i →L[ℂ] SelectedGNS root j ↦ T x) (he a) 88 simpa [selectedRepresentation, ContinuousLinearMap.comp_apply] using hx 89 90/-- The arbitrary dependent sum of the literal chosen pure-GNS fibers. -/ 91abbrev SelectedAtomicHilbert (root : PureState A) := 92 MathlibAnnex.Analysis.InnerProductSpace.HilbertSum (SelectedGNS root) 93 94/-- Coordinate inclusion using a local classical equality decision. -/ 95noncomputable def selectedEmbedding (root : PureState A) (j : GNSClass A) : 96 SelectedGNS root j →L[ℂ] SelectedAtomicHilbert root := by 97 classical 98 exact MathlibAnnex.Analysis.InnerProductSpace.coordinateEmbedding j 99 100end PureState 101 102namespace AtomicConstruction 103 104open MathlibAnnex.Analysis.CStarAlgebra 105open MathlibAnnex.Analysis.InnerProductSpace 106 107/-- Natural projection-shell data on the chosen pure-GNS family yields the 108actual irreducible atomic model with unitary inter-block generators. -/ 109theorem exists_irreducible_pureAtomicShellModel 110 (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.classOf 133 (PureState.selectedVector root root.classOf)) 134 (PureState.selectedEmbedding root root.classOf 135 (PureState.selectedVector root root.classOf))) : 136 ∃ L : PureState.GNSClass A → 137 PureState.SelectedAtomicHilbert root →L[ℂ] 138 PureState.SelectedAtomicHilbert root, 139 (∀ i, L i ∈ unitary 140 (PureState.SelectedAtomicHilbert root →L[ℂ] 141 PureState.SelectedAtomicHilbert root)) ∧ 142 (∀ i, L i (PureState.selectedEmbedding root i 143 (PureState.selectedVector root i)) = 144 PureState.selectedEmbedding root root.classOf 145 (PureState.selectedVector root root.classOf)) ∧ 146 (∀ i n, (L i).comp (Submodule.projectionShell (U i) n) = W i n) ∧ 147 Representation.IsIrreducible 148 (ambientInclusion 149 (atomicRepresentation (PureState.selectedRepresentation root)) L) := by 150 classical 151 simpa [PureState.selectedEmbedding] using 152 (exists_irreducible_atomicShellModel 153 (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) 160 161end AtomicConstruction 162 163end MathlibAnnex.CStarAlgebra