Exact source: MathlibAnnex/Analysis/CStarAlgebra/PureStateGNS/PureIrreducible.lean, lines 138–155.
Back to Pure CAR states admit two-sided inner intertwining sequences
1import Mathlib.Analysis.InnerProductSpace.Projection.Basic 2import MathlibAnnex.Analysis.CStarAlgebra.Representation.Cyclic 3import MathlibAnnex.Analysis.CStarAlgebra.PureStateGNS.Purity 4import MathlibAnnex.Analysis.CStarAlgebra.PureStateGNS.VectorState 5 6/-! 7# The pure-to-irreducible GNS bridge 8 9This file proves the projection half of the classical correspondence without 10finite-dimensional reduction or Kadison transitivity. 11-/ 12 13set_option autoImplicit false 14 15open Set 16open scoped ComplexOrder InnerProduct 17 18namespace MathlibAnnex.CStarAlgebra 19 20universe u v 21 22variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] 23variable {H : Type v} 24variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 25 26open MathlibAnnex.Analysis.CStarAlgebra 27 28/-- A cyclic representation whose unit vector state is pure has no 29nontrivial closed reducing subspace. -/ 30theorem isIrreducible_starAlgHom_of_isPureState 31 (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (ξ : H) (hξ : ‖ξ‖ = 1) 32 (hcyclic : DenseRange (StarAlgHom.orbitMap pi ξ)) 33 (hpure : IsPureState A (Representation.vectorFunctional pi ξ)) : 34 StarAlgHom.IsIrreducible pi := by 35 intro K hKclosed hKreduces 36 letI : IsClosed (K : Set H) := hKclosed 37 letI : CompleteSpace K := inferInstance 38 letI : K.HasOrthogonalProjection := inferInstance 39 let P : H →L[ℂ] H := K.starProjection 40 let x : H := P ξ 41 let y : H := ξ - x 42 let rho : A →L[ℂ] ℂ := Representation.vectorFunctional pi x 43 have hxK : x ∈ K := by 44 exact K.starProjection_apply_mem ξ 45 have hyK : y ∈ Kᗮ := by 46 exact K.sub_starProjection_mem_orthogonal ξ 47 have hmapK (a : A) : pi a x ∈ K := 48 (hKreduces a).1 hxK 49 have hmapOrth (a : A) : pi a y ∈ Kᗮ := 50 Representation.map_mem_orthogonal_of_adjoint_mem (pi a) K 51 (hKreduces a).2 hyK 52 have hdecomp (a : A) : 53 Representation.vectorFunctional pi ξ a = 54 rho a + Representation.vectorFunctional pi y a := by 55 simp only [Representation.vectorFunctional_apply] 56 rw [show ξ = x + y by simp [y], map_add] 57 simp only [inner_add_left, inner_add_right] 58 rw [K.inner_right_of_mem_orthogonal hxK (hmapOrth a), 59 K.inner_left_of_mem_orthogonal (hmapK a) hyK] 60 simp [rho] 61 have hrho_nonneg : ∀ a : A, 0 ≤ a → 0 ≤ rho a := by 62 intro a ha 63 exact Representation.vectorFunctional_nonnegative pi x ha 64 have hrho_le : ∀ a : A, 0 ≤ a → 65 rho a ≤ Representation.vectorFunctional pi ξ a := by 66 intro a ha 67 rw [hdecomp] 68 exact le_add_of_nonneg_right 69 (Representation.vectorFunctional_nonnegative pi y ha) 70 obtain ⟨t, ht, ht_one, hrho⟩ := eq_smul_of_pureState_of_nonnegative_le 71 (Representation.vectorFunctional pi ξ) rho hpure hrho_nonneg hrho_le 72 have hPcomm (a : A) : P.comp (pi a) = (pi a).comp P := by 73 exact Submodule.Reduces.starProjection_commute (hKreduces a) 74 have hP_orbit (a : A) : P (pi a ξ) = pi a x := by 75 simpa [P, x, ContinuousLinearMap.comp_apply] using 76 congrArg (fun T : H →L[ℂ] H ↦ T ξ) (hPcomm a) 77 have hgram (a b : A) : 78 inner ℂ (pi a ξ) (P (pi b ξ)) = rho (star a * b) := by 79 calc 80 inner ℂ (pi a ξ) (P (pi b ξ)) = 81 inner ℂ (P (pi a ξ)) (pi b ξ) := by 82 exact (K.inner_starProjection_left_eq_right (pi a ξ) (pi b ξ)).symm 83 _ = inner ℂ (P (pi a ξ)) (P (pi b ξ)) := by 84 let z : K := ⟨P (pi a ξ), K.starProjection_apply_mem (pi a ξ)⟩ 85 exact (K.inner_orthogonalProjectionOnto_eq_of_mem_left z (pi b ξ)).symm 86 _ = inner ℂ (pi a x) (pi b x) := by rw [hP_orbit, hP_orbit] 87 _ = rho (star a * b) := 88 (Representation.vectorFunctional_star_mul pi x a b).symm 89 have hinner (a b : A) : 90 inner ℂ (pi a ξ) (P (pi b ξ)) = 91 inner ℂ (pi a ξ) (t • pi b ξ) := by 92 calc 93 inner ℂ (pi a ξ) (P (pi b ξ)) = rho (star a * b) := hgram a b 94 _ = (t • Representation.vectorFunctional pi ξ) (star a * b) := by 95 rw [hrho] 96 _ = t • inner ℂ (pi a ξ) (pi b ξ) := by 97 simp only [smul_apply, Representation.vectorFunctional_star_mul] 98 _ = inner ℂ (pi a ξ) (t • pi b ξ) := by 99 simpa [Complex.real_smul] using 100 (inner_smul_right (pi a ξ) (pi b ξ) (t : ℂ)).symm 101 have hP_on_orbit (b : A) : P (pi b ξ) = t • pi b ξ := by 102 apply ext_inner_left ℂ 103 intro z 104 exact hcyclic.induction_on z 105 (isClosed_eq (continuous_id.inner continuous_const) 106 (continuous_id.inner continuous_const)) fun a ↦ hinner a b 107 have hP : P = t • ContinuousLinearMap.id ℂ H := by 108 apply ContinuousLinearMap.ext 109 intro z 110 exact hcyclic.induction_on z 111 (isClosed_eq P.continuous (t • ContinuousLinearMap.id ℂ H).continuous) fun b ↦ by 112 simpa [StarAlgHom.orbitMap] using hP_on_orbit b 113 have hξ_ne : ξ ≠ 0 := by 114 intro hzero 115 simpa [hzero] using hξ 116 have ht_idem : t * t = t := by 117 apply smul_left_injective ℝ hξ_ne 118 have hidem := congrArg (fun T : H →L[ℂ] H ↦ T ξ) 119 K.isIdempotentElem_starProjection.eq 120 change P (P ξ) = P ξ at hidem 121 rw [hP] at hidem 122 simpa [smul_smul] using hidem 123 have ht_cases : t = 0 ∨ t = 1 := by 124 rcases eq_zero_or_eq_zero_of_mul_eq_zero (show t * (t - 1) = 0 by nlinarith) with h | h 125 · exact Or.inl h 126 · exact Or.inr (sub_eq_zero.mp h) 127 rcases ht_cases with rfl | rfl 128 · left 129 rw [← K.range_starProjection] 130 simp [P] at hP 131 simpa [hP] 132 · right 133 rw [← K.range_starProjection] 134 simp [P] at hP 135 simpa [hP] 136 137/-- In particular, the GNS representation of a pure state is irreducible. -/ 138theorem isIrreducible_pureState_gnsStarAlgHom 139 (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) (hpure : IsPureState A phi) : 140 StarAlgHom.IsIrreducible 141 (positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom := by 142 apply isIrreducible_starAlgHom_of_isPureState 143 (positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom 144 (stateGNSVector phi hphi) (norm_stateGNSVector phi hphi) 145 (denseRange_gnsStarAlgHom_stateGNSVector phi hphi) 146 have hfunctional : 147 Representation.vectorFunctional 148 (positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom 149 (stateGNSVector phi hphi) = phi := by 150 apply ContinuousLinearMap.ext 151 intro a 152 exact inner_gnsStarAlgHom_stateGNSVector phi hphi a 153 rw [hfunctional] 154 exact hpure 155 156end MathlibAnnex.CStarAlgebra