Exact source: MathlibAnnex/Analysis/CStarAlgebra/PureStateGNS/IrreduciblePure.lean
Pinned GitHub source · Raw UTF-8 source
Back to An irreducible target representation has a surviving fixed space
1import Mathlib.Analysis.Normed.Operator.Extend2import MathlibAnnex.Analysis.CStarAlgebra.Intertwiner3import MathlibAnnex.Analysis.CStarAlgebra.PureStateGNS.PureIrreducible4import MathlibAnnex.Analysis.CStarAlgebra.Representation.PureStateRepresentatives56/-!7# Irreducible representations and pure vector states89The reverse pure-state/GNS implication is proved by extending the dominated10GNS orbit map to a contraction. Its positive initial operator lies in the11commutant, so the arbitrary-dimensional Schur theorem makes it scalar.12-/1314set_option autoImplicit false1516open Set17open scoped ComplexOrder Convex InnerProduct1819namespace MathlibAnnex.CStarAlgebra2021universe u v2223variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]24variable {H : Type v}25variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]2627open MathlibAnnex.Analysis.CStarAlgebra2829/-- A positive functional dominated by an irreducible unit vector state is a30real scalar multiple of that state. The dominated functional may be zero;31no normalization or nonzero hypothesis is used. -/32theorem eq_smul_of_irreducible_vectorFunctional_of_nonnegative_le33 (pi : Representation A H) (hirr : pi.IsIrreducible)34 (xi : H) (hxi : ‖xi‖ = 1)35 (rho : A →L[ℂ] ℂ) (hrho : ∀ a : A, 0 ≤ a → 0 ≤ rho a)36 (hle : ∀ a : A, 0 ≤ a → rho a ≤ Representation.vectorFunctional pi xi a) :37 ∃ t : ℝ, 0 ≤ t ∧ t ≤ 1 ∧38 rho = t • Representation.vectorFunctional pi xi := by39 letI : Nontrivial H := Representation.nontrivial_of_isNonzero pi hirr.140 have hxi_ne : xi ≠ 0 := by41 intro hzero42 simpa [hzero] using hxi43 have hdense : DenseRange (StarAlgHom.orbitMap pi xi) :=44 Representation.denseRange_orbitMap_of_isIrreducible pi hirr hxi_ne45 let f : A →ₚ[ℂ] ℂ := PositiveLinearMap.mk₀ rho.toLinearMap hrho46 let sigma : Representation A f.GNS := f.gnsStarAlgHom47 let eta : f.GNS := f.gnsCyclicVector48 let p : A →ₗ[ℂ] H := StarAlgHom.orbitMap pi xi49 let q : A →ₗ[ℂ] f.GNS := StarAlgHom.orbitMap sigma eta50 have hq_inner (a : A) : inner ℂ (q a) (q a) = rho (star a * a) := by51 calc52 inner ℂ (q a) (q a) =53 Representation.vectorFunctional sigma eta (star a * a) := by54 simpa [p, q, StarAlgHom.orbitMap] using55 (Representation.vectorFunctional_star_mul sigma eta a a).symm56 _ = f (star a * a) := by57 exact PositiveLinearMap.inner_gnsCyclicVector_gnsStarAlgHom f (star a * a)58 _ = rho (star a * a) := rfl59 have hp_inner (a : A) : inner ℂ (p a) (p a) =60 Representation.vectorFunctional pi xi (star a * a) := by61 simpa [p, StarAlgHom.orbitMap] using62 (Representation.vectorFunctional_star_mul pi xi a a).symm63 have hnorm (a : A) : ‖q a‖ ≤ (1 : ℝ) * ‖p a‖ := by64 rw [one_mul]65 apply (sq_le_sq₀ (norm_nonneg _) (norm_nonneg _)).mp66 rw [norm_sq_eq_re_inner (𝕜 := ℂ) (q a),67 norm_sq_eq_re_inner (𝕜 := ℂ) (p a), hq_inner, hp_inner]68 have hdiff := RCLike.nonneg_iff.mp69 (sub_nonneg.mpr (hle (star a * a) (star_mul_self_nonneg a)))70 simpa using hdiff.171 let T : H →L[ℂ] f.GNS := q.extendOfNorm p72 have hT_orbit (a : A) : T (pi a xi) = sigma a eta := by73 simpa [T, p, q, StarAlgHom.orbitMap] using74 (LinearMap.extendOfNorm_eq hdense ⟨(1 : ℝ), hnorm⟩ a)75 have hT_intertwines : StarAlgHom.Intertwines pi sigma T := by76 intro b77 apply ContinuousLinearMap.ext78 intro x79 exact hdense.induction_on x80 (isClosed_eq ((T.comp (pi b)).continuous) (((sigma b).comp T).continuous))81 fun a ↦ by82 change T (pi b (pi a xi)) = sigma b (T (pi a xi))83 have hpi_mul : pi (b * a) xi = pi b (pi a xi) := by84 rw [map_mul]85 rfl86 have hsigma_mul : sigma (b * a) eta = sigma b (sigma a eta) := by87 rw [map_mul]88 rfl89 calc90 T (pi b (pi a xi)) = T (pi (b * a) xi) := congrArg T hpi_mul.symm91 _ = sigma (b * a) eta := hT_orbit (b * a)92 _ = sigma b (sigma a eta) := hsigma_mul93 _ = sigma b (T (pi a xi)) := by rw [hT_orbit a]94 let D : H →L[ℂ] H := (T†).comp T95 have hD_self : IsSelfAdjoint D := by96 rw [isSelfAdjoint_iff, ContinuousLinearMap.star_eq_adjoint,97 ContinuousLinearMap.adjoint_comp, ContinuousLinearMap.adjoint_adjoint]98 have hD_comm : StarAlgHom.InCommutant pi D := by99 exact hT_intertwines.inCommutant_adjoint_comp_self100 obtain ⟨t, hD⟩ := StarAlgHom.eq_algebraMap_of_isSelfAdjoint_of_irreducible101 pi (Representation.isIrreducible_starAlgHom pi hirr) D hD_self hD_comm102 have hTxi : T xi = eta := by103 simpa using hT_orbit (1 : A)104 have heta_sq : ‖eta‖ ^ 2 = (rho 1).re := by105 rw [norm_sq_eq_re_inner (𝕜 := ℂ) eta]106 have hcoeff : inner ℂ eta eta = rho 1 := by107 calc108 inner ℂ eta eta = inner ℂ eta (sigma 1 eta) := by simp109 _ = f 1 := PositiveLinearMap.inner_gnsCyclicVector_gnsStarAlgHom f 1110 _ = rho 1 := rfl111 rw [hcoeff]112 rw [RCLike.re_eq_complex_re]113 have ht_eq : t = (rho 1).re := by114 have hnormD := ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_right T xi115 rw [hTxi, heta_sq] at hnormD116 rw [show (T†).comp T = D by rfl, hD] at hnormD117 rw [ContinuousLinearMap.algebraMap_apply,118 RCLike.real_smul_eq_coe_smul (K := ℂ), inner_smul_real_right,119 RCLike.smul_re, ← norm_sq_eq_re_inner (𝕜 := ℂ), hxi] at hnormD120 simpa using hnormD.symm121 have ht_nonneg : 0 ≤ t := by122 rw [ht_eq]123 exact (RCLike.nonneg_iff.mp124 (hrho 1 (by simpa using star_mul_self_nonneg (1 : A)))).1125 have ht_le_one : t ≤ 1 := by126 rw [ht_eq]127 have hdiff := RCLike.nonneg_iff.mp128 (sub_nonneg.mpr (hle 1 (by simpa using star_mul_self_nonneg (1 : A))))129 simpa [Representation.vectorFunctional_one pi hxi] using hdiff.1130 refine ⟨t, ht_nonneg, ht_le_one, ?_⟩131 apply ContinuousLinearMap.ext132 intro a133 calc134 rho a = inner ℂ eta (sigma a eta) := by135 exact (PositiveLinearMap.inner_gnsCyclicVector_gnsStarAlgHom f a).symm136 _ = inner ℂ (T xi) (sigma a (T xi)) := by rw [hTxi]137 _ = inner ℂ (T xi) (T (pi a xi)) := by138 have h := congrArg (fun R : H →L[ℂ] f.GNS ↦ R xi) (hT_intertwines a)139 simpa [ContinuousLinearMap.comp_apply] using congrArg (inner ℂ (T xi)) h.symm140 _ = inner ℂ xi (D (pi a xi)) := by141 simpa [D, ContinuousLinearMap.comp_apply] using142 (ContinuousLinearMap.adjoint_inner_right T xi (T (pi a xi))).symm143 _ = inner ℂ xi ((algebraMap ℝ (H →L[ℂ] H) t) (pi a xi)) := by rw [hD]144 _ = (t • Representation.vectorFunctional pi xi) a := by145 rw [ContinuousLinearMap.algebraMap_apply,146 RCLike.real_smul_eq_coe_smul (K := ℂ), inner_smul_right]147 simp [Representation.vectorFunctional_apply, Complex.real_smul]148149/-- Every unit vector state of an explicitly nonzero irreducible unital150representation is pure. -/151theorem isPureState_vectorFunctional_of_isIrreducible152 (pi : Representation A H) (hirr : pi.IsIrreducible)153 (xi : H) (hxi : ‖xi‖ = 1) :154 IsPureState A (Representation.vectorFunctional pi xi) := by155 rw [IsPureState, mem_extremePoints_iff_left]156 refine ⟨vectorFunctional_mem_stateSpace pi xi hxi, ?_⟩157 intro psi hpsi chi hchi hsegment158 rcases hsegment with ⟨s, t, hs, ht, hst, hconv⟩159 let rho : A →L[ℂ] ℂ := s • psi160 have hrho : ∀ a : A, 0 ≤ a → 0 ≤ rho a := by161 intro a ha162 exact smul_nonneg hs.le (hpsi.1 a ha)163 have hle : ∀ a : A, 0 ≤ a →164 rho a ≤ Representation.vectorFunctional pi xi a := by165 intro a ha166 rw [← hconv]167 simp only [ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply]168 exact le_add_of_nonneg_right (smul_nonneg ht.le (hchi.1 a ha))169 obtain ⟨r, -, -, hrho_eq⟩ :=170 eq_smul_of_irreducible_vectorFunctional_of_nonnegative_le171 pi hirr xi hxi rho hrho hle172 have hrs : r = s := by173 have h := congrArg (fun f : A →L[ℂ] ℂ ↦ f 1) hrho_eq174 have hre := congrArg Complex.re h175 simpa [rho, hpsi.2, Representation.vectorFunctional_one pi hxi,176 Complex.real_smul] using hre.symm177 apply smul_right_injective (A →L[ℂ] ℂ) hs.ne'178 simpa [rho, hrs] using hrho_eq179180/-- Ordinary pure states are exactly those whose canonical GNS181representations are irreducible. -/182theorem isPureState_iff_gnsStarAlgHom_isIrreducible183 (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) :184 IsPureState A phi ↔185 StarAlgHom.IsIrreducible186 (positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom := by187 constructor188 · exact isIrreducible_pureState_gnsStarAlgHom phi hphi189 · intro hirr190 let f : A →ₚ[ℂ] ℂ := positiveLinearMapOfMemStateSpace phi hphi191 let xi : f.GNS := f.gnsCyclicVector192 have hxi : ‖xi‖ = 1 := by193 exact PositiveLinearMap.norm_gnsCyclicVector f194 (positiveLinearMapOfMemStateSpace_one phi hphi)195 have hxi_ne : xi ≠ 0 := by196 intro hzero197 simpa [hzero] using hxi198 letI : Nontrivial f.GNS := nontrivial_of_ne xi 0 hxi_ne199 have hirr' : Representation.IsIrreducible f.gnsStarAlgHom :=200 (Representation.isIrreducible_iff_starAlgHom f.gnsStarAlgHom).2 hirr201 have hpure := isPureState_vectorFunctional_of_isIrreducible202 f.gnsStarAlgHom hirr' xi hxi203 have hfunctional : Representation.vectorFunctional f.gnsStarAlgHom xi = phi := by204 apply ContinuousLinearMap.ext205 intro a206 exact inner_gnsStarAlgHom_stateGNSVector phi hphi a207 rw [hfunctional] at hpure208 exact hpure209210/-- The existing chosen pure-GNS transversal covers every nonzero211irreducible representation on an arbitrary target Hilbert-space universe. -/212theorem irreducible_covered_by_pureState_representative213 (root : PureState A) (pi : Representation A H) (hirr : pi.IsIrreducible) :214 ∃ j : PureState.GNSClass A,215 Representation.UnitaryEquivalent pi216 (PureState.representative root j).positiveFunctional.gnsStarAlgHom := by217 obtain ⟨xi, hxi, hcyclic, -, hpi⟩ := irreducible_exists_vectorStateGNS pi hirr218 have hpure : IsPureState A (Representation.vectorFunctional pi xi) :=219 isPureState_vectorFunctional_of_isIrreducible pi hirr xi hxi220 let phi : PureState A := ⟨Representation.vectorFunctional pi xi, hpure⟩221 have hpositive : phi.positiveFunctional = vectorPositiveFunctional pi xi hxi := by222 ext a223 rfl224 have hpi' : Representation.UnitaryEquivalent pi phi.positiveFunctional.gnsStarAlgHom := by225 rw [hpositive]226 exact hpi227 have hrep : Representation.UnitaryEquivalent228 (PureState.representative root phi.classOf).positiveFunctional.gnsStarAlgHom229 phi.positiveFunctional.gnsStarAlgHom :=230 PureState.representative_covers root phi231 exact ⟨phi.classOf, Representation.unitaryEquivalent_trans hpi'232 (Representation.unitaryEquivalent_symm hrep)⟩233234end MathlibAnnex.CStarAlgebra