Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/TracialTransport.lean
Pinned GitHub source · Raw UTF-8 source
Back to Uniqueness among all state extensions of the CAR trace · Back to Pointed unitary transport between trace-cyclic target representations
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.TracialCyclic2import MathlibAnnex.Analysis.CStarAlgebra.AtomicConstruction.GeneratedExt34/-!5# Transport between target-cyclic realizations of the source trace67Source cyclicity is proved, not assumed. The source intertwiner passes to8both strong shell sums, and norm generation then gives target intertwining.9-/1011set_option autoImplicit false1213open Filter Topology14open scoped InnerProduct1516namespace MathlibAnnex.CStarAlgebra.CAR1718open MathlibAnnex.Analysis.CStarAlgebra1920universe v w21variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]22variable {K : Type w} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]2324set_option maxHeartbeats 1000000 in25/-- On a target-cyclic realization of the trace, the source shell sums26converge strongly to the actual represented generator and its adjoint. -/27theorem stronglyConverges_shell_sums_of_trace_of_cyclic28 (family : RepresentativeShellFamily)29 (ρ : Representation (ShellFamilyTarget family) H) (ξ : H)30 (hξ : ∀ a, Representation.vectorFunctional31 (ρ.comp (shellFamilySourceHom family)) ξ a = trace a)32 (hcyclic : DenseRange (fun a ↦ ρ a ξ))33 (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) :34 ContinuousLinearMap.StronglyConverges35 (ContinuousLinearMap.partialSum (fun n ↦36 ρ (shellFamilySourceHom family ((representativeShellData family i).link n))))37 atTop (ρ (shellFamilyGenerator family i)) ∧38 ContinuousLinearMap.StronglyConverges39 (ContinuousLinearMap.partialSum (fun n ↦40 (ρ (shellFamilySourceHom family ((representativeShellData family i).link n)))†))41 atTop ((ρ (shellFamilyGenerator family i))†) := by42 obtain ⟨S, T, hS, hT, _, _, _, heq⟩ :=43 exists_shell_sums_eq_on_cyclicSubspace family ρ ξ hξ i44 have htop := cyclicSubspace_eq_top_of_trace_of_cyclic family ρ ξ hξ hcyclic45 have hall (x : H) : ρ (shellFamilyGenerator family i) x = S x ∧46 ((ρ (shellFamilyGenerator family i))†) x = T x := by47 apply heq x48 rw [htop]49 trivial50 have hS_eq : S = ρ (shellFamilyGenerator family i) :=51 ContinuousLinearMap.ext fun x ↦ (hall x).1.symm52 have hT_eq : T = (ρ (shellFamilyGenerator family i))† :=53 ContinuousLinearMap.ext fun x ↦ (hall x).2.symm54 exact ⟨hS_eq ▸ hS, hT_eq ▸ hT⟩5556private theorem comp_partialSum_eq_partialSum_comp57 (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 := by61 ext x62 simp only [ContinuousLinearMap.comp_apply, ContinuousLinearMap.partialSum_apply, map_sum]63 apply Finset.sum_congr rfl64 intro n _65 exact congrArg (fun T : H →L[ℂ] K ↦ T x) (h n)6667/-- Two cyclic target representations of the source trace are pointed68unitarily equivalent on the whole target, including every added generator. -/69theorem exists_pointed_unitary_of_trace_of_cyclic70 (family : RepresentativeShellFamily)71 (ρ : Representation (ShellFamilyTarget family) H)72 (σ : Representation (ShellFamilyTarget family) K) (ξ : H) (η : K)73 (hξ : ∀ a, Representation.vectorFunctional74 (ρ.comp (shellFamilySourceHom family)) ξ a = trace a)75 (hη : ∀ a, Representation.vectorFunctional76 (σ.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) := by80 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).symm88 obtain ⟨e, he, _⟩ :=89 StarAlgHom.existsUnique_pointedCyclicTransport ρB σB ξ η hdρ hdσ hstate90 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) := by93 have hρsum := (stronglyConverges_shell_sums_of_trace_of_cyclic family ρ ξ hξ hρ i).194 have hσsum := (stronglyConverges_shell_sums_of_trace_of_cyclic family σ η hη hσ i).195 apply ContinuousLinearMap.intertwines_strongLimits (e : H →L[ℂ] K)96 (e : H →L[ℂ] K) hρsum hσsum97 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_generators101 selectedAtomicRepresentation (shellFamilyLinks family) ρ σ e he.2.2 hgen⟩102103end MathlibAnnex.CStarAlgebra.CAR