Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/NoCompacts.lean
Pinned GitHub source · Raw UTF-8 source
Back to An irreducible CAR representation has no nonzero compact image
1import MathlibAnnex.Analysis.CStarAlgebra.CompactPreimage2import MathlibAnnex.Analysis.CStarAlgebra.Representation.Adapters3import MathlibAnnex.Analysis.CStarAlgebra.CAR.Simplicity4import MathlibAnnex.Analysis.CStarAlgebra.PureStateGNS.PureIrreducible56/-!7# Absence of compact operators in irreducible CAR representations89Simplicity makes every nonzero unital representation faithful. Pulling the10compact operators back to a closed two-sided ideal then excludes every11nonzero compact image, using the already proved infinite-dimensionality of12the completed CAR algebra.13-/1415set_option autoImplicit false1617open MathlibAnnex.Analysis.CStarAlgebra1819namespace MathlibAnnex.CStarAlgebra.CAR2021universe v2223variable {H : Type v}24variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]2526/-- A nonzero irreducible unital representation of the completed CAR algebra27is faithful. -/28theorem representation_injective29 (rho : Representation Limit H) (hrho : rho.IsIrreducible) :30 Function.Injective rho := by31 letI : Nontrivial H := Representation.nontrivial_of_isNonzero rho hrho.132 exact rho.toRingHom.injective3334/-- No nonzero element of the completed CAR algebra can have compact image in35a nonzero irreducible representation. -/36theorem eq_zero_of_isCompactOperator_image37 (rho : Representation Limit H) (hrho : rho.IsIrreducible)38 {a : Limit} (ha : IsCompactOperator (rho a)) : a = 0 := by39 exact MathlibAnnex.CStarAlgebra.eq_zero_of_isCompactOperator_of_injective40 not_finiteDimensional isSimpleCStarAlgebra_limit.2 rho41 (representation_injective rho hrho) ha4243/-- The canonical GNS representation of a pure CAR state has no nonzero44compact operator in its represented range. This is the concrete45no-compacts input used by the local pure-state approximation argument. -/46theorem eq_zero_of_isCompactOperator_pureGNS_image47 (phi : Limit →L[ℂ] ℂ) (hphi : phi ∈ MathlibAnnex.CStarAlgebra.stateSpace Limit)48 (hpure : MathlibAnnex.CStarAlgebra.IsPureState Limit phi) {a : Limit}49 (ha : IsCompactOperator50 ((MathlibAnnex.CStarAlgebra.positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom a)) :51 a = 0 := by52 let f := MathlibAnnex.CStarAlgebra.positiveLinearMapOfMemStateSpace phi hphi53 let xi : f.GNS := f.gnsCyclicVector54 have hxi : ‖xi‖ = 1 := PositiveLinearMap.norm_gnsCyclicVector f55 (MathlibAnnex.CStarAlgebra.positiveLinearMapOfMemStateSpace_one phi hphi)56 have hxi_ne : xi ≠ 0 := by57 intro hzero58 simpa [hzero] using hxi59 letI : Nontrivial f.GNS := nontrivial_of_ne xi 0 hxi_ne60 have hirr : Representation.IsIrreducible f.gnsStarAlgHom :=61 (Representation.isIrreducible_iff_starAlgHom f.gnsStarAlgHom).262 (MathlibAnnex.CStarAlgebra.isIrreducible_pureState_gnsStarAlgHom phi hphi hpure)63 exact eq_zero_of_isCompactOperator_image f.gnsStarAlgHom hirr ha6465/-- Range formulation of the preceding theorem: a compact operator belonging66to a pure CAR GNS image is the zero operator. -/67theorem eq_zero_of_mem_range_pureGNS_of_isCompactOperator68 (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.range73 (MathlibAnnex.CStarAlgebra.positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom)74 (hcompact : IsCompactOperator T) : T = 0 := by75 obtain ⟨a, rfl⟩ := hT76 rw [eq_zero_of_isCompactOperator_pureGNS_image phi hphi hpure hcompact,77 map_zero]7879end MathlibAnnex.CStarAlgebra.CAR