Exact source: MathlibAnnex/Analysis/CStarAlgebra/NonUnital/CharacterEigenvector.lean
Pinned GitHub source · Raw UTF-8 source
Back to The full character space is countable · Back to A character becomes a joint unit eigenvector · Back to Every operator in a singleton image is compact
1import Mathlib.Analysis.CStarAlgebra.GelfandDuality2import MathlibAnnex.Analysis.CStarAlgebra.NonUnital.Singleton3import MathlibAnnex.Analysis.CStarAlgebra.State.Extension45/-!6# Non-scalar unitization characters as eigenvectors7-/89set_option autoImplicit false1011open Set12open scoped ComplexOrder InnerProduct1314namespace MathlibAnnex.Analysis.CStarAlgebra1516universe u v1718variable {A : Type u} [NonUnitalCStarAlgebra A]19 [PartialOrder A] [StarOrderedRing A]20variable {H : Type v}21variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]2223namespace NonUnitalCStarRepresentation2425/-- The scalar character of the minimal unitization. -/26noncomputable def infinityCharacter :27 WeakDual.characterSpace ℂ (Unitization ℂ A) :=28 WeakDual.CharacterSpace.equivAlgHom.symm (Unitization.fstHom (R := ℂ) (A := A))2930@[simp]31theorem infinityCharacter_apply (z : Unitization ℂ A) :32 infinityCharacter (A := A) z = z.fst := by33 simp [infinityCharacter]3435/-- The restriction of the scalar character to a unital star subalgebra of36the unitization. -/37noncomputable def infinityCharacterOn38 (D : StarSubalgebra ℂ (Unitization ℂ A))39 [IsClosed (D : Set (Unitization ℂ A))] :40 WeakDual.characterSpace ℂ D :=41 WeakDual.CharacterSpace.equivAlgHom.symm42 ((Unitization.fstHom (R := ℂ) (A := A)).comp D.subtype.toAlgHom)4344@[simp]45theorem infinityCharacterOn_apply46 (D : StarSubalgebra ℂ (Unitization ℂ A))47 [IsClosed (D : Set (Unitization ℂ A))] (d : D) :48 infinityCharacterOn (A := A) D d = (d : Unitization ℂ A).fst := by49 change (d : Unitization ℂ A).fst = (d : Unitization ℂ A).fst50 rfl5152/-- If the GNS representation of a state of the unitization vanishes on the53original algebra, then the state is the scalar character. -/54theorem state_eq_infinity_of_gns_restriction_zero55 (phi : Unitization ℂ A →L[ℂ] ℂ)56 (hphi : phi ∈ stateSpace (Unitization ℂ A))57 (hzero : ∀ a : A,58 (positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom59 (Unitization.inr a) = 0) :60 phi = (Unitization.fstHom (R := ℂ) (A := A)).toContinuousLinearMap := by61 let f : Unitization ℂ A →ₚ[ℂ] ℂ :=62 positiveLinearMapOfMemStateSpace phi hphi63 apply ContinuousLinearMap.ext64 intro z65 induction z using Unitization.ind with66 | inl_add_inr c a =>67 have hinr : phi (Unitization.inr a) = 0 := by68 calc69 phi (Unitization.inr a) = f (Unitization.inr a) := rfl70 _ = inner ℂ f.gnsCyclicVector71 (f.gnsStarAlgHom (Unitization.inr a) f.gnsCyclicVector) :=72 (PositiveLinearMap.inner_gnsCyclicVector_gnsStarAlgHom f _).symm73 _ = 0 := by rw [hzero a]; simp74 have hinl : phi (Unitization.inl c) = c := by75 calc76 phi (Unitization.inl c) = phi (c • (1 : Unitization ℂ A)) := by77 congr 178 simpa using79 (Unitization.inl_smul (A := A) c (1 : ℂ))80 _ = c • phi (1 : Unitization ℂ A) := map_smul phi c 181 _ = c := by rw [hphi.2]; simp82 simp only [map_add, hinl, hinr, add_zero]83 simp [Unitization.fstHom]8485/-- Every character of a closed unital star subalgebra of the unitization,86except the scalar character, occurs as a joint unit eigenvector for the87unitized singleton model. -/88theorem 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 := by97 obtain ⟨phi, hphi, hpure, hext⟩ :=98 exists_pureState_extension D chi99 let f : Unitization ℂ A →ₚ[ℂ] ℂ :=100 positiveLinearMapOfMemStateSpace phi hphi101 let rhoU : Representation (Unitization ℂ A) f.GNS := f.gnsStarAlgHom102 let rho : NonUnitalCStarRepresentation A f.GNS :=103 rhoU.toNonUnitalStarAlgHom.comp104 (Unitization.inrNonUnitalStarAlgHom ℂ A)105 have hrho_nonzero : rho.IsNonzero := by106 by_contra hnz107 have hzero : ∀ a : A, rhoU (Unitization.inr a) = 0 := by108 intro a109 have : rho a = 0 := by110 by_contra ha111 exact hnz ⟨a, ha⟩112 simpa [rho] using this113 have hphi_inf :=114 state_eq_infinity_of_gns_restriction_zero phi hphi hzero115 apply hchi116 apply WeakDual.CharacterSpace.ext117 intro d118 calc119 chi d = phi (d : Unitization ℂ A) := (hext d).symm120 _ = (Unitization.fstHom (R := ℂ) (A := A)).toContinuousLinearMap121 (d : Unitization ℂ A) := by rw [hphi_inf]122 _ = infinityCharacterOn (A := A) D d := by123 simp124 have hxi : ‖f.gnsCyclicVector‖ = 1 :=125 PositiveLinearMap.norm_gnsCyclicVector f126 (positiveLinearMapOfMemStateSpace_one phi hphi)127 have hxi_ne : f.gnsCyclicVector ≠ 0 := by128 intro hzero129 simp [hzero] at hxi130 letI : Nontrivial f.GNS :=131 nontrivial_of_ne f.gnsCyclicVector 0 hxi_ne132 have hirrU : rhoU.IsIrreducible :=133 (Representation.isIrreducible_iff_starAlgHom rhoU).2134 (isIrreducible_pureState_gnsStarAlgHom phi hphi hpure)135 have hirr : rho.IsIrreducible :=136 isIrreducible_restriction_of_isIrreducible_unitization rhoU hirrU137 hrho_nonzero138 obtain ⟨U, hU⟩ := hsingle.2 f.GNS rho hirr139 have hUunit := unitization_unitaryEquivalent (pi := pi) (rho := rho) ⟨U, hU⟩140 obtain ⟨V, hV⟩ := hUunit141 have hrhoeq : rho.unitization = rhoU := by142 apply Unitization.starAlgHom_ext143 ext a144 simp [rho, unitization]145 have heigen (d : D) :146 rhoU (d : Unitization ℂ A) f.gnsCyclicVector =147 chi d • f.gnsCyclicVector := by148 let q : D := d - algebraMap ℂ D (chi d)149 have hchiq : chi q = 0 := by150 dsimp [q]151 rw [map_sub, AlgHomClass.commutes]152 simp153 have hchiqq : chi (star q * q) = 0 := by154 rw [map_mul, map_star, hchiq]155 simp156 have hphiqq : phi (star (q : Unitization ℂ A) *157 (q : Unitization ℂ A)) = 0 := by158 have hvalue := hext (star q * q)159 change phi (star (q : Unitization ℂ A) *160 (q : Unitization ℂ A)) = chi (star q * q) at hvalue161 exact hvalue.trans hchiqq162 have hinner : inner ℂ163 (rhoU (q : Unitization ℂ A) f.gnsCyclicVector)164 (rhoU (q : Unitization ℂ A) f.gnsCyclicVector) = 0 := by165 calc166 _ = Representation.vectorFunctional rhoU f.gnsCyclicVector167 (star (q : Unitization ℂ A) * (q : Unitization ℂ A)) := by168 simpa using169 (Representation.vectorFunctional_star_mul rhoU f.gnsCyclicVector170 (q : Unitization ℂ A) (q : Unitization ℂ A)).symm171 _ = 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)) := rfl176 _ = 0 := hphiqq177 have hqzero : rhoU (q : Unitization ℂ A) f.gnsCyclicVector = 0 :=178 inner_self_eq_zero.mp hinner179 have hsub : rhoU (d : Unitization ℂ A) f.gnsCyclicVector -180 chi d • f.gnsCyclicVector = 0 := by181 calc182 _ = rhoU (q : Unitization ℂ A) f.gnsCyclicVector := by183 simp [q, Algebra.algebraMap_eq_smul_one]184 _ = 0 := hqzero185 exact sub_eq_zero.mp hsub186 refine ⟨V.symm f.gnsCyclicVector,187 (V.symm.norm_map f.gnsCyclicVector).trans hxi, ?_⟩188 intro d189 apply V.injective190 calc191 V (pi.unitization (d : Unitization ℂ A)192 (V.symm f.gnsCyclicVector)) =193 rho.unitization (d : Unitization ℂ A) f.gnsCyclicVector := by194 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 d197 _ = V (chi d • V.symm f.gnsCyclicVector) := by simp198199end NonUnitalCStarRepresentation200201end MathlibAnnex.Analysis.CStarAlgebra