Exact source: MathlibAnnex/Analysis/CStarAlgebra/State/Centralizer.lean
Pinned GitHub source · Raw UTF-8 source
Back to The unique trace extension is tracial on the whole target
1import MathlibAnnex.Analysis.CStarAlgebra.State.Basic2import MathlibAnnex.Analysis.InnerProductSpace.StrongOperator34/-!5# The centralizer of a state67Norm-closed star-algebra operations and passage to a represented strong limit8are separated. No strong continuity of a star homomorphism is asserted.9-/1011set_option autoImplicit false1213open Filter Topology14open scoped ComplexOrder InnerProduct1516namespace MathlibAnnex.Analysis.CStarAlgebra1718universe u v19variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]2021/-- 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φ) a2526/-- Elements which can be moved cyclically through the state. -/27def stateCentralizer (φ : A →L[ℂ] ℂ) (hφ : φ ∈ stateSpace A) : StarSubalgebra ℂ A where28 carrier := {a | ∀ b, φ (a * b) = φ (b * a)}29 zero_mem' := by intro b; simp30 one_mem' := by intro b; simp31 add_mem' := by32 intro a c ha hc b33 simp only [add_mul, mul_add, map_add, ha b, hc b]34 mul_mem' := by35 intro a c ha hc b36 calc37 φ ((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' := by43 intro c b44 rw [Algebra.commutes c b]45 star_mem' := by46 intro a ha b47 have h := congrArg star (ha (star b))48 simpa only [← apply_star_of_mem_stateSpace φ hφ, star_mul, star_star] using h.symm4950@[simp]51theorem mem_stateCentralizer_iff (φ : A →L[ℂ] ℂ) (hφ : φ ∈ stateSpace A) (a : A) :52 a ∈ stateCentralizer φ hφ ↔ ∀ b, φ (a * b) = φ (b * a) := Iff.rfl5354theorem isClosed_stateCentralizer (φ : A →L[ℂ] ℂ) (hφ : φ ∈ stateSpace A) :55 IsClosed (stateCentralizer φ hφ : Set A) := by56 change IsClosed {a : A | ∀ b, φ (a * b) = φ (b * a)}57 simp only [Set.setOf_forall]58 exact isClosed_iInter fun b ↦ isClosed_eq59 (φ.continuous.comp (continuous_id.mul continuous_const))60 (φ.continuous.comp (continuous_const.mul continuous_id))6162/-- A vector-functional centralizer identity passes to an operator strong63limit formed in that same representation. -/64theorem vectorFunctional_mul_eq_mul_of_stronglyConverges65 {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) := by72 have hleft : Tendsto (fun n ↦ Representation.vectorFunctional ρ ξ (x n * a)) atTop73 (nhds (Representation.vectorFunctional ρ ξ (u * a))) := by74 simpa only [Representation.vectorFunctional_apply, map_mul, mul_apply_eq_comp,75 Function.comp_def, innerSL_apply_apply] using76 ((innerSL ℂ ξ).continuous.tendsto (ρ u (ρ a ξ))).comp (hx (ρ a ξ))77 have hright : Tendsto (fun n ↦ Representation.vectorFunctional ρ ξ (a * x n)) atTop78 (nhds (Representation.vectorFunctional ρ ξ (a * u))) := by79 simpa only [Representation.vectorFunctional_apply, map_mul, mul_apply_eq_comp,80 Function.comp_def, ContinuousLinearMap.comp_apply, innerSL_apply_apply] using81 (((innerSL ℂ ξ).comp (ρ a)).continuous.tendsto (ρ u ξ)).comp (hx ξ)82 exact tendsto_nhds_unique hleft (by simpa only [← heq] using hright)8384end MathlibAnnex.Analysis.CStarAlgebra