Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/NoCompacts.lean, lines 34–41.
Back to An irreducible CAR representation has no nonzero compact image
1import MathlibAnnex.Analysis.CStarAlgebra.CompactPreimage 2import MathlibAnnex.Analysis.CStarAlgebra.Representation.Adapters 3import MathlibAnnex.Analysis.CStarAlgebra.CAR.Simplicity 4import MathlibAnnex.Analysis.CStarAlgebra.PureStateGNS.PureIrreducible 5 6/-! 7# Absence of compact operators in irreducible CAR representations 8 9Simplicity makes every nonzero unital representation faithful. Pulling the 10compact operators back to a closed two-sided ideal then excludes every 11nonzero compact image, using the already proved infinite-dimensionality of 12the completed CAR algebra. 13-/ 14 15set_option autoImplicit false 16 17open MathlibAnnex.Analysis.CStarAlgebra 18 19namespace MathlibAnnex.CStarAlgebra.CAR 20 21universe v 22 23variable {H : Type v} 24variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 25 26/-- A nonzero irreducible unital representation of the completed CAR algebra 27is faithful. -/ 28theorem representation_injective 29 (rho : Representation Limit H) (hrho : rho.IsIrreducible) : 30 Function.Injective rho := by 31 letI : Nontrivial H := Representation.nontrivial_of_isNonzero rho hrho.1 32 exact rho.toRingHom.injective 33 34/-- No nonzero element of the completed CAR algebra can have compact image in 35a nonzero irreducible representation. -/ 36theorem eq_zero_of_isCompactOperator_image 37 (rho : Representation Limit H) (hrho : rho.IsIrreducible) 38 {a : Limit} (ha : IsCompactOperator (rho a)) : a = 0 := by 39 exact MathlibAnnex.CStarAlgebra.eq_zero_of_isCompactOperator_of_injective 40 not_finiteDimensional isSimpleCStarAlgebra_limit.2 rho 41 (representation_injective rho hrho) ha 42 43/-- The canonical GNS representation of a pure CAR state has no nonzero 44compact operator in its represented range. This is the concrete 45no-compacts input used by the local pure-state approximation argument. -/ 46theorem eq_zero_of_isCompactOperator_pureGNS_image 47 (phi : Limit →L[ℂ] ℂ) (hphi : phi ∈ MathlibAnnex.CStarAlgebra.stateSpace Limit) 48 (hpure : MathlibAnnex.CStarAlgebra.IsPureState Limit phi) {a : Limit} 49 (ha : IsCompactOperator 50 ((MathlibAnnex.CStarAlgebra.positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom a)) : 51 a = 0 := by 52 let f := MathlibAnnex.CStarAlgebra.positiveLinearMapOfMemStateSpace phi hphi 53 let xi : f.GNS := f.gnsCyclicVector 54 have hxi : ‖xi‖ = 1 := PositiveLinearMap.norm_gnsCyclicVector f 55 (MathlibAnnex.CStarAlgebra.positiveLinearMapOfMemStateSpace_one phi hphi) 56 have hxi_ne : xi ≠ 0 := by 57 intro hzero 58 simpa [hzero] using hxi 59 letI : Nontrivial f.GNS := nontrivial_of_ne xi 0 hxi_ne 60 have hirr : Representation.IsIrreducible f.gnsStarAlgHom := 61 (Representation.isIrreducible_iff_starAlgHom f.gnsStarAlgHom).2 62 (MathlibAnnex.CStarAlgebra.isIrreducible_pureState_gnsStarAlgHom phi hphi hpure) 63 exact eq_zero_of_isCompactOperator_image f.gnsStarAlgHom hirr ha 64 65/-- Range formulation of the preceding theorem: a compact operator belonging 66to a pure CAR GNS image is the zero operator. -/ 67theorem eq_zero_of_mem_range_pureGNS_of_isCompactOperator 68 (phi : Limit →L[ℂ] ℂ) (hphi : phi ∈ MathlibAnnex.CStarAlgebra.stateSpace Limit) 69 (hpure : MathlibAnnex.CStarAlgebra.IsPureState Limit phi) 70 {T : (MathlibAnnex.CStarAlgebra.positiveLinearMapOfMemStateSpace phi hphi).GNS →L[ℂ] 71 (MathlibAnnex.CStarAlgebra.positiveLinearMapOfMemStateSpace phi hphi).GNS} 72 (hT : T ∈ Set.range 73 (MathlibAnnex.CStarAlgebra.positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom) 74 (hcompact : IsCompactOperator T) : T = 0 := by 75 obtain ⟨a, rfl⟩ := hT 76 rw [eq_zero_of_isCompactOperator_pureGNS_image phi hphi hpure hcompact, 77 map_zero] 78 79end MathlibAnnex.CStarAlgebra.CAR