Exact source view. Private integrated preview.
Exact declaration: MathlibAnnex.CStarAlgebra.CAR.atomicCounterexampleEndpoint_and_exists_separable_faithful_representation_and_no_separable_irreducible_representation
MathlibAnnex/Analysis/CStarAlgebra/CAR/SeparableFaithful.lean · lines 152–171
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.TraceGNSModel 2import MathlibAnnex.Analysis.CStarAlgebra.CAR.TraceState 3import MathlibAnnex.Analysis.CStarAlgebra.CAR.SeparableIrreducible 4import MathlibAnnex.Analysis.CStarAlgebra.Representation.CyclicRestriction 5 6/-! 7# The separably represented ordinary Naimark endpoint 8 9The carrier remains exactly `AtomicCounterexampleAlgebra`. Its faithful 10separable representation is reducible and has no nonzero irreducible closed 11subrepresentation. These are separate conclusions from uniqueness of the 12abstract irreducible representation class. 13-/ 14 15set_option autoImplicit false 16 17open scoped InnerProduct 18 19namespace MathlibAnnex.CStarAlgebra.CAR 20 21open MathlibAnnex.Analysis.CStarAlgebra 22 23universe v 24 25/-- The separable Hilbert space for the single previously selected target. -/ 26abbrev SeparableCounterexampleHilbertSpace := TraceHilbertSpace 27 28/-- A faithful representation of exactly the existing atomic counterexample 29on a separable Hilbert space. -/ 30noncomputable def separableCounterexampleRepresentation : 31 Representation AtomicCounterexampleAlgebra SeparableCounterexampleHilbertSpace := 32 traceModelRepresentation homogeneityShellFamily 33 34theorem separableSpace_separableCounterexampleHilbertSpace : 35 TopologicalSpace.SeparableSpace SeparableCounterexampleHilbertSpace := 36 separableSpace_traceHilbertSpace 37 38theorem separableCounterexampleRepresentation_injective : 39 Function.Injective separableCounterexampleRepresentation := 40 traceModelRepresentation_injective homogeneityShellFamily 41 42theorem isometry_separableCounterexampleRepresentation : 43 Isometry separableCounterexampleRepresentation := 44 isometry_traceModelRepresentation homogeneityShellFamily 45 46theorem not_isIrreducible_separableCounterexampleRepresentation : 47 ¬ Representation.IsIrreducible separableCounterexampleRepresentation := by 48 letI : TopologicalSpace.SeparableSpace SeparableCounterexampleHilbertSpace := 49 separableSpace_separableCounterexampleHilbertSpace 50 exact not_isIrreducible_of_separable 51 separableCounterexampleRepresentation.toNonUnitalStarAlgHom 52 53/-- Even passing to an arbitrary closed reducing subspace does not yield a 54nonzero irreducible subrepresentation. -/ 55theorem not_isIrreducible_restrictToReducing_separableCounterexampleRepresentation 56 (M : Submodule ℂ SeparableCounterexampleHilbertSpace) 57 (hM : separableCounterexampleRepresentation.Reduces M) : 58 letI : CompleteSpace M := hM.1.completeSpace_coe 59 ¬ Representation.IsIrreducible 60 (Representation.restrictToReducing separableCounterexampleRepresentation M hM) := by 61 letI : CompleteSpace M := hM.1.completeSpace_coe 62 letI : TopologicalSpace.SeparableSpace SeparableCounterexampleHilbertSpace := 63 separableSpace_separableCounterexampleHilbertSpace 64 letI : TopologicalSpace.SeparableSpace M := inferInstance 65 exact not_isIrreducible_of_separable 66 (Representation.restrictToReducing 67 separableCounterexampleRepresentation M hM).toNonUnitalStarAlgHom 68 69/-- 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⟩ 79 80/-- The stronger conclusion preserves the entire previously proved 81ordinary 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⟩ 90 91/-- The unique trace of the unchanged atomic counterexample. -/ 92noncomputable def atomicCounterexampleTrace : AtomicCounterexampleAlgebra →L[ℂ] ℂ := 93 traceExtension homogeneityShellFamily 94 95theorem atomicCounterexampleTrace_mem_stateSpace : 96 atomicCounterexampleTrace ∈ 97 MathlibAnnex.Analysis.CStarAlgebra.stateSpace AtomicCounterexampleAlgebra := 98 traceExtension_mem_stateSpace homogeneityShellFamily 99 100theorem atomicCounterexampleTrace_mul_comm (a b : AtomicCounterexampleAlgebra) : 101 atomicCounterexampleTrace (a * b) = atomicCounterexampleTrace (b * a) := 102 traceExtension_mul_comm homogeneityShellFamily a b 103 104theorem atomicCounterexampleTrace_star_mul_self_eq_zero_iff 105 (a : AtomicCounterexampleAlgebra) : 106 atomicCounterexampleTrace (star a * a) = 0 ↔ a = 0 := 107 traceExtension_star_mul_self_eq_zero_iff homogeneityShellFamily a 108 109/-- The trace is implemented by the original CAR trace vector in the 110separable faithful model. -/ 111@[simp] 112theorem inner_traceVector_separableCounterexampleRepresentation 113 (a : AtomicCounterexampleAlgebra) : 114 inner ℂ traceVector (separableCounterexampleRepresentation a traceVector) = 115 atomicCounterexampleTrace a := 116 inner_traceVector_traceModelRepresentation homogeneityShellFamily a 117 118theorem eq_atomicCounterexampleTrace_of_mem_stateSpace_of_mul_comm 119 (φ : 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φtrace 123 124/-- The final strengthened endpoint uses only previously separated proof 125constants. It retains the ordinary endpoint at any comparison universe and 126adds 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⟩ 151 152/-- The same fixed algebra has a faithful representation on a nontrivial separable 153Hilbert space, but has no nonzero irreducible representation on any separable 154Hilbert space in the arbitrary comparison universe. This does not assert that 155the 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) := by 166 refine ⟨shellFamilyEndpoint homogeneityShellFamily, nontrivial_traceHilbertSpace, 167 separableSpace_separableCounterexampleHilbertSpace, 168 ⟨separableCounterexampleRepresentation, 169 separableCounterexampleRepresentation_injective⟩, ?_⟩ 170 intro H _ _ _ _ ρ 171 exact not_isIrreducible_of_separable ρ 172 173end MathlibAnnex.CStarAlgebra.CAR