Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/TracialCyclic.lean
Pinned GitHub source · Raw UTF-8 source
Back to Pointed unitary transport between trace-cyclic target representations
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.AtomicEndpoint2import MathlibAnnex.Analysis.CStarAlgebra.CAR.TraceFlag3import MathlibAnnex.Analysis.CStarAlgebra.AtomicConstruction.GeneratedReduction4import MathlibAnnex.Analysis.InnerProductSpace.Reduction56/-!7# A trace-cyclic subspace reduces the same concrete target89This is the connection to the already constructed algebra. We do not infer10a universal mapping property from the finite shell relations. Instead, an11existing representation of the actual target is used, and its source-cyclic12subspace is shown to reduce every target generator and its adjoint.13-/1415set_option autoImplicit false1617open Filter Topology18open scoped InnerProduct1920namespace MathlibAnnex.CStarAlgebra.CAR2122open MathlibAnnex.Analysis.CStarAlgebra2324universe v25variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]2627/-- 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.generator31 selectedAtomicRepresentation (shellFamilyLinks family) i3233/-- The generator is unitary as an element of the actual target, not only34as 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) := by38 rw [Unitary.mem_iff]39 constructor40 · apply Subtype.ext41 exact (shellFamilyLinks_unitary family i).142 · apply Subtype.ext43 exact (shellFamilyLinks_unitary family i).24445@[simp]46theorem shellFamilyGenerator_root (family : RepresentativeShellFamily) :47 shellFamilyGenerator family completedRootPureState.classOf = 1 := by48 apply Subtype.ext49 exact shellFamilyLinks_root family5051/-- 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.vectorFunctional56 (ρ.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.StronglyConverges62 (ContinuousLinearMap.partialSum63 (fun n ↦ σ ((representativeShellData family i).link n))) atTop S ∧64 ContinuousLinearMap.StronglyConverges65 (ContinuousLinearMap.partialSum66 (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 := by70 dsimp only71 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) ρ i77 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 hPrange81 have hQzero : ∀ x ∈ M, Q x = 0 :=82 projection_eq_zero_on_cyclicSubspace σ ξ rootFlag isStarProjection_rootFlag83 (tendsto_rootFlag_orbit_zero σ ξ hξ) Q hQ hQrange84 change ρ (shellFamilyGenerator family i) = S + R at hgen85 change R = (ρ (shellFamilyGenerator family i)).comp P at hR86 have hRzero (x : H) (hx : x ∈ M) : R x = 0 := by87 rw [hR, ContinuousLinearMap.comp_apply, hPzero x hx, map_zero]88 have hstar : star R = P * star R * Q := by89 change R = Q * R * P at hsupport90 have h := congrArg star hsupport91 simpa only [star_mul, hP.isSelfAdjoint.star_eq, hQ.isSelfAdjoint.star_eq,92 mul_assoc] using h93 have hRadjoint_zero (x : H) (hx : x ∈ M) : (R†) x = 0 := by94 rw [← ContinuousLinearMap.star_eq_adjoint, hstar]95 change P ((star R) (Q x)) = 096 rw [hQzero x hx, map_zero, map_zero]97 refine ⟨S, T, hS, hT, hSnorm, hTnorm, hAdj, ?_⟩98 intro x hx99 constructor100 · 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]103104/-- No target irreducibility is used: the source trace alone makes the105source-cyclic subspace reducing for the actual target. -/106theorem reduces_cyclicSubspace_of_trace (family : RepresentativeShellFamily)107 (ρ : Representation (ShellFamilyTarget family) H) (ξ : H)108 (hξ : ∀ a, Representation.vectorFunctional109 (ρ.comp (shellFamilySourceHom family)) ξ a = trace a) :110 ρ.Reduces (Representation.cyclicSubspace111 (ρ.comp (shellFamilySourceHom family)) ξ) := by112 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)) := by117 constructor118 · intro x hx119 exact Representation.map_mem_cyclicSubspace σ ξ a hx120 · intro x hx121 exact Representation.adjoint_mem_cyclicSubspace σ ξ a hx122 have hgenerator (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) :123 M.Reduces (ρ (shellFamilyGenerator family i)) := by124 obtain ⟨S, T, hS, hT, _, _, hAdj, heq⟩ :=125 exists_shell_sums_eq_on_cyclicSubspace family ρ ξ hξ i126 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 hAdj130 constructor131 · intro x hx132 rw [(heq x hx).1]133 exact hSreduce.1 hx134 · intro x hx135 rw [(heq x hx).2, hAdj]136 exact hSreduce.2 hx137 have hall := MathlibAnnex.CStarAlgebra.AtomicConstruction.reduces_concreteTarget_of_generators138 selectedAtomicRepresentation (shellFamilyLinks family) ρ M hMclosed hsource hgenerator139 refine ⟨hMclosed, ?_⟩140 intro a x hx141 exact ⟨(hall a).1 hx, (hall a).2 hx⟩142143/-- In a cyclic representation extending the source trace, source cyclicity144already equals target cyclicity. -/145theorem cyclicSubspace_eq_top_of_trace_of_cyclic (family : RepresentativeShellFamily)146 (ρ : Representation (ShellFamilyTarget family) H) (ξ : H)147 (hξ : ∀ a, Representation.vectorFunctional148 (ρ.comp (shellFamilySourceHom family)) ξ a = trace a)149 (hcyclic : DenseRange (fun a ↦ ρ a ξ)) :150 Representation.cyclicSubspace (ρ.comp (shellFamilySourceHom family)) ξ = ⊤ := by151 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_unique156 intro x _157 have hsubset : Set.range (fun a ↦ ρ a ξ) ⊆ (M : Set H) := by158 rintro _ ⟨a, rfl⟩159 exact (hreduce.2 a ξ hmem).1160 apply closure_minimal hsubset hreduce.1161 rw [hcyclic.closure_range]162 exact Set.mem_univ x163164theorem denseRange_source_orbit_of_trace_of_cyclic (family : RepresentativeShellFamily)165 (ρ : Representation (ShellFamilyTarget family) H) (ξ : H)166 (hξ : ∀ a, Representation.vectorFunctional167 (ρ.comp (shellFamilySourceHom family)) ξ a = trace a)168 (hcyclic : DenseRange (fun a ↦ ρ a ξ)) :169 DenseRange (fun b ↦ ρ (shellFamilySourceHom family b) ξ) := by170 have htop := cyclicSubspace_eq_top_of_trace_of_cyclic family ρ ξ hξ hcyclic171 have hsets := congrArg (fun M : Submodule ℂ H ↦ (M : Set H)) htop172 apply dense_iff_closure_eq.mpr173 simpa [Representation.cyclicSubspace, Submodule.topologicalClosure_coe,174 LinearMap.coe_range, Representation.orbitLinearMap] using hsets175176/-- Separability comes from the actual CAR orbit; the full target algebra is177not assumed norm separable. -/178theorem separableSpace_of_trace_of_cyclic (family : RepresentativeShellFamily)179 (ρ : Representation (ShellFamilyTarget family) H) (ξ : H)180 (hξ : ∀ a, Representation.vectorFunctional181 (ρ.comp (shellFamilySourceHom family)) ξ a = trace a)182 (hcyclic : DenseRange (fun a ↦ ρ a ξ)) : TopologicalSpace.SeparableSpace H := by183 have hdense := denseRange_source_orbit_of_trace_of_cyclic family ρ ξ hξ hcyclic184 let σ := ρ.comp (shellFamilySourceHom family)185 exact hdense.separableSpace186 (((ContinuousLinearMap.apply ℂ H ξ).comp187 (Representation.continuousLinearMap σ)).continuous)188189end MathlibAnnex.CStarAlgebra.CAR