Exact source: MathlibAnnex/Analysis/CStarAlgebra/State/Centralizer.lean, lines 27–48.
Back to The unique trace extension is tracial on the whole target
1import MathlibAnnex.Analysis.CStarAlgebra.State.Basic 2import MathlibAnnex.Analysis.InnerProductSpace.StrongOperator 3 4/-! 5# The centralizer of a state 6 7Norm-closed star-algebra operations and passage to a represented strong limit 8are separated. No strong continuity of a star homomorphism is asserted. 9-/ 10 11set_option autoImplicit false 12 13open Filter Topology 14open scoped ComplexOrder InnerProduct 15 16namespace MathlibAnnex.Analysis.CStarAlgebra 17 18universe u v 19variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] 20 21/-- A positive state preserves the star operation. -/ 22theorem apply_star_of_mem_stateSpace (φ : A →L[ℂ] ℂ) (hφ : φ ∈ stateSpace A) (a : A) : 23 φ (star a) = star (φ a) := 24 map_star (positiveLinearMapOfMemStateSpace φ hφ) a 25 26/-- Elements which can be moved cyclically through the state. -/ 27def stateCentralizer (φ : A →L[ℂ] ℂ) (hφ : φ ∈ stateSpace A) : StarSubalgebra ℂ A where 28 carrier := {a | ∀ b, φ (a * b) = φ (b * a)} 29 zero_mem' := by intro b; simp 30 one_mem' := by intro b; simp 31 add_mem' := by 32 intro a c ha hc b 33 simp only [add_mul, mul_add, map_add, ha b, hc b] 34 mul_mem' := by 35 intro a c ha hc b 36 calc 37 φ ((a * c) * b) = φ (a * (c * b)) := by rw [mul_assoc] 38 _ = φ ((c * b) * a) := ha _ 39 _ = φ (c * (b * a)) := by rw [mul_assoc] 40 _ = φ ((b * a) * c) := hc _ 41 _ = φ (b * (a * c)) := by rw [mul_assoc] 42 algebraMap_mem' := by 43 intro c b 44 rw [Algebra.commutes c b] 45 star_mem' := by 46 intro a ha b 47 have h := congrArg star (ha (star b)) 48 simpa only [← apply_star_of_mem_stateSpace φ hφ, star_mul, star_star] using h.symm 49 50@[simp] 51theorem mem_stateCentralizer_iff (φ : A →L[ℂ] ℂ) (hφ : φ ∈ stateSpace A) (a : A) : 52 a ∈ stateCentralizer φ hφ ↔ ∀ b, φ (a * b) = φ (b * a) := Iff.rfl 53 54theorem isClosed_stateCentralizer (φ : A →L[ℂ] ℂ) (hφ : φ ∈ stateSpace A) : 55 IsClosed (stateCentralizer φ hφ : Set A) := by 56 change IsClosed {a : A | ∀ b, φ (a * b) = φ (b * a)} 57 simp only [Set.setOf_forall] 58 exact isClosed_iInter fun b ↦ isClosed_eq 59 (φ.continuous.comp (continuous_id.mul continuous_const)) 60 (φ.continuous.comp (continuous_const.mul continuous_id)) 61 62/-- A vector-functional centralizer identity passes to an operator strong 63limit formed in that same representation. -/ 64theorem vectorFunctional_mul_eq_mul_of_stronglyConverges 65 {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 66 (ρ : Representation A H) (ξ : H) (x : ℕ → A) (u a : A) 67 (hx : ContinuousLinearMap.StronglyConverges (fun n ↦ ρ (x n)) atTop (ρ u)) 68 (heq : ∀ n, Representation.vectorFunctional ρ ξ (x n * a) = 69 Representation.vectorFunctional ρ ξ (a * x n)) : 70 Representation.vectorFunctional ρ ξ (u * a) = 71 Representation.vectorFunctional ρ ξ (a * u) := by 72 have hleft : Tendsto (fun n ↦ Representation.vectorFunctional ρ ξ (x n * a)) atTop 73 (nhds (Representation.vectorFunctional ρ ξ (u * a))) := by 74 simpa only [Representation.vectorFunctional_apply, map_mul, mul_apply_eq_comp, 75 Function.comp_def, innerSL_apply_apply] using 76 ((innerSL ℂ ξ).continuous.tendsto (ρ u (ρ a ξ))).comp (hx (ρ a ξ)) 77 have hright : Tendsto (fun n ↦ Representation.vectorFunctional ρ ξ (a * x n)) atTop 78 (nhds (Representation.vectorFunctional ρ ξ (a * u))) := by 79 simpa only [Representation.vectorFunctional_apply, map_mul, mul_apply_eq_comp, 80 Function.comp_def, ContinuousLinearMap.comp_apply, innerSL_apply_apply] using 81 (((innerSL ℂ ξ).comp (ρ a)).continuous.tendsto (ρ u ξ)).comp (hx ξ) 82 exact tendsto_nhds_unique hleft (by simpa only [← heq] using hright) 83 84end MathlibAnnex.Analysis.CStarAlgebra