Exact source: MathlibAnnex/Analysis/CStarAlgebra/State/Irreducible.lean
Pinned GitHub source · Raw UTF-8 source
Back to The GNS representation of a pure state is irreducible
1import Mathlib.Analysis.InnerProductSpace.Projection.Basic2import MathlibAnnex.Analysis.CStarAlgebra.Representation.Cyclic3import MathlibAnnex.Analysis.CStarAlgebra.State.Purity45/-!6# Pure states give irreducible GNS representations7-/89set_option autoImplicit false1011open Set12open scoped ComplexOrder InnerProduct1314namespace MathlibAnnex.Analysis.CStarAlgebra1516universe u v1718variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]19variable {H : Type v}20variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]2122/-- A cyclic representation whose unit-vector state is pure is irreducible. -/23theorem isIrreducible_starAlgHom_of_isPureState24 (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 := by28 intro K hKclosed hKreduces29 letI : IsClosed (K : Set H) := hKclosed30 letI : CompleteSpace K := inferInstance31 letI : K.HasOrthogonalProjection := inferInstance32 let P : H →L[ℂ] H := K.starProjection33 let x : H := P xi34 let y : H := xi - x35 let rho : A →L[ℂ] ℂ := Representation.vectorFunctional pi x36 have hxK : x ∈ K := K.starProjection_apply_mem xi37 have hyK : y ∈ Kᗮ := K.sub_starProjection_mem_orthogonal xi38 have hmapK (a : A) : pi a x ∈ K := (hKreduces a).1 hxK39 have hmapOrth (a : A) : pi a y ∈ Kᗮ :=40 Representation.map_mem_orthogonal_of_adjoint_mem (pi a) K41 (hKreduces a).2 hyK42 have hdecomp (a : A) :43 Representation.vectorFunctional pi xi a =44 rho a + Representation.vectorFunctional pi y a := by45 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 := by52 intro a ha53 exact Representation.vectorFunctional_nonnegative pi x ha54 have hrho_le : ∀ a : A, 0 ≤ a →55 rho a ≤ Representation.vectorFunctional pi xi a := by56 intro a ha57 rw [hdecomp]58 exact le_add_of_nonneg_right59 (Representation.vectorFunctional_nonnegative pi y ha)60 obtain ⟨t, ht, ht_one, hrho⟩ := eq_smul_of_pureState_of_nonnegative_le61 (Representation.vectorFunctional pi xi) rho hpure hrho_nonneg hrho_le62 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 := by65 simpa [P, x, ContinuousLinearMap.comp_apply] using66 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) := by69 calc70 inner ℂ (pi a xi) (P (pi b xi)) =71 inner ℂ (P (pi a xi)) (pi b xi) := by72 exact (K.inner_starProjection_left_eq_right (pi a xi) (pi b xi)).symm73 _ = inner ℂ (P (pi a xi)) (P (pi b xi)) := by74 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)).symm76 _ = 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).symm79 have hinner (a b : A) :80 inner ℂ (pi a xi) (P (pi b xi)) =81 inner ℂ (pi a xi) (t • pi b xi) := by82 calc83 inner ℂ (pi a xi) (P (pi b xi)) = rho (star a * b) := hgram a b84 _ = (t • Representation.vectorFunctional pi xi) (star a * b) := by rw [hrho]85 _ = t • inner ℂ (pi a xi) (pi b xi) := by86 simp only [smul_apply, Representation.vectorFunctional_star_mul]87 _ = inner ℂ (pi a xi) (t • pi b xi) := by88 simpa [Complex.real_smul] using89 (inner_smul_right (pi a xi) (pi b xi) (t : ℂ)).symm90 have hP_on_orbit (b : A) : P (pi b xi) = t • pi b xi := by91 apply ext_inner_left ℂ92 intro z93 exact hcyclic.induction_on z94 (isClosed_eq (continuous_id.inner continuous_const)95 (continuous_id.inner continuous_const)) fun a ↦ hinner a b96 have hP : P = t • ContinuousLinearMap.id ℂ H := by97 apply ContinuousLinearMap.ext98 intro z99 exact hcyclic.induction_on z100 (isClosed_eq P.continuous (t • ContinuousLinearMap.id ℂ H).continuous) fun b ↦ by101 simpa [StarAlgHom.orbitMap] using hP_on_orbit b102 have hxi_ne : xi ≠ 0 := by103 intro hzero104 simpa [hzero] using hxi105 have ht_idem : t * t = t := by106 apply smul_left_injective ℝ hxi_ne107 have hidem := congrArg (fun T : H →L[ℂ] H ↦ T xi)108 K.isIdempotentElem_starProjection.eq109 change P (P xi) = P xi at hidem110 rw [hP] at hidem111 simpa [smul_smul] using hidem112 have ht_cases : t = 0 ∨ t = 1 := by113 rcases eq_zero_or_eq_zero_of_mul_eq_zero114 (show t * (t - 1) = 0 by nlinarith) with h | h115 · exact Or.inl h116 · exact Or.inr (sub_eq_zero.mp h)117 rcases ht_cases with rfl | rfl118 · left119 rw [← K.range_starProjection]120 simp [P] at hP121 simpa [hP]122 · right123 rw [← K.range_starProjection]124 simp [P] at hP125 simpa [hP]126127/-- The canonical GNS representation of a pure state is irreducible. -/128theorem isIrreducible_pureState_gnsStarAlgHom129 (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) (hpure : IsPureState A phi) :130 StarAlgHom.IsIrreducible131 (positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom := by132 apply isIrreducible_starAlgHom_of_isPureState133 (positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom134 (stateGNSVector phi hphi) (norm_stateGNSVector phi hphi)135 (denseRange_gnsStarAlgHom_stateGNSVector phi hphi)136 have hfunctional :137 Representation.vectorFunctional138 (positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom139 (stateGNSVector phi hphi) = phi := by140 apply ContinuousLinearMap.ext141 intro a142 exact inner_gnsStarAlgHom_stateGNSVector phi hphi a143 rw [hfunctional]144 exact hpure145146end MathlibAnnex.Analysis.CStarAlgebra