Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/TraceState.lean
Pinned GitHub source · Raw UTF-8 source
Back to The fixed shell target has a unique tracial state
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.TraceExtensionTracial2import MathlibAnnex.Analysis.CStarAlgebra.CAR.TraceUnique3import MathlibAnnex.Analysis.CStarAlgebra.GNS.TracialFaithfulness45/-!6# The faithful unique tracial state of the fixed shell-family target78Faithfulness uses the trace identity and the faithful cyclic representation.9Uniqueness among all tracial states follows by restriction to the completed10CAR algebra and the stronger uniqueness theorem for state extensions.11-/1213set_option autoImplicit false1415open scoped ComplexOrder InnerProduct1617namespace MathlibAnnex.CStarAlgebra.CAR1819open MathlibAnnex.Analysis.CStarAlgebra2021/-- The extended trace detects every nonzero square. This is faithfulness22of the state, not merely injectivity of its representation. -/23theorem traceExtension_star_mul_self_eq_zero_iff24 (family : RepresentativeShellFamily) (a : ShellFamilyTarget family) :25 traceExtension family (star a * a) = 0 ↔ a = 0 := by26 constructor27 · intro ha28 apply eq_zero_of_apply_star_mul_self_eq_zero_of_tracial29 (traceExtensionPositive family)30 (fun x y ↦ traceExtension_mul_comm family x y)31 (tracialRepresentation family) (tracialVector family)32 (fun x ↦ inner_tracialVector_tracialRepresentation family x)33 (denseRange_tracialRepresentation_orbit family)34 (tracialRepresentation_injective family)35 exact ha36 · rintro rfl37 simp only [star_zero, zero_mul, map_zero]3839set_option maxHeartbeats 1000000 in40/-- Every normalized continuous trace on the target restricts to the41original normalized trace on CAR. -/42theorem apply_shellFamilySourceHom_eq_trace_of_apply_one_of_mul_comm43 (family : RepresentativeShellFamily)44 (φ : ShellFamilyTarget family →L[ℂ] ℂ) (hφ1 : φ 1 = 1)45 (hφ : ∀ a b, φ (a * b) = φ (b * a)) (b : Limit) :46 φ (shellFamilySourceHom family b) = trace b := by47 let j := shellFamilySourceHom family48 let ψ : Limit →L[ℂ] ℂ :=49 { toLinearMap := φ.toLinearMap.comp j.toLinearMap50 cont := φ.continuous.comp (map_continuous j) }51 have hψ1 : ψ 1 = 1 := by52 change φ (j 1) = 153 rw [map_one, hφ1]54 have hψ (a b : Limit) : ψ (a * b) = ψ (b * a) := by55 change φ (j (a * b)) = φ (j (b * a))56 rw [map_mul j, map_mul j]57 exact hφ _ _58 have heq := eq_trace_of_apply_one_of_mul_comm ψ hψ1 hψ59 exact congrArg (fun f : Limit →L[ℂ] ℂ ↦ f b) heq6061/-- There is no other tracial state of the target. -/62theorem eq_traceExtension_of_mem_stateSpace_of_mul_comm63 (family : RepresentativeShellFamily)64 (φ : ShellFamilyTarget family →L[ℂ] ℂ)65 (hφ : φ ∈ MathlibAnnex.Analysis.CStarAlgebra.stateSpace (ShellFamilyTarget family))66 (hφtrace : ∀ a b, φ (a * b) = φ (b * a)) : φ = traceExtension family := by67 apply eq_traceExtension_of_mem_stateSpace_of_apply_shellFamilySourceHom_eq_trace family φ hφ68 exact apply_shellFamilySourceHom_eq_trace_of_apply_one_of_mul_comm family φ hφ.2 hφtrace6970/-- The existing target has exactly one tracial state. Faithfulness is proved71separately above; uniqueness ranges over all states, not just selected extensions. -/72theorem existsUnique_tracial_state (family : RepresentativeShellFamily) :73 ∃! φ : ShellFamilyTarget family →L[ℂ] ℂ,74 φ ∈ MathlibAnnex.Analysis.CStarAlgebra.stateSpace (ShellFamilyTarget family) ∧75 ∀ a b, φ (a * b) = φ (b * a) := by76 refine ⟨traceExtension family,77 ⟨traceExtension_mem_stateSpace family, traceExtension_mul_comm family⟩, ?_⟩78 intro φ hφ79 exact eq_traceExtension_of_mem_stateSpace_of_mul_comm family φ hφ.1 hφ.28081end MathlibAnnex.CStarAlgebra.CAR