Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/TracialRepresentation.lean
Pinned GitHub source · Raw UTF-8 source
Back to Faithfulness of the representation on the CAR trace Hilbert space · Back to Faithfulness of the representation on the CAR trace Hilbert space · Back to Faithfulness of the target-state GNS representation
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.TracialCyclic2import MathlibAnnex.Analysis.CStarAlgebra.State.ExtensionOfEmbedding3import MathlibAnnex.Analysis.CStarAlgebra.Representation.SimpleFaithful45/-!6# A separable faithful representation of the same shell-family target78The state is extended onto the existing concrete algebra before any new9representation is introduced. Its ordinary GNS representation is then proved10separable, and the already established closed-ideal dichotomy proves it11faithful. No irreducibility of this representation is assumed.12-/1314set_option autoImplicit false1516open scoped ComplexOrder InnerProduct1718namespace MathlibAnnex.CStarAlgebra.CAR1920open MathlibAnnex.Analysis.CStarAlgebra2122/-- 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_le2930/-- 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)3435theorem traceExtension_mem_stateSpace (family : RepresentativeShellFamily) :36 traceExtension family ∈37 MathlibAnnex.Analysis.CStarAlgebra.stateSpace (ShellFamilyTarget family) :=38 (Classical.choose_spec (exists_state_extension_trace family)).13940@[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 b4445/-- 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)5051@[simp]52theorem traceExtensionPositive_apply (family : RepresentativeShellFamily)53 (a : ShellFamilyTarget family) :54 traceExtensionPositive family a = traceExtension family a := rfl5556@[simp]57theorem traceExtensionPositive_one (family : RepresentativeShellFamily) :58 traceExtensionPositive family 1 = 1 := (traceExtension_mem_stateSpace family).25960/-- The ordinary GNS Hilbert space of the state on the actual target. -/61abbrev TracialHilbertSpace (family : RepresentativeShellFamily) :=62 (traceExtensionPositive family).GNS6364/-- The canonical unit vector of the target-state GNS construction. -/65noncomputable def tracialVector (family : RepresentativeShellFamily) :66 TracialHilbertSpace family := (traceExtensionPositive family).gnsCyclicVector6768/-- 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).gnsStarAlgHom7273@[simp]74theorem norm_tracialVector (family : RepresentativeShellFamily) :75 ‖tracialVector family‖ = 1 :=76 (traceExtensionPositive family).norm_gnsCyclicVector (traceExtensionPositive_one family)7778theorem tracialVector_ne_zero (family : RepresentativeShellFamily) :79 tracialVector family ≠ 0 := by80 intro hzero81 have h := norm_tracialVector family82 rw [hzero, norm_zero] at h83 exact zero_ne_one h8485/-- 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)8990@[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 a9697/-- The source restriction implements the original CAR trace exactly. -/98theorem vectorFunctional_tracialRepresentation_source (family : RepresentativeShellFamily)99 (b : Limit) :100 Representation.vectorFunctional101 ((tracialRepresentation family).comp (shellFamilySourceHom family))102 (tracialVector family) b = trace b := by103 change inner ℂ (tracialVector family)104 (tracialRepresentation family (shellFamilySourceHom family b) (tracialVector family)) = _105 rw [inner_tracialVector_tracialRepresentation, traceExtension_shellFamilySourceHom]106107theorem denseRange_tracialRepresentation_orbit (family : RepresentativeShellFamily) :108 DenseRange (fun a ↦ tracialRepresentation family a (tracialVector family)) :=109 (traceExtensionPositive family).denseRange_gnsStarAlgHom_apply_gnsCyclicVector110111/-- 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 family115 (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)119120theorem 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)125126/-- Faithfulness follows from the previously proved ideal dichotomy of the127same target, after the representation has actually been constructed. -/128theorem tracialRepresentation_injective (family : RepresentativeShellFamily) :129 Function.Injective (tracialRepresentation family) := by130 letI : Nontrivial (TracialHilbertSpace family) := nontrivial_tracialHilbertSpace family131 exact Representation.injective_of_closed_ideal_dichotomy132 (shellFamilyTarget_closedIdeal_dichotomy family) (tracialRepresentation family)133134theorem 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))139140end MathlibAnnex.CStarAlgebra.CAR