Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/TracialTransport.lean, lines 25–54.
Back to Pointed unitary transport between trace-cyclic target representations · Back to The unique trace extension is tracial on the whole target
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.TracialCyclic 2import MathlibAnnex.Analysis.CStarAlgebra.AtomicConstruction.GeneratedExt 3 4/-! 5# Transport between target-cyclic realizations of the source trace 6 7Source cyclicity is proved, not assumed. The source intertwiner passes to 8both strong shell sums, and norm generation then gives target intertwining. 9-/ 10 11set_option autoImplicit false 12 13open Filter Topology 14open scoped InnerProduct 15 16namespace MathlibAnnex.CStarAlgebra.CAR 17 18open MathlibAnnex.Analysis.CStarAlgebra 19 20universe v w 21variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 22variable {K : Type w} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] 23 24set_option maxHeartbeats 1000000 in 25/-- On a target-cyclic realization of the trace, the source shell sums 26converge strongly to the actual represented generator and its adjoint. -/ 27theorem stronglyConverges_shell_sums_of_trace_of_cyclic 28 (family : RepresentativeShellFamily) 29 (ρ : Representation (ShellFamilyTarget family) H) (ξ : H) 30 (hξ : ∀ a, Representation.vectorFunctional 31 (ρ.comp (shellFamilySourceHom family)) ξ a = trace a) 32 (hcyclic : DenseRange (fun a ↦ ρ a ξ)) 33 (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : 34 ContinuousLinearMap.StronglyConverges 35 (ContinuousLinearMap.partialSum (fun n ↦ 36 ρ (shellFamilySourceHom family ((representativeShellData family i).link n)))) 37 atTop (ρ (shellFamilyGenerator family i)) ∧ 38 ContinuousLinearMap.StronglyConverges 39 (ContinuousLinearMap.partialSum (fun n ↦ 40 (ρ (shellFamilySourceHom family ((representativeShellData family i).link n)))†)) 41 atTop ((ρ (shellFamilyGenerator family i))†) := by 42 obtain ⟨S, T, hS, hT, _, _, _, heq⟩ := 43 exists_shell_sums_eq_on_cyclicSubspace family ρ ξ hξ i 44 have htop := cyclicSubspace_eq_top_of_trace_of_cyclic family ρ ξ hξ hcyclic 45 have hall (x : H) : ρ (shellFamilyGenerator family i) x = S x ∧ 46 ((ρ (shellFamilyGenerator family i))†) x = T x := by 47 apply heq x 48 rw [htop] 49 trivial 50 have hS_eq : S = ρ (shellFamilyGenerator family i) := 51 ContinuousLinearMap.ext fun x ↦ (hall x).1.symm 52 have hT_eq : T = (ρ (shellFamilyGenerator family i))† := 53 ContinuousLinearMap.ext fun x ↦ (hall x).2.symm 54 exact ⟨hS_eq ▸ hS, hT_eq ▸ hT⟩ 55 56private theorem comp_partialSum_eq_partialSum_comp 57 (e : H →L[ℂ] K) (A : ℕ → H →L[ℂ] H) (B : ℕ → K →L[ℂ] K) 58 (h : ∀ n, e.comp (A n) = (B n).comp e) (N : ℕ) : 59 e.comp (ContinuousLinearMap.partialSum A N) = 60 (ContinuousLinearMap.partialSum B N).comp e := by 61 ext x 62 simp only [ContinuousLinearMap.comp_apply, ContinuousLinearMap.partialSum_apply, map_sum] 63 apply Finset.sum_congr rfl 64 intro n _ 65 exact congrArg (fun T : H →L[ℂ] K ↦ T x) (h n) 66 67/-- Two cyclic target representations of the source trace are pointed 68unitarily equivalent on the whole target, including every added generator. -/ 69theorem exists_pointed_unitary_of_trace_of_cyclic 70 (family : RepresentativeShellFamily) 71 (ρ : Representation (ShellFamilyTarget family) H) 72 (σ : Representation (ShellFamilyTarget family) K) (ξ : H) (η : K) 73 (hξ : ∀ a, Representation.vectorFunctional 74 (ρ.comp (shellFamilySourceHom family)) ξ a = trace a) 75 (hη : ∀ a, Representation.vectorFunctional 76 (σ.comp (shellFamilySourceHom family)) η a = trace a) 77 (hρ : DenseRange (fun a ↦ ρ a ξ)) (hσ : DenseRange (fun a ↦ σ a η)) : 78 ∃ e : H ≃ₗᵢ[ℂ] K, e ξ = η ∧ 79 ∀ a, (e : H →L[ℂ] K).comp (ρ a) = (σ a).comp (e : H →L[ℂ] K) := by 80 let ρB := ρ.comp (shellFamilySourceHom family) 81 let σB := σ.comp (shellFamilySourceHom family) 82 have hdρ : DenseRange (StarAlgHom.orbitMap ρB ξ) := 83 denseRange_source_orbit_of_trace_of_cyclic family ρ ξ hξ hρ 84 have hdσ : DenseRange (StarAlgHom.orbitMap σB η) := 85 denseRange_source_orbit_of_trace_of_cyclic family σ η hη hσ 86 have hstate (a : Limit) : inner ℂ ξ (ρB a ξ) = inner ℂ η (σB a η) := 87 (hξ a).trans (hη a).symm 88 obtain ⟨e, he, _⟩ := 89 StarAlgHom.existsUnique_pointedCyclicTransport ρB σB ξ η hdρ hdσ hstate 90 have hgen (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : 91 (e : H →L[ℂ] K).comp (ρ (shellFamilyGenerator family i)) = 92 (σ (shellFamilyGenerator family i)).comp (e : H →L[ℂ] K) := by 93 have hρsum := (stronglyConverges_shell_sums_of_trace_of_cyclic family ρ ξ hξ hρ i).1 94 have hσsum := (stronglyConverges_shell_sums_of_trace_of_cyclic family σ η hη hσ i).1 95 apply ContinuousLinearMap.intertwines_strongLimits (e : H →L[ℂ] K) 96 (e : H →L[ℂ] K) hρsum hσsum 97 exact comp_partialSum_eq_partialSum_comp _ _ _ 98 (fun n ↦ he.2.2 ((representativeShellData family i).link n)) 99 exact ⟨e, he.2.1, 100 MathlibAnnex.CStarAlgebra.AtomicConstruction.intertwines_of_source_of_generators 101 selectedAtomicRepresentation (shellFamilyLinks family) ρ σ e he.2.2 hgen⟩ 102 103end MathlibAnnex.CStarAlgebra.CAR