Exact source view. Private integrated preview.
Exact declaration: MathlibAnnex.CStarAlgebra.CAR.existsUnique_tracial_state
MathlibAnnex/Analysis/CStarAlgebra/CAR/TraceState.lean · lines 70–79
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.TraceExtensionTracial 2import MathlibAnnex.Analysis.CStarAlgebra.CAR.TraceUnique 3import MathlibAnnex.Analysis.CStarAlgebra.GNS.TracialFaithfulness 4 5/-! 6# The faithful unique tracial state of the fixed shell-family target 7 8Faithfulness uses the trace identity and the faithful cyclic representation. 9Uniqueness among all tracial states follows by restriction to the completed 10CAR algebra and the stronger uniqueness theorem for state extensions. 11-/ 12 13set_option autoImplicit false 14 15open scoped ComplexOrder InnerProduct 16 17namespace MathlibAnnex.CStarAlgebra.CAR 18 19open MathlibAnnex.Analysis.CStarAlgebra 20 21/-- The extended trace detects every nonzero square. This is faithfulness 22of the state, not merely injectivity of its representation. -/ 23theorem traceExtension_star_mul_self_eq_zero_iff 24 (family : RepresentativeShellFamily) (a : ShellFamilyTarget family) : 25 traceExtension family (star a * a) = 0 ↔ a = 0 := by 26 constructor 27 · intro ha 28 apply eq_zero_of_apply_star_mul_self_eq_zero_of_tracial 29 (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 ha 36 · rintro rfl 37 simp only [star_zero, zero_mul, map_zero] 38 39set_option maxHeartbeats 1000000 in 40/-- Every normalized continuous trace on the target restricts to the 41original normalized trace on CAR. -/ 42theorem apply_shellFamilySourceHom_eq_trace_of_apply_one_of_mul_comm 43 (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 := by 47 let j := shellFamilySourceHom family 48 let ψ : Limit →L[ℂ] ℂ := 49 { toLinearMap := φ.toLinearMap.comp j.toLinearMap 50 cont := φ.continuous.comp (map_continuous j) } 51 have hψ1 : ψ 1 = 1 := by 52 change φ (j 1) = 1 53 rw [map_one, hφ1] 54 have hψ (a b : Limit) : ψ (a * b) = ψ (b * a) := by 55 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) heq 60 61/-- There is no other tracial state of the target. -/ 62theorem eq_traceExtension_of_mem_stateSpace_of_mul_comm 63 (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 := by 67 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φtrace 69 70/-- The existing target has exactly one tracial state. Faithfulness is proved 71separately 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) := by 76 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φ.2 80 81end MathlibAnnex.CStarAlgebra.CAR