Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/SeparableFaithful.lean
Pinned GitHub source · Raw UTF-8 source
Back to A separably represented C*-algebra with no separable irreducible representation
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.TraceGNSModel2import MathlibAnnex.Analysis.CStarAlgebra.CAR.TraceState3import MathlibAnnex.Analysis.CStarAlgebra.CAR.SeparableIrreducible4import MathlibAnnex.Analysis.CStarAlgebra.Representation.CyclicRestriction56/-!7# The separably represented ordinary Naimark endpoint89The carrier remains exactly `AtomicCounterexampleAlgebra`. Its faithful10separable representation is reducible and has no nonzero irreducible closed11subrepresentation. These are separate conclusions from uniqueness of the12abstract irreducible representation class.13-/1415set_option autoImplicit false1617open scoped InnerProduct1819namespace MathlibAnnex.CStarAlgebra.CAR2021open MathlibAnnex.Analysis.CStarAlgebra2223universe v2425/-- The separable Hilbert space for the single previously selected target. -/26abbrev SeparableCounterexampleHilbertSpace := TraceHilbertSpace2728/-- A faithful representation of exactly the existing atomic counterexample29on a separable Hilbert space. -/30noncomputable def separableCounterexampleRepresentation :31 Representation AtomicCounterexampleAlgebra SeparableCounterexampleHilbertSpace :=32 traceModelRepresentation homogeneityShellFamily3334theorem separableSpace_separableCounterexampleHilbertSpace :35 TopologicalSpace.SeparableSpace SeparableCounterexampleHilbertSpace :=36 separableSpace_traceHilbertSpace3738theorem separableCounterexampleRepresentation_injective :39 Function.Injective separableCounterexampleRepresentation :=40 traceModelRepresentation_injective homogeneityShellFamily4142theorem isometry_separableCounterexampleRepresentation :43 Isometry separableCounterexampleRepresentation :=44 isometry_traceModelRepresentation homogeneityShellFamily4546theorem not_isIrreducible_separableCounterexampleRepresentation :47 ¬ Representation.IsIrreducible separableCounterexampleRepresentation := by48 letI : TopologicalSpace.SeparableSpace SeparableCounterexampleHilbertSpace :=49 separableSpace_separableCounterexampleHilbertSpace50 exact not_isIrreducible_of_separable51 separableCounterexampleRepresentation.toNonUnitalStarAlgHom5253/-- Even passing to an arbitrary closed reducing subspace does not yield a54nonzero irreducible subrepresentation. -/55theorem not_isIrreducible_restrictToReducing_separableCounterexampleRepresentation56 (M : Submodule ℂ SeparableCounterexampleHilbertSpace)57 (hM : separableCounterexampleRepresentation.Reduces M) :58 letI : CompleteSpace M := hM.1.completeSpace_coe59 ¬ Representation.IsIrreducible60 (Representation.restrictToReducing separableCounterexampleRepresentation M hM) := by61 letI : CompleteSpace M := hM.1.completeSpace_coe62 letI : TopologicalSpace.SeparableSpace SeparableCounterexampleHilbertSpace :=63 separableSpace_separableCounterexampleHilbertSpace64 letI : TopologicalSpace.SeparableSpace M := inferInstance65 exact not_isIrreducible_of_separable66 (Representation.restrictToReducing67 separableCounterexampleRepresentation M hM).toNonUnitalStarAlgHom6869/-- A closed, fully specified existence statement for the same target;70separability is concluded, not passed as an additional premise. -/71theorem exists_separable_faithful_representation :72 TopologicalSpace.SeparableSpace SeparableCounterexampleHilbertSpace ∧73 ∃ ρ : Representation AtomicCounterexampleAlgebra SeparableCounterexampleHilbertSpace,74 Function.Injective ρ ∧ ¬ ρ.IsIrreducible :=75 ⟨separableSpace_separableCounterexampleHilbertSpace,76 separableCounterexampleRepresentation,77 separableCounterexampleRepresentation_injective,78 not_isIrreducible_separableCounterexampleRepresentation⟩7980/-- The stronger conclusion preserves the entire previously proved81ordinary endpoint, including its independent comparison universe. -/82theorem atomicCounterexampleEndpoint_and_separable_faithful_representation :83 AtomicCounterexampleEndpoint.{v} ∧84 TopologicalSpace.SeparableSpace SeparableCounterexampleHilbertSpace ∧85 Function.Injective separableCounterexampleRepresentation ∧86 ¬ Representation.IsIrreducible separableCounterexampleRepresentation :=87 ⟨shellFamilyEndpoint homogeneityShellFamily, separableSpace_separableCounterexampleHilbertSpace,88 separableCounterexampleRepresentation_injective,89 not_isIrreducible_separableCounterexampleRepresentation⟩9091/-- The unique trace of the unchanged atomic counterexample. -/92noncomputable def atomicCounterexampleTrace : AtomicCounterexampleAlgebra →L[ℂ] ℂ :=93 traceExtension homogeneityShellFamily9495theorem atomicCounterexampleTrace_mem_stateSpace :96 atomicCounterexampleTrace ∈97 MathlibAnnex.Analysis.CStarAlgebra.stateSpace AtomicCounterexampleAlgebra :=98 traceExtension_mem_stateSpace homogeneityShellFamily99100theorem atomicCounterexampleTrace_mul_comm (a b : AtomicCounterexampleAlgebra) :101 atomicCounterexampleTrace (a * b) = atomicCounterexampleTrace (b * a) :=102 traceExtension_mul_comm homogeneityShellFamily a b103104theorem atomicCounterexampleTrace_star_mul_self_eq_zero_iff105 (a : AtomicCounterexampleAlgebra) :106 atomicCounterexampleTrace (star a * a) = 0 ↔ a = 0 :=107 traceExtension_star_mul_self_eq_zero_iff homogeneityShellFamily a108109/-- The trace is implemented by the original CAR trace vector in the110separable faithful model. -/111@[simp]112theorem inner_traceVector_separableCounterexampleRepresentation113 (a : AtomicCounterexampleAlgebra) :114 inner ℂ traceVector (separableCounterexampleRepresentation a traceVector) =115 atomicCounterexampleTrace a :=116 inner_traceVector_traceModelRepresentation homogeneityShellFamily a117118theorem eq_atomicCounterexampleTrace_of_mem_stateSpace_of_mul_comm119 (φ : AtomicCounterexampleAlgebra →L[ℂ] ℂ)120 (hφ : φ ∈ MathlibAnnex.Analysis.CStarAlgebra.stateSpace AtomicCounterexampleAlgebra)121 (hφtrace : ∀ a b, φ (a * b) = φ (b * a)) : φ = atomicCounterexampleTrace :=122 eq_traceExtension_of_mem_stateSpace_of_mul_comm homogeneityShellFamily φ hφ hφtrace123124/-- The final strengthened endpoint uses only previously separated proof125constants. It retains the ordinary endpoint at any comparison universe and126adds the fixed separable faithful model and the faithful unique trace. -/127theorem atomicCounterexampleEndpoint_and_separable_tracial_representation :128 AtomicCounterexampleEndpoint.{v} ∧129 Nontrivial SeparableCounterexampleHilbertSpace ∧130 TopologicalSpace.SeparableSpace SeparableCounterexampleHilbertSpace ∧131 Function.Injective separableCounterexampleRepresentation ∧132 Isometry separableCounterexampleRepresentation ∧133 ¬ Representation.IsIrreducible separableCounterexampleRepresentation ∧134 atomicCounterexampleTrace ∈135 MathlibAnnex.Analysis.CStarAlgebra.stateSpace AtomicCounterexampleAlgebra ∧136 (∀ a b, atomicCounterexampleTrace (a * b) = atomicCounterexampleTrace (b * a)) ∧137 (∀ a, atomicCounterexampleTrace (star a * a) = 0 ↔ a = 0) ∧138 (∀ φ : AtomicCounterexampleAlgebra →L[ℂ] ℂ,139 φ ∈ MathlibAnnex.Analysis.CStarAlgebra.stateSpace AtomicCounterexampleAlgebra →140 (∀ a b, φ (a * b) = φ (b * a)) → φ = atomicCounterexampleTrace) :=141 ⟨shellFamilyEndpoint homogeneityShellFamily,142 nontrivial_traceHilbertSpace,143 separableSpace_separableCounterexampleHilbertSpace,144 separableCounterexampleRepresentation_injective,145 isometry_separableCounterexampleRepresentation,146 not_isIrreducible_separableCounterexampleRepresentation,147 atomicCounterexampleTrace_mem_stateSpace,148 atomicCounterexampleTrace_mul_comm,149 atomicCounterexampleTrace_star_mul_self_eq_zero_iff,150 eq_atomicCounterexampleTrace_of_mem_stateSpace_of_mul_comm⟩151152/-- The same fixed algebra has a faithful representation on a nontrivial separable153Hilbert space, but has no nonzero irreducible representation on any separable154Hilbert space in the arbitrary comparison universe. This does not assert that155the algebra is nonprimitive: the original irreducible model is retained. -/156theorem atomicCounterexampleEndpoint_and_exists_separable_faithful_representation_and_no_separable_irreducible_representation :157 AtomicCounterexampleEndpoint.{v} ∧158 Nontrivial SeparableCounterexampleHilbertSpace ∧159 TopologicalSpace.SeparableSpace SeparableCounterexampleHilbertSpace ∧160 (∃ ρ : Representation AtomicCounterexampleAlgebra SeparableCounterexampleHilbertSpace,161 Function.Injective ρ) ∧162 (∀ (H : Type v) [NormedAddCommGroup H] [InnerProductSpace ℂ H]163 [CompleteSpace H] [TopologicalSpace.SeparableSpace H],164 ∀ ρ : NonUnitalRepresentation (A := AtomicCounterexampleAlgebra) (H := H),165 ¬ ρ.IsIrreducible) := by166 refine ⟨shellFamilyEndpoint homogeneityShellFamily, nontrivial_traceHilbertSpace,167 separableSpace_separableCounterexampleHilbertSpace,168 ⟨separableCounterexampleRepresentation,169 separableCounterexampleRepresentation_injective⟩, ?_⟩170 intro H _ _ _ _ ρ171 exact not_isIrreducible_of_separable ρ172173end MathlibAnnex.CStarAlgebra.CAR