Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/TraceExtensionTracial.lean, lines 111–123.
Back to The unique trace extension is tracial on the whole target
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.TraceExtensionUnique 2import MathlibAnnex.Analysis.CStarAlgebra.State.Centralizer 3import Mathlib.Analysis.CStarAlgebra.Unitary.Span 4 5/-! 6# The unique extension is tracial on the entire target 7 8Uniqueness makes the extension invariant under source unitary conjugation. 9Source unitaries span CAR. Strong shell sums then put every added generator 10in the state centralizer, and norm generation completes the argument. 11-/ 12 13set_option autoImplicit false 14 15open Filter Topology 16open scoped ComplexOrder InnerProduct 17 18namespace MathlibAnnex.CStarAlgebra.CAR 19 20open MathlibAnnex.Analysis.CStarAlgebra 21 22private theorem trace_star_unitary_mul_mul (u : unitary Limit) (b : Limit) : 23 trace (star (u : Limit) * b * (u : Limit)) = trace b := by 24 rw [trace_mul_comm (star (u : Limit) * b) (u : Limit), ← mul_assoc, 25 u.property.2, one_mul] 26 27/-- 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 := by 31 ext a 32 exact inner_tracialVector_tracialRepresentation family a 33 34set_option maxHeartbeats 5000000 in 35/-- 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 family 39 (star (shellFamilySourceHom family (u : Limit)) * a * 40 shellFamilySourceHom family (u : Limit)) = traceExtension family a := by 41 let ζ := tracialRepresentation family 42 (shellFamilySourceHom family (u : Limit)) (tracialVector family) 43 let ψ := Representation.vectorFunctional (tracialRepresentation family) ζ 44 have hζ : ‖ζ‖ = 1 := by 45 change ‖((tracialRepresentation family).comp (shellFamilySourceHom family)) 46 (u : Limit) (tracialVector family)‖ = 1 47 rw [(((tracialRepresentation family).comp (shellFamilySourceHom family)) 48 (u : Limit)).norm_map_of_mem_unitary 49 (Unitary.map_mem ((tracialRepresentation family).comp 50 (shellFamilySourceHom family)) u.property)] 51 exact norm_tracialVector family 52 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 := by 56 change Representation.vectorFunctional (tracialRepresentation family) 57 (tracialRepresentation family (shellFamilySourceHom family (u : Limit)) 58 (tracialVector family)) (shellFamilySourceHom family b) = trace b 59 calc 60 _ = 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 family 68 (star (shellFamilySourceHom family (u : Limit)) * 69 shellFamilySourceHom family b * shellFamilySourceHom family (u : Limit)) := by 70 rw [vectorFunctional_tracialRepresentation] 71 _ = trace (star (u : Limit) * b * (u : Limit)) := by 72 rw [← map_star, ← map_mul, ← map_mul, traceExtension_shellFamilySourceHom] 73 _ = trace b := trace_star_unitary_mul_mul u b 74 have hψ : ψ = traceExtension family := 75 eq_traceExtension_of_mem_stateSpace_of_apply_shellFamilySourceHom_eq_trace family ψ hψstate hψsource 76 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 hvalue 80 calc 81 traceExtension family 82 (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)) := by 87 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).symm 93 _ = traceExtension family a := hvalue 94 95set_option maxHeartbeats 1000000 in 96private 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)) := by 100 let v := shellFamilySourceHom family (u : Limit) 101 have hv : star v * v = 1 := by 102 change star (shellFamilySourceHom family (u : Limit)) * 103 shellFamilySourceHom family (u : Limit) = 1 104 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 h 107 rw [← mul_assoc (star v) v a, hv, one_mul] at h 108 exact h.symm 109 110set_option maxHeartbeats 1000000 in 111/-- Every source element, not just source unitaries, lies in the full state's 112centralizer. -/ 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) := by 117 obtain ⟨u, c, hb, _⟩ := CStarAlgebra.exists_sum_four_unitary b 118 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 rfl 122 intro i _ 123 rw [traceExtension_unitary_mul] 124 125set_option maxHeartbeats 1000000 in 126/-- A generator is in the centralizer by the source shell approximants in 127this 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) := by 133 let x : ℕ → ShellFamilyTarget family := fun N ↦ shellFamilySourceHom family 134 (∑ n ∈ Finset.range N, (representativeShellData family i).link n) 135 have hx : ContinuousLinearMap.StronglyConverges 136 (fun N ↦ tracialRepresentation family (x N)) atTop 137 (tracialRepresentation family (shellFamilyGenerator family i)) := by 138 have hfamily : (fun N ↦ tracialRepresentation family (x N)) = 139 ContinuousLinearMap.partialSum (fun n ↦ 140 tracialRepresentation family 141 (shellFamilySourceHom family ((representativeShellData family i).link n))) := by 142 funext N 143 simp only [x, map_sum, ContinuousLinearMap.partialSum] 144 rw [hfamily] 145 exact (stronglyConverges_shell_sums_of_trace_of_cyclic family 146 (tracialRepresentation family) (tracialVector family) 147 (vectorFunctional_tracialRepresentation_source family) 148 (denseRange_tracialRepresentation_orbit family) i).1 149 have heq (N : ℕ) : Representation.vectorFunctional 150 (tracialRepresentation family) (tracialVector family) (x N * a) = 151 Representation.vectorFunctional (tracialRepresentation family) (tracialVector family) 152 (a * x N) := by 153 rw [vectorFunctional_tracialRepresentation] 154 exact traceExtension_shellFamilySourceHom_mul family _ a 155 have h := vectorFunctional_mul_eq_mul_of_stronglyConverges 156 (tracialRepresentation family) (tracialVector family) x 157 (shellFamilyGenerator family i) a hx heq 158 simpa only [vectorFunctional_tracialRepresentation] using h 159 160set_option maxHeartbeats 1000000 in 161/-- The unique state extension of the CAR trace is a trace on the whole 162previously constructed target. -/ 163theorem traceExtension_mul_comm (family : RepresentativeShellFamily) 164 (a b : ShellFamilyTarget family) : 165 traceExtension family (a * b) = traceExtension family (b * a) := by 166 let C := stateCentralizer (traceExtension family) (traceExtension_mem_stateSpace family) 167 have htop : C = ⊤ := 168 MathlibAnnex.CStarAlgebra.AtomicConstruction.eq_top_of_source_mem_of_generator_mem 169 selectedAtomicRepresentation (shellFamilyLinks family) C 170 (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]; trivial 174 exact ha b 175 176end MathlibAnnex.CStarAlgebra.CAR