Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/TracialCyclic.lean, lines 104–141.
Back to Pointed unitary transport between trace-cyclic target representations
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.AtomicEndpoint 2import MathlibAnnex.Analysis.CStarAlgebra.CAR.TraceFlag 3import MathlibAnnex.Analysis.CStarAlgebra.AtomicConstruction.GeneratedReduction 4import MathlibAnnex.Analysis.InnerProductSpace.Reduction 5 6/-! 7# A trace-cyclic subspace reduces the same concrete target 8 9This is the connection to the already constructed algebra. We do not infer 10a universal mapping property from the finite shell relations. Instead, an 11existing representation of the actual target is used, and its source-cyclic 12subspace is shown to reduce every target generator and its adjoint. 13-/ 14 15set_option autoImplicit false 16 17open Filter Topology 18open scoped InnerProduct 19 20namespace MathlibAnnex.CStarAlgebra.CAR 21 22open MathlibAnnex.Analysis.CStarAlgebra 23 24universe v 25variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 26 27/-- An actual added generator of the fixed shell-family target. -/ 28noncomputable def shellFamilyGenerator (family : RepresentativeShellFamily) 29 (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : ShellFamilyTarget family := 30 MathlibAnnex.CStarAlgebra.AtomicConstruction.generator 31 selectedAtomicRepresentation (shellFamilyLinks family) i 32 33/-- The generator is unitary as an element of the actual target, not only 34as an operator in its ambient realization. -/ 35theorem shellFamilyGenerator_mem_unitary (family : RepresentativeShellFamily) 36 (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : 37 shellFamilyGenerator family i ∈ unitary (ShellFamilyTarget family) := by 38 rw [Unitary.mem_iff] 39 constructor 40 · apply Subtype.ext 41 exact (shellFamilyLinks_unitary family i).1 42 · apply Subtype.ext 43 exact (shellFamilyLinks_unitary family i).2 44 45@[simp] 46theorem shellFamilyGenerator_root (family : RepresentativeShellFamily) : 47 shellFamilyGenerator family completedRootPureState.classOf = 1 := by 48 apply Subtype.ext 49 exact shellFamilyLinks_root family 50 51/-- A compact interface for the inherited five-operator reconstruction: 52on the trace-cyclic subspace, both residual terms vanish. -/ 53theorem exists_shell_sums_eq_on_cyclicSubspace (family : RepresentativeShellFamily) 54 (ρ : Representation (ShellFamilyTarget family) H) (ξ : H) 55 (hξ : ∀ a, Representation.vectorFunctional 56 (ρ.comp (shellFamilySourceHom family)) ξ a = trace a) 57 (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : 58 let σ := ρ.comp (shellFamilySourceHom family) 59 let M := Representation.cyclicSubspace σ ξ 60 ∃ S T : H →L[ℂ] H, 61 ContinuousLinearMap.StronglyConverges 62 (ContinuousLinearMap.partialSum 63 (fun n ↦ σ ((representativeShellData family i).link n))) atTop S ∧ 64 ContinuousLinearMap.StronglyConverges 65 (ContinuousLinearMap.partialSum 66 (fun n ↦ (σ ((representativeShellData family i).link n))†)) atTop T ∧ 67 ‖S‖ ≤ 1 ∧ ‖T‖ ≤ 1 ∧ T = S† ∧ 68 ∀ x ∈ M, ρ (shellFamilyGenerator family i) x = S x ∧ 69 ((ρ (shellFamilyGenerator family i))†) x = T x := by 70 dsimp only 71 let σ := ρ.comp (shellFamilySourceHom family) 72 let M := Representation.cyclicSubspace σ ξ 73 obtain ⟨S, T, P, Q, R, hS, hT, hSnorm, hTnorm, hAdj, 74 hP, hPrange, hQ, hQrange, _, _, hgen, hR, _, _, hsupport, _⟩ := 75 exists_targetShellReconstruction family (shellFamilyLinks family) 76 (shellFamilyLinks_unitary family) (shellFamilyLinks_sourceShell family) ρ i 77 have hPzero : ∀ x ∈ M, P x = 0 := 78 projection_eq_zero_on_cyclicSubspace σ ξ (transportedFlag family i) 79 (isStarProjection_transportedFlag family i) 80 (tendsto_transportedFlag_orbit_zero family i σ ξ hξ) P hP hPrange 81 have hQzero : ∀ x ∈ M, Q x = 0 := 82 projection_eq_zero_on_cyclicSubspace σ ξ rootFlag isStarProjection_rootFlag 83 (tendsto_rootFlag_orbit_zero σ ξ hξ) Q hQ hQrange 84 change ρ (shellFamilyGenerator family i) = S + R at hgen 85 change R = (ρ (shellFamilyGenerator family i)).comp P at hR 86 have hRzero (x : H) (hx : x ∈ M) : R x = 0 := by 87 rw [hR, ContinuousLinearMap.comp_apply, hPzero x hx, map_zero] 88 have hstar : star R = P * star R * Q := by 89 change R = Q * R * P at hsupport 90 have h := congrArg star hsupport 91 simpa only [star_mul, hP.isSelfAdjoint.star_eq, hQ.isSelfAdjoint.star_eq, 92 mul_assoc] using h 93 have hRadjoint_zero (x : H) (hx : x ∈ M) : (R†) x = 0 := by 94 rw [← ContinuousLinearMap.star_eq_adjoint, hstar] 95 change P ((star R) (Q x)) = 0 96 rw [hQzero x hx, map_zero, map_zero] 97 refine ⟨S, T, hS, hT, hSnorm, hTnorm, hAdj, ?_⟩ 98 intro x hx 99 constructor 100 · rw [hgen, ContinuousLinearMap.add_apply, hRzero x hx, add_zero] 101 · rw [hgen, map_add, ContinuousLinearMap.add_apply, 102 hRadjoint_zero x hx, add_zero, ← hAdj] 103 104/-- No target irreducibility is used: the source trace alone makes the 105source-cyclic subspace reducing for the actual target. -/ 106theorem reduces_cyclicSubspace_of_trace (family : RepresentativeShellFamily) 107 (ρ : Representation (ShellFamilyTarget family) H) (ξ : H) 108 (hξ : ∀ a, Representation.vectorFunctional 109 (ρ.comp (shellFamilySourceHom family)) ξ a = trace a) : 110 ρ.Reduces (Representation.cyclicSubspace 111 (ρ.comp (shellFamilySourceHom family)) ξ) := by 112 let σ := ρ.comp (shellFamilySourceHom family) 113 let M := Representation.cyclicSubspace σ ξ 114 have hMclosed : IsClosed (M : Set H) := Representation.isClosed_cyclicSubspace σ ξ 115 have hsource (a : Limit) : 116 M.Reduces (ρ (shellFamilySourceHom family a)) := by 117 constructor 118 · intro x hx 119 exact Representation.map_mem_cyclicSubspace σ ξ a hx 120 · intro x hx 121 exact Representation.adjoint_mem_cyclicSubspace σ ξ a hx 122 have hgenerator (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : 123 M.Reduces (ρ (shellFamilyGenerator family i)) := by 124 obtain ⟨S, T, hS, hT, _, _, hAdj, heq⟩ := 125 exists_shell_sums_eq_on_cyclicSubspace family ρ ξ hξ i 126 have hW (n : ℕ) : M.Reduces (σ ((representativeShellData family i).link n)) := 127 hsource ((representativeShellData family i).link n) 128 have hSreduce : M.Reduces S := 129 Submodule.Reduces.of_stronglyConverges_partialSum hMclosed hW hS hT hAdj 130 constructor 131 · intro x hx 132 rw [(heq x hx).1] 133 exact hSreduce.1 hx 134 · intro x hx 135 rw [(heq x hx).2, hAdj] 136 exact hSreduce.2 hx 137 have hall := MathlibAnnex.CStarAlgebra.AtomicConstruction.reduces_concreteTarget_of_generators 138 selectedAtomicRepresentation (shellFamilyLinks family) ρ M hMclosed hsource hgenerator 139 refine ⟨hMclosed, ?_⟩ 140 intro a x hx 141 exact ⟨(hall a).1 hx, (hall a).2 hx⟩ 142 143/-- In a cyclic representation extending the source trace, source cyclicity 144already equals target cyclicity. -/ 145theorem cyclicSubspace_eq_top_of_trace_of_cyclic (family : RepresentativeShellFamily) 146 (ρ : Representation (ShellFamilyTarget family) H) (ξ : H) 147 (hξ : ∀ a, Representation.vectorFunctional 148 (ρ.comp (shellFamilySourceHom family)) ξ a = trace a) 149 (hcyclic : DenseRange (fun a ↦ ρ a ξ)) : 150 Representation.cyclicSubspace (ρ.comp (shellFamilySourceHom family)) ξ = ⊤ := by 151 let σ := ρ.comp (shellFamilySourceHom family) 152 let M := Representation.cyclicSubspace σ ξ 153 have hreduce := reduces_cyclicSubspace_of_trace family ρ ξ hξ 154 have hmem : ξ ∈ M := Representation.self_mem_cyclicSubspace σ ξ 155 apply top_unique 156 intro x _ 157 have hsubset : Set.range (fun a ↦ ρ a ξ) ⊆ (M : Set H) := by 158 rintro _ ⟨a, rfl⟩ 159 exact (hreduce.2 a ξ hmem).1 160 apply closure_minimal hsubset hreduce.1 161 rw [hcyclic.closure_range] 162 exact Set.mem_univ x 163 164theorem denseRange_source_orbit_of_trace_of_cyclic (family : RepresentativeShellFamily) 165 (ρ : Representation (ShellFamilyTarget family) H) (ξ : H) 166 (hξ : ∀ a, Representation.vectorFunctional 167 (ρ.comp (shellFamilySourceHom family)) ξ a = trace a) 168 (hcyclic : DenseRange (fun a ↦ ρ a ξ)) : 169 DenseRange (fun b ↦ ρ (shellFamilySourceHom family b) ξ) := by 170 have htop := cyclicSubspace_eq_top_of_trace_of_cyclic family ρ ξ hξ hcyclic 171 have hsets := congrArg (fun M : Submodule ℂ H ↦ (M : Set H)) htop 172 apply dense_iff_closure_eq.mpr 173 simpa [Representation.cyclicSubspace, Submodule.topologicalClosure_coe, 174 LinearMap.coe_range, Representation.orbitLinearMap] using hsets 175 176/-- Separability comes from the actual CAR orbit; the full target algebra is 177not assumed norm separable. -/ 178theorem separableSpace_of_trace_of_cyclic (family : RepresentativeShellFamily) 179 (ρ : Representation (ShellFamilyTarget family) H) (ξ : H) 180 (hξ : ∀ a, Representation.vectorFunctional 181 (ρ.comp (shellFamilySourceHom family)) ξ a = trace a) 182 (hcyclic : DenseRange (fun a ↦ ρ a ξ)) : TopologicalSpace.SeparableSpace H := by 183 have hdense := denseRange_source_orbit_of_trace_of_cyclic family ρ ξ hξ hcyclic 184 let σ := ρ.comp (shellFamilySourceHom family) 185 exact hdense.separableSpace 186 (((ContinuousLinearMap.apply ℂ H ξ).comp 187 (Representation.continuousLinearMap σ)).continuous) 188 189end MathlibAnnex.CStarAlgebra.CAR