MATHLIBANNEX / EXACT SOURCE v0.4.0
MathlibAnnex.Analysis.CStarAlgebra.isIrreducible_pureState_gnsStarAlgHom
theorem isIrreducible_pureState_gnsStarAlgHom
(phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) (hpure : IsPureState A phi) :
StarAlgHom.IsIrreducible
(positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom1 import Mathlib.Analysis.InnerProductSpace.Projection.Basic 2 import MathlibAnnex.Analysis.CStarAlgebra.Representation.Cyclic 3 import MathlibAnnex.Analysis.CStarAlgebra.State.Purity 4 5 /-! 6 # Pure states give irreducible GNS representations 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} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] 19 variable {H : Type v} 20 variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 21 22 /-- A cyclic representation whose unit-vector state is pure is irreducible. -/ 23 theorem isIrreducible_starAlgHom_of_isPureState 24 (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (xi : H) (hxi : ‖xi‖ = 1) 25 (hcyclic : DenseRange (StarAlgHom.orbitMap pi xi)) 26 (hpure : IsPureState A (Representation.vectorFunctional pi xi)) : 27 StarAlgHom.IsIrreducible pi := by 28 intro K hKclosed hKreduces 29 letI : IsClosed (K : Set H) := hKclosed 30 letI : CompleteSpace K := inferInstance 31 letI : K.HasOrthogonalProjection := inferInstance 32 let P : H →L[ℂ] H := K.starProjection 33 let x : H := P xi 34 let y : H := xi - x 35 let rho : A →L[ℂ] ℂ := Representation.vectorFunctional pi x 36 have hxK : x ∈ K := K.starProjection_apply_mem xi 37 have hyK : y ∈ Kᗮ := K.sub_starProjection_mem_orthogonal xi 38 have hmapK (a : A) : pi a x ∈ K := (hKreduces a).1 hxK 39 have hmapOrth (a : A) : pi a y ∈ Kᗮ := 40 Representation.map_mem_orthogonal_of_adjoint_mem (pi a) K 41 (hKreduces a).2 hyK 42 have hdecomp (a : A) : 43 Representation.vectorFunctional pi xi a = 44 rho a + Representation.vectorFunctional pi y a := by 45 simp only [Representation.vectorFunctional_apply] 46 rw [show xi = x + y by simp [y], map_add] 47 simp only [inner_add_left, inner_add_right] 48 rw [K.inner_right_of_mem_orthogonal hxK (hmapOrth a), 49 K.inner_left_of_mem_orthogonal (hmapK a) hyK] 50 simp [rho] 51 have hrho_nonneg : ∀ a : A, 0 ≤ a → 0 ≤ rho a := by 52 intro a ha 53 exact Representation.vectorFunctional_nonnegative pi x ha 54 have hrho_le : ∀ a : A, 0 ≤ a → 55 rho a ≤ Representation.vectorFunctional pi xi a := by 56 intro a ha 57 rw [hdecomp] 58 exact le_add_of_nonneg_right 59 (Representation.vectorFunctional_nonnegative pi y ha) 60 obtain ⟨t, ht, ht_one, hrho⟩ := eq_smul_of_pureState_of_nonnegative_le 61 (Representation.vectorFunctional pi xi) rho hpure hrho_nonneg hrho_le 62 have hPcomm (a : A) : P.comp (pi a) = (pi a).comp P := 63 Submodule.Reduces.starProjection_commute (hKreduces a) 64 have hP_orbit (a : A) : P (pi a xi) = pi a x := by 65 simpa [P, x, ContinuousLinearMap.comp_apply] using 66 congrArg (fun T : H →L[ℂ] H ↦ T xi) (hPcomm a) 67 have hgram (a b : A) : 68 inner ℂ (pi a xi) (P (pi b xi)) = rho (star a * b) := by 69 calc 70 inner ℂ (pi a xi) (P (pi b xi)) = 71 inner ℂ (P (pi a xi)) (pi b xi) := by 72 exact (K.inner_starProjection_left_eq_right (pi a xi) (pi b xi)).symm 73 _ = inner ℂ (P (pi a xi)) (P (pi b xi)) := by 74 let z : K := ⟨P (pi a xi), K.starProjection_apply_mem (pi a xi)⟩ 75 exact (K.inner_orthogonalProjectionOnto_eq_of_mem_left z (pi b xi)).symm 76 _ = inner ℂ (pi a x) (pi b x) := by rw [hP_orbit, hP_orbit] 77 _ = rho (star a * b) := 78 (Representation.vectorFunctional_star_mul pi x a b).symm 79 have hinner (a b : A) : 80 inner ℂ (pi a xi) (P (pi b xi)) = 81 inner ℂ (pi a xi) (t • pi b xi) := by 82 calc 83 inner ℂ (pi a xi) (P (pi b xi)) = rho (star a * b) := hgram a b 84 _ = (t • Representation.vectorFunctional pi xi) (star a * b) := by rw [hrho] 85 _ = t • inner ℂ (pi a xi) (pi b xi) := by 86 simp only [smul_apply, Representation.vectorFunctional_star_mul] 87 _ = inner ℂ (pi a xi) (t • pi b xi) := by 88 simpa [Complex.real_smul] using 89 (inner_smul_right (pi a xi) (pi b xi) (t : ℂ)).symm 90 have hP_on_orbit (b : A) : P (pi b xi) = t • pi b xi := by 91 apply ext_inner_left ℂ 92 intro z 93 exact hcyclic.induction_on z 94 (isClosed_eq (continuous_id.inner continuous_const) 95 (continuous_id.inner continuous_const)) fun a ↦ hinner a b 96 have hP : P = t • ContinuousLinearMap.id ℂ H := by 97 apply ContinuousLinearMap.ext 98 intro z 99 exact hcyclic.induction_on z 100 (isClosed_eq P.continuous (t • ContinuousLinearMap.id ℂ H).continuous) fun b ↦ by 101 simpa [StarAlgHom.orbitMap] using hP_on_orbit b 102 have hxi_ne : xi ≠ 0 := by 103 intro hzero 104 simpa [hzero] using hxi 105 have ht_idem : t * t = t := by 106 apply smul_left_injective ℝ hxi_ne 107 have hidem := congrArg (fun T : H →L[ℂ] H ↦ T xi) 108 K.isIdempotentElem_starProjection.eq 109 change P (P xi) = P xi at hidem 110 rw [hP] at hidem 111 simpa [smul_smul] using hidem 112 have ht_cases : t = 0 ∨ t = 1 := by 113 rcases eq_zero_or_eq_zero_of_mul_eq_zero 114 (show t * (t - 1) = 0 by nlinarith) with h | h 115 · exact Or.inl h 116 · exact Or.inr (sub_eq_zero.mp h) 117 rcases ht_cases with rfl | rfl 118 · left 119 rw [← K.range_starProjection] 120 simp [P] at hP 121 simpa [hP] 122 · right 123 rw [← K.range_starProjection] 124 simp [P] at hP 125 simpa [hP] 126 127 /-- The canonical GNS representation of a pure state is irreducible. -/ 128 theorem isIrreducible_pureState_gnsStarAlgHom 129 (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) (hpure : IsPureState A phi) : 130 StarAlgHom.IsIrreducible 131 (positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom := by 132 apply isIrreducible_starAlgHom_of_isPureState 133 (positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom 134 (stateGNSVector phi hphi) (norm_stateGNSVector phi hphi) 135 (denseRange_gnsStarAlgHom_stateGNSVector phi hphi) 136 have hfunctional : 137 Representation.vectorFunctional 138 (positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom 139 (stateGNSVector phi hphi) = phi := by 140 apply ContinuousLinearMap.ext 141 intro a 142 exact inner_gnsStarAlgHom_stateGNSVector phi hphi a 143 rw [hfunctional] 144 exact hpure 145 146 end MathlibAnnex.Analysis.CStarAlgebra