MATHLIBANNEX / EXACT SOURCE v0.4.0
MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_unit_eigenvector_of_character_ne_infinity
theorem exists_unit_eigenvector_of_character_ne_infinity [Nontrivial A]
(pi : NonUnitalCStarRepresentation A H)
(hsingle : IsSingletonIrreducibleModel.{u, v, u} pi)
(D : StarSubalgebra ℂ (Unitization ℂ A))
[IsClosed (D : Set (Unitization ℂ A))]
(chi : WeakDual.characterSpace ℂ D)
(hchi : chi ≠ infinityCharacterOn (A := A) D) :
∃ eta : H, ‖eta‖ = 1 ∧
∀ d : D, pi.unitization (d : Unitization ℂ A) eta = chi d • eta1 import Mathlib.Analysis.CStarAlgebra.GelfandDuality 2 import MathlibAnnex.Analysis.CStarAlgebra.NonUnital.Singleton 3 import MathlibAnnex.Analysis.CStarAlgebra.State.Extension 4 5 /-! 6 # Non-scalar unitization characters as eigenvectors 7 -/ 8 9 set_option autoImplicit false 10 11 open Set 12 open scoped ComplexOrder InnerProduct 13 14 namespace MathlibAnnex.Analysis.CStarAlgebra 15 16 universe u v 17 18 variable {A : Type u} [NonUnitalCStarAlgebra A] 19 [PartialOrder A] [StarOrderedRing A] 20 variable {H : Type v} 21 variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 22 23 namespace NonUnitalCStarRepresentation 24 25 /-- The scalar character of the minimal unitization. -/ 26 noncomputable def infinityCharacter : 27 WeakDual.characterSpace ℂ (Unitization ℂ A) := 28 WeakDual.CharacterSpace.equivAlgHom.symm (Unitization.fstHom (R := ℂ) (A := A)) 29 30 @[simp] 31 theorem infinityCharacter_apply (z : Unitization ℂ A) : 32 infinityCharacter (A := A) z = z.fst := by 33 simp [infinityCharacter] 34 35 /-- The restriction of the scalar character to a unital star subalgebra of 36 the unitization. -/ 37 noncomputable def infinityCharacterOn 38 (D : StarSubalgebra ℂ (Unitization ℂ A)) 39 [IsClosed (D : Set (Unitization ℂ A))] : 40 WeakDual.characterSpace ℂ D := 41 WeakDual.CharacterSpace.equivAlgHom.symm 42 ((Unitization.fstHom (R := ℂ) (A := A)).comp D.subtype.toAlgHom) 43 44 @[simp] 45 theorem infinityCharacterOn_apply 46 (D : StarSubalgebra ℂ (Unitization ℂ A)) 47 [IsClosed (D : Set (Unitization ℂ A))] (d : D) : 48 infinityCharacterOn (A := A) D d = (d : Unitization ℂ A).fst := by 49 change (d : Unitization ℂ A).fst = (d : Unitization ℂ A).fst 50 rfl 51 52 /-- If the GNS representation of a state of the unitization vanishes on the 53 original algebra, then the state is the scalar character. -/ 54 theorem state_eq_infinity_of_gns_restriction_zero 55 (phi : Unitization ℂ A →L[ℂ] ℂ) 56 (hphi : phi ∈ stateSpace (Unitization ℂ A)) 57 (hzero : ∀ a : A, 58 (positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom 59 (Unitization.inr a) = 0) : 60 phi = (Unitization.fstHom (R := ℂ) (A := A)).toContinuousLinearMap := by 61 let f : Unitization ℂ A →ₚ[ℂ] ℂ := 62 positiveLinearMapOfMemStateSpace phi hphi 63 apply ContinuousLinearMap.ext 64 intro z 65 induction z using Unitization.ind with 66 | inl_add_inr c a => 67 have hinr : phi (Unitization.inr a) = 0 := by 68 calc 69 phi (Unitization.inr a) = f (Unitization.inr a) := rfl 70 _ = inner ℂ f.gnsCyclicVector 71 (f.gnsStarAlgHom (Unitization.inr a) f.gnsCyclicVector) := 72 (PositiveLinearMap.inner_gnsCyclicVector_gnsStarAlgHom f _).symm 73 _ = 0 := by rw [hzero a]; simp 74 have hinl : phi (Unitization.inl c) = c := by 75 calc 76 phi (Unitization.inl c) = phi (c • (1 : Unitization ℂ A)) := by 77 congr 1 78 simpa using 79 (Unitization.inl_smul (A := A) c (1 : ℂ)) 80 _ = c • phi (1 : Unitization ℂ A) := map_smul phi c 1 81 _ = c := by rw [hphi.2]; simp 82 simp only [map_add, hinl, hinr, add_zero] 83 simp [Unitization.fstHom] 84 85 /-- Every character of a closed unital star subalgebra of the unitization, 86 except the scalar character, occurs as a joint unit eigenvector for the 87 unitized singleton model. -/ 88 theorem exists_unit_eigenvector_of_character_ne_infinity [Nontrivial A] 89 (pi : NonUnitalCStarRepresentation A H) 90 (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) 91 (D : StarSubalgebra ℂ (Unitization ℂ A)) 92 [IsClosed (D : Set (Unitization ℂ A))] 93 (chi : WeakDual.characterSpace ℂ D) 94 (hchi : chi ≠ infinityCharacterOn (A := A) D) : 95 ∃ eta : H, ‖eta‖ = 1 ∧ 96 ∀ d : D, pi.unitization (d : Unitization ℂ A) eta = chi d • eta := by 97 obtain ⟨phi, hphi, hpure, hext⟩ := 98 exists_pureState_extension D chi 99 let f : Unitization ℂ A →ₚ[ℂ] ℂ := 100 positiveLinearMapOfMemStateSpace phi hphi 101 let rhoU : Representation (Unitization ℂ A) f.GNS := f.gnsStarAlgHom 102 let rho : NonUnitalCStarRepresentation A f.GNS := 103 rhoU.toNonUnitalStarAlgHom.comp 104 (Unitization.inrNonUnitalStarAlgHom ℂ A) 105 have hrho_nonzero : rho.IsNonzero := by 106 by_contra hnz 107 have hzero : ∀ a : A, rhoU (Unitization.inr a) = 0 := by 108 intro a 109 have : rho a = 0 := by 110 by_contra ha 111 exact hnz ⟨a, ha⟩ 112 simpa [rho] using this 113 have hphi_inf := 114 state_eq_infinity_of_gns_restriction_zero phi hphi hzero 115 apply hchi 116 apply WeakDual.CharacterSpace.ext 117 intro d 118 calc 119 chi d = phi (d : Unitization ℂ A) := (hext d).symm 120 _ = (Unitization.fstHom (R := ℂ) (A := A)).toContinuousLinearMap 121 (d : Unitization ℂ A) := by rw [hphi_inf] 122 _ = infinityCharacterOn (A := A) D d := by 123 simp 124 have hxi : ‖f.gnsCyclicVector‖ = 1 := 125 PositiveLinearMap.norm_gnsCyclicVector f 126 (positiveLinearMapOfMemStateSpace_one phi hphi) 127 have hxi_ne : f.gnsCyclicVector ≠ 0 := by 128 intro hzero 129 simp [hzero] at hxi 130 letI : Nontrivial f.GNS := 131 nontrivial_of_ne f.gnsCyclicVector 0 hxi_ne 132 have hirrU : rhoU.IsIrreducible := 133 (Representation.isIrreducible_iff_starAlgHom rhoU).2 134 (isIrreducible_pureState_gnsStarAlgHom phi hphi hpure) 135 have hirr : rho.IsIrreducible := 136 isIrreducible_restriction_of_isIrreducible_unitization rhoU hirrU 137 hrho_nonzero 138 obtain ⟨U, hU⟩ := hsingle.2 f.GNS rho hirr 139 have hUunit := unitization_unitaryEquivalent (pi := pi) (rho := rho) ⟨U, hU⟩ 140 obtain ⟨V, hV⟩ := hUunit 141 have hrhoeq : rho.unitization = rhoU := by 142 apply Unitization.starAlgHom_ext 143 ext a 144 simp [rho, unitization] 145 have heigen (d : D) : 146 rhoU (d : Unitization ℂ A) f.gnsCyclicVector = 147 chi d • f.gnsCyclicVector := by 148 let q : D := d - algebraMap ℂ D (chi d) 149 have hchiq : chi q = 0 := by 150 dsimp [q] 151 rw [map_sub, AlgHomClass.commutes] 152 simp 153 have hchiqq : chi (star q * q) = 0 := by 154 rw [map_mul, map_star, hchiq] 155 simp 156 have hphiqq : phi (star (q : Unitization ℂ A) * 157 (q : Unitization ℂ A)) = 0 := by 158 have hvalue := hext (star q * q) 159 change phi (star (q : Unitization ℂ A) * 160 (q : Unitization ℂ A)) = chi (star q * q) at hvalue 161 exact hvalue.trans hchiqq 162 have hinner : inner ℂ 163 (rhoU (q : Unitization ℂ A) f.gnsCyclicVector) 164 (rhoU (q : Unitization ℂ A) f.gnsCyclicVector) = 0 := by 165 calc 166 _ = Representation.vectorFunctional rhoU f.gnsCyclicVector 167 (star (q : Unitization ℂ A) * (q : Unitization ℂ A)) := by 168 simpa using 169 (Representation.vectorFunctional_star_mul rhoU f.gnsCyclicVector 170 (q : Unitization ℂ A) (q : Unitization ℂ A)).symm 171 _ = f (star (q : Unitization ℂ A) * 172 (q : Unitization ℂ A)) := 173 PositiveLinearMap.inner_gnsCyclicVector_gnsStarAlgHom f _ 174 _ = phi (star (q : Unitization ℂ A) * 175 (q : Unitization ℂ A)) := rfl 176 _ = 0 := hphiqq 177 have hqzero : rhoU (q : Unitization ℂ A) f.gnsCyclicVector = 0 := 178 inner_self_eq_zero.mp hinner 179 have hsub : rhoU (d : Unitization ℂ A) f.gnsCyclicVector - 180 chi d • f.gnsCyclicVector = 0 := by 181 calc 182 _ = rhoU (q : Unitization ℂ A) f.gnsCyclicVector := by 183 simp [q, Algebra.algebraMap_eq_smul_one] 184 _ = 0 := hqzero 185 exact sub_eq_zero.mp hsub 186 refine ⟨V.symm f.gnsCyclicVector, 187 (V.symm.norm_map f.gnsCyclicVector).trans hxi, ?_⟩ 188 intro d 189 apply V.injective 190 calc 191 V (pi.unitization (d : Unitization ℂ A) 192 (V.symm f.gnsCyclicVector)) = 193 rho.unitization (d : Unitization ℂ A) f.gnsCyclicVector := by 194 simpa using hV (d : Unitization ℂ A) (V.symm f.gnsCyclicVector) 195 _ = rhoU (d : Unitization ℂ A) f.gnsCyclicVector := by rw [hrhoeq] 196 _ = chi d • f.gnsCyclicVector := heigen d 197 _ = V (chi d • V.symm f.gnsCyclicVector) := by simp 198 199 end NonUnitalCStarRepresentation 200 201 end MathlibAnnex.Analysis.CStarAlgebra