Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/TraceExtensionTracial.lean
Pinned GitHub source · Raw UTF-8 source
Back to The unique trace extension is tracial on the whole target
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.TraceExtensionUnique2import MathlibAnnex.Analysis.CStarAlgebra.State.Centralizer3import Mathlib.Analysis.CStarAlgebra.Unitary.Span45/-!6# The unique extension is tracial on the entire target78Uniqueness makes the extension invariant under source unitary conjugation.9Source unitaries span CAR. Strong shell sums then put every added generator10in the state centralizer, and norm generation completes the argument.11-/1213set_option autoImplicit false1415open Filter Topology16open scoped ComplexOrder InnerProduct1718namespace MathlibAnnex.CStarAlgebra.CAR1920open MathlibAnnex.Analysis.CStarAlgebra2122private theorem trace_star_unitary_mul_mul (u : unitary Limit) (b : Limit) :23 trace (star (u : Limit) * b * (u : Limit)) = trace b := by24 rw [trace_mul_comm (star (u : Limit) * b) (u : Limit), ← mul_assoc,25 u.property.2, one_mul]2627/-- The vector functional of the chosen target-state GNS is its state. -/28theorem vectorFunctional_tracialRepresentation (family : RepresentativeShellFamily) :29 Representation.vectorFunctional (tracialRepresentation family) (tracialVector family) =30 traceExtension family := by31 ext a32 exact inner_tracialVector_tracialRepresentation family a3334set_option maxHeartbeats 5000000 in35/-- Conjugation by any source unitary fixes the state on the full target. -/36theorem traceExtension_star_unitary_mul_mul (family : RepresentativeShellFamily)37 (u : unitary Limit) (a : ShellFamilyTarget family) :38 traceExtension family39 (star (shellFamilySourceHom family (u : Limit)) * a *40 shellFamilySourceHom family (u : Limit)) = traceExtension family a := by41 let ζ := tracialRepresentation family42 (shellFamilySourceHom family (u : Limit)) (tracialVector family)43 let ψ := Representation.vectorFunctional (tracialRepresentation family) ζ44 have hζ : ‖ζ‖ = 1 := by45 change ‖((tracialRepresentation family).comp (shellFamilySourceHom family))46 (u : Limit) (tracialVector family)‖ = 147 rw [(((tracialRepresentation family).comp (shellFamilySourceHom family))48 (u : Limit)).norm_map_of_mem_unitary49 (Unitary.map_mem ((tracialRepresentation family).comp50 (shellFamilySourceHom family)) u.property)]51 exact norm_tracialVector family52 have hψstate : ψ ∈53 MathlibAnnex.Analysis.CStarAlgebra.stateSpace (ShellFamilyTarget family) :=54 vectorFunctional_mem_stateSpace (tracialRepresentation family) ζ hζ55 have hψsource (b : Limit) : ψ (shellFamilySourceHom family b) = trace b := by56 change Representation.vectorFunctional (tracialRepresentation family)57 (tracialRepresentation family (shellFamilySourceHom family (u : Limit))58 (tracialVector family)) (shellFamilySourceHom family b) = trace b59 calc60 _ = Representation.vectorFunctional (tracialRepresentation family)61 (tracialVector family)62 (star (shellFamilySourceHom family (u : Limit)) *63 shellFamilySourceHom family b * shellFamilySourceHom family (u : Limit)) :=64 Representation.vectorFunctional_map_apply (tracialRepresentation family)65 (tracialVector family) (shellFamilySourceHom family (u : Limit))66 (shellFamilySourceHom family b)67 _ = traceExtension family68 (star (shellFamilySourceHom family (u : Limit)) *69 shellFamilySourceHom family b * shellFamilySourceHom family (u : Limit)) := by70 rw [vectorFunctional_tracialRepresentation]71 _ = trace (star (u : Limit) * b * (u : Limit)) := by72 rw [← map_star, ← map_mul, ← map_mul, traceExtension_shellFamilySourceHom]73 _ = trace b := trace_star_unitary_mul_mul u b74 have hψ : ψ = traceExtension family :=75 eq_traceExtension_of_mem_stateSpace_of_apply_shellFamilySourceHom_eq_trace family ψ hψstate hψsource76 have hvalue := congrArg (fun f : ShellFamilyTarget family →L[ℂ] ℂ ↦ f a) hψ77 change Representation.vectorFunctional (tracialRepresentation family)78 (tracialRepresentation family (shellFamilySourceHom family (u : Limit))79 (tracialVector family)) a = _ at hvalue80 calc81 traceExtension family82 (star (shellFamilySourceHom family (u : Limit)) * a *83 shellFamilySourceHom family (u : Limit)) =84 Representation.vectorFunctional (tracialRepresentation family) (tracialVector family)85 (star (shellFamilySourceHom family (u : Limit)) * a *86 shellFamilySourceHom family (u : Limit)) := by87 rw [vectorFunctional_tracialRepresentation]88 _ = Representation.vectorFunctional (tracialRepresentation family)89 (tracialRepresentation family (shellFamilySourceHom family (u : Limit))90 (tracialVector family)) a :=91 (Representation.vectorFunctional_map_apply (tracialRepresentation family)92 (tracialVector family) (shellFamilySourceHom family (u : Limit)) a).symm93 _ = traceExtension family a := hvalue9495set_option maxHeartbeats 1000000 in96private theorem traceExtension_unitary_mul (family : RepresentativeShellFamily)97 (u : unitary Limit) (a : ShellFamilyTarget family) :98 traceExtension family (shellFamilySourceHom family (u : Limit) * a) =99 traceExtension family (a * shellFamilySourceHom family (u : Limit)) := by100 let v := shellFamilySourceHom family (u : Limit)101 have hv : star v * v = 1 := by102 change star (shellFamilySourceHom family (u : Limit)) *103 shellFamilySourceHom family (u : Limit) = 1104 rw [← map_star, ← map_mul, u.property.1, map_one]105 have h := traceExtension_star_unitary_mul_mul family u (v * a)106 change traceExtension family (star v * (v * a) * v) = _ at h107 rw [← mul_assoc (star v) v a, hv, one_mul] at h108 exact h.symm109110set_option maxHeartbeats 1000000 in111/-- Every source element, not just source unitaries, lies in the full state's112centralizer. -/113theorem traceExtension_shellFamilySourceHom_mul (family : RepresentativeShellFamily)114 (b : Limit) (a : ShellFamilyTarget family) :115 traceExtension family (shellFamilySourceHom family b * a) =116 traceExtension family (a * shellFamilySourceHom family b) := by117 obtain ⟨u, c, hb, _⟩ := CStarAlgebra.exists_sum_four_unitary b118 rw [hb]119 simp only [map_sum, map_smul, Finset.sum_mul, Finset.mul_sum,120 smul_mul_assoc, mul_smul_comm]121 apply Finset.sum_congr rfl122 intro i _123 rw [traceExtension_unitary_mul]124125set_option maxHeartbeats 1000000 in126/-- A generator is in the centralizer by the source shell approximants in127this very GNS representation. -/128theorem traceExtension_shellFamilyGenerator_mul (family : RepresentativeShellFamily)129 (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit)130 (a : ShellFamilyTarget family) :131 traceExtension family (shellFamilyGenerator family i * a) =132 traceExtension family (a * shellFamilyGenerator family i) := by133 let x : ℕ → ShellFamilyTarget family := fun N ↦ shellFamilySourceHom family134 (∑ n ∈ Finset.range N, (representativeShellData family i).link n)135 have hx : ContinuousLinearMap.StronglyConverges136 (fun N ↦ tracialRepresentation family (x N)) atTop137 (tracialRepresentation family (shellFamilyGenerator family i)) := by138 have hfamily : (fun N ↦ tracialRepresentation family (x N)) =139 ContinuousLinearMap.partialSum (fun n ↦140 tracialRepresentation family141 (shellFamilySourceHom family ((representativeShellData family i).link n))) := by142 funext N143 simp only [x, map_sum, ContinuousLinearMap.partialSum]144 rw [hfamily]145 exact (stronglyConverges_shell_sums_of_trace_of_cyclic family146 (tracialRepresentation family) (tracialVector family)147 (vectorFunctional_tracialRepresentation_source family)148 (denseRange_tracialRepresentation_orbit family) i).1149 have heq (N : ℕ) : Representation.vectorFunctional150 (tracialRepresentation family) (tracialVector family) (x N * a) =151 Representation.vectorFunctional (tracialRepresentation family) (tracialVector family)152 (a * x N) := by153 rw [vectorFunctional_tracialRepresentation]154 exact traceExtension_shellFamilySourceHom_mul family _ a155 have h := vectorFunctional_mul_eq_mul_of_stronglyConverges156 (tracialRepresentation family) (tracialVector family) x157 (shellFamilyGenerator family i) a hx heq158 simpa only [vectorFunctional_tracialRepresentation] using h159160set_option maxHeartbeats 1000000 in161/-- The unique state extension of the CAR trace is a trace on the whole162previously constructed target. -/163theorem traceExtension_mul_comm (family : RepresentativeShellFamily)164 (a b : ShellFamilyTarget family) :165 traceExtension family (a * b) = traceExtension family (b * a) := by166 let C := stateCentralizer (traceExtension family) (traceExtension_mem_stateSpace family)167 have htop : C = ⊤ :=168 MathlibAnnex.CStarAlgebra.AtomicConstruction.eq_top_of_source_mem_of_generator_mem169 selectedAtomicRepresentation (shellFamilyLinks family) C170 (isClosed_stateCentralizer _ _)171 (fun c ↦ traceExtension_shellFamilySourceHom_mul family c)172 (fun i ↦ traceExtension_shellFamilyGenerator_mul family i)173 have ha : a ∈ C := by rw [htop]; trivial174 exact ha b175176end MathlibAnnex.CStarAlgebra.CAR