Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/TracialRepresentation.lean, lines 85–88.
Back to The GNS representation of the target trace extension · Back to Faithfulness of the target-state GNS representation
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.TracialCyclic 2import MathlibAnnex.Analysis.CStarAlgebra.State.ExtensionOfEmbedding 3import MathlibAnnex.Analysis.CStarAlgebra.Representation.SimpleFaithful 4 5/-! 6# A separable faithful representation of the same shell-family target 7 8The state is extended onto the existing concrete algebra before any new 9representation is introduced. Its ordinary GNS representation is then proved 10separable, and the already established closed-ideal dichotomy proves it 11faithful. No irreducibility of this representation is assumed. 12-/ 13 14set_option autoImplicit false 15 16open scoped ComplexOrder InnerProduct 17 18namespace MathlibAnnex.CStarAlgebra.CAR 19 20open MathlibAnnex.Analysis.CStarAlgebra 21 22/-- The CAR trace extends to a state of the actual target. -/ 23theorem exists_state_extension_trace (family : RepresentativeShellFamily) : 24 ∃ φ : ShellFamilyTarget family →L[ℂ] ℂ, 25 φ ∈ MathlibAnnex.Analysis.CStarAlgebra.stateSpace (ShellFamilyTarget family) ∧ 26 ∀ b, φ (shellFamilySourceHom family b) = trace b := 27 exists_state_extension_of_injective (shellFamilySourceHom family) 28 (shellFamilySourceHom_injective family) trace trace_one norm_trace_le 29 30/-- A state extension of the source trace, chosen on the same concrete algebra. -/ 31noncomputable def traceExtension (family : RepresentativeShellFamily) : 32 ShellFamilyTarget family →L[ℂ] ℂ := 33 Classical.choose (exists_state_extension_trace family) 34 35theorem traceExtension_mem_stateSpace (family : RepresentativeShellFamily) : 36 traceExtension family ∈ 37 MathlibAnnex.Analysis.CStarAlgebra.stateSpace (ShellFamilyTarget family) := 38 (Classical.choose_spec (exists_state_extension_trace family)).1 39 40@[simp] 41theorem traceExtension_shellFamilySourceHom (family : RepresentativeShellFamily) (b : Limit) : 42 traceExtension family (shellFamilySourceHom family b) = trace b := 43 (Classical.choose_spec (exists_state_extension_trace family)).2 b 44 45/-- The positive-linear-map bundle of the chosen extension. -/ 46noncomputable def traceExtensionPositive (family : RepresentativeShellFamily) : 47 ShellFamilyTarget family →ₚ[ℂ] ℂ := 48 positiveLinearMapOfMemStateSpace (traceExtension family) 49 (traceExtension_mem_stateSpace family) 50 51@[simp] 52theorem traceExtensionPositive_apply (family : RepresentativeShellFamily) 53 (a : ShellFamilyTarget family) : 54 traceExtensionPositive family a = traceExtension family a := rfl 55 56@[simp] 57theorem traceExtensionPositive_one (family : RepresentativeShellFamily) : 58 traceExtensionPositive family 1 = 1 := (traceExtension_mem_stateSpace family).2 59 60/-- The ordinary GNS Hilbert space of the state on the actual target. -/ 61abbrev TracialHilbertSpace (family : RepresentativeShellFamily) := 62 (traceExtensionPositive family).GNS 63 64/-- The canonical unit vector of the target-state GNS construction. -/ 65noncomputable def tracialVector (family : RepresentativeShellFamily) : 66 TracialHilbertSpace family := (traceExtensionPositive family).gnsCyclicVector 67 68/-- The target's GNS representation, not merely a representation of its CAR source. -/ 69noncomputable def tracialRepresentation (family : RepresentativeShellFamily) : 70 Representation (ShellFamilyTarget family) (TracialHilbertSpace family) := 71 (traceExtensionPositive family).gnsStarAlgHom 72 73@[simp] 74theorem norm_tracialVector (family : RepresentativeShellFamily) : 75 ‖tracialVector family‖ = 1 := 76 (traceExtensionPositive family).norm_gnsCyclicVector (traceExtensionPositive_one family) 77 78theorem tracialVector_ne_zero (family : RepresentativeShellFamily) : 79 tracialVector family ≠ 0 := by 80 intro hzero 81 have h := norm_tracialVector family 82 rw [hzero, norm_zero] at h 83 exact zero_ne_one h 84 85/-- This nontriviality proof remains separate from the representation proof. -/ 86theorem nontrivial_tracialHilbertSpace (family : RepresentativeShellFamily) : 87 Nontrivial (TracialHilbertSpace family) := 88 nontrivial_of_ne (tracialVector family) 0 (tracialVector_ne_zero family) 89 90@[simp] 91theorem inner_tracialVector_tracialRepresentation (family : RepresentativeShellFamily) 92 (a : ShellFamilyTarget family) : 93 inner ℂ (tracialVector family) (tracialRepresentation family a (tracialVector family)) = 94 traceExtension family a := 95 (traceExtensionPositive family).inner_gnsCyclicVector_gnsStarAlgHom a 96 97/-- The source restriction implements the original CAR trace exactly. -/ 98theorem vectorFunctional_tracialRepresentation_source (family : RepresentativeShellFamily) 99 (b : Limit) : 100 Representation.vectorFunctional 101 ((tracialRepresentation family).comp (shellFamilySourceHom family)) 102 (tracialVector family) b = trace b := by 103 change inner ℂ (tracialVector family) 104 (tracialRepresentation family (shellFamilySourceHom family b) (tracialVector family)) = _ 105 rw [inner_tracialVector_tracialRepresentation, traceExtension_shellFamilySourceHom] 106 107theorem denseRange_tracialRepresentation_orbit (family : RepresentativeShellFamily) : 108 DenseRange (fun a ↦ tracialRepresentation family a (tracialVector family)) := 109 (traceExtensionPositive family).denseRange_gnsStarAlgHom_apply_gnsCyclicVector 110 111/-- The CAR orbit, although smaller than the target orbit algebraically, 112is already dense in this Hilbert space. -/ 113theorem denseRange_tracialRepresentation_source_orbit (family : RepresentativeShellFamily) : 114 DenseRange (fun b ↦ tracialRepresentation family 115 (shellFamilySourceHom family b) (tracialVector family)) := 116 denseRange_source_orbit_of_trace_of_cyclic family (tracialRepresentation family) 117 (tracialVector family) (vectorFunctional_tracialRepresentation_source family) 118 (denseRange_tracialRepresentation_orbit family) 119 120theorem separableSpace_tracialHilbertSpace (family : RepresentativeShellFamily) : 121 TopologicalSpace.SeparableSpace (TracialHilbertSpace family) := 122 separableSpace_of_trace_of_cyclic family (tracialRepresentation family) 123 (tracialVector family) (vectorFunctional_tracialRepresentation_source family) 124 (denseRange_tracialRepresentation_orbit family) 125 126/-- Faithfulness follows from the previously proved ideal dichotomy of the 127same target, after the representation has actually been constructed. -/ 128theorem tracialRepresentation_injective (family : RepresentativeShellFamily) : 129 Function.Injective (tracialRepresentation family) := by 130 letI : Nontrivial (TracialHilbertSpace family) := nontrivial_tracialHilbertSpace family 131 exact Representation.injective_of_closed_ideal_dichotomy 132 (shellFamilyTarget_closedIdeal_dichotomy family) (tracialRepresentation family) 133 134theorem isometry_tracialRepresentation (family : RepresentativeShellFamily) : 135 Isometry (tracialRepresentation family) := 136 AddMonoidHomClass.isometry_of_norm (tracialRepresentation family) 137 (NonUnitalStarAlgHom.norm_map (tracialRepresentation family) 138 (tracialRepresentation_injective family)) 139 140end MathlibAnnex.CStarAlgebra.CAR