Exact source: MathlibAnnex/Analysis/CStarAlgebra/CompactPreimage.lean, lines 97–126.
Back to An irreducible CAR representation has no nonzero compact image
1import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap 2import Mathlib.Analysis.CStarAlgebra.Hom 3import Mathlib.Analysis.InnerProductSpace.LinearMap 4import Mathlib.Analysis.Normed.Operator.Compact.FiniteDimension 5import Mathlib.RingTheory.TwoSidedIdeal.Basic 6import Mathlib.Topology.Algebra.Module.FiniteDimension 7 8/-! 9# The ideal pulled back from the compact operators 10 11For a star representation on a Hilbert space, the elements represented by 12compact operators form a norm-closed two-sided ideal. Consequently an 13injective representation of an infinite-dimensional simple unital C-star 14algebra contains no nonzero compact operator. 15-/ 16 17set_option autoImplicit false 18 19open scoped CStarAlgebra 20 21namespace MathlibAnnex.CStarAlgebra 22 23universe u v 24 25variable {A : Type u} 26variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 27 28/-- The inverse image of the compact operators under a star representation, 29as an algebraic two-sided ideal. -/ 30def compactPreimageIdeal [NonUnitalCStarAlgebra A] 31 (rho : A →⋆ₙₐ[ℂ] (H →L[ℂ] H)) : TwoSidedIdeal A := 32 TwoSidedIdeal.mk' {a | rho a ∈ compactOperator (RingHom.id ℂ) H H} 33 (by 34 change rho 0 ∈ compactOperator (RingHom.id ℂ) H H 35 rw [map_zero] 36 exact Submodule.zero_mem _) 37 (fun {x y} hx hy => by 38 change rho x ∈ compactOperator (RingHom.id ℂ) H H at hx 39 change rho y ∈ compactOperator (RingHom.id ℂ) H H at hy 40 change rho (x + y) ∈ compactOperator (RingHom.id ℂ) H H 41 rw [map_add] 42 exact Submodule.add_mem _ hx hy) 43 (fun {x} hx => by 44 change rho x ∈ compactOperator (RingHom.id ℂ) H H at hx 45 change rho (-x) ∈ compactOperator (RingHom.id ℂ) H H 46 rw [map_neg] 47 exact Submodule.neg_mem _ hx) 48 (fun {x y} hy => by 49 change rho y ∈ compactOperator (RingHom.id ℂ) H H at hy 50 change rho (x * y) ∈ compactOperator (RingHom.id ℂ) H H 51 rw [map_mul] 52 have hxy : (rho x).comp (rho y) ∈ compactOperator (RingHom.id ℂ) H H := by 53 change IsCompactOperator ⇑((rho x).comp (rho y)) 54 exact hy.clm_comp (rho x) 55 exact hxy) 56 (fun {x y} hx => by 57 change rho x ∈ compactOperator (RingHom.id ℂ) H H at hx 58 change rho (x * y) ∈ compactOperator (RingHom.id ℂ) H H 59 rw [map_mul] 60 have hxy : (rho x).comp (rho y) ∈ compactOperator (RingHom.id ℂ) H H := by 61 change IsCompactOperator ⇑((rho x).comp (rho y)) 62 exact hx.comp_clm (rho y) 63 exact hxy) 64 65@[simp] theorem mem_compactPreimageIdeal [NonUnitalCStarAlgebra A] 66 (rho : A →⋆ₙₐ[ℂ] (H →L[ℂ] H)) (a : A) : 67 a ∈ compactPreimageIdeal rho ↔ IsCompactOperator (rho a) := by 68 unfold compactPreimageIdeal 69 rw [TwoSidedIdeal.mem_mk'] 70 rfl 71 72/-- The compact-operator preimage is norm closed. -/ 73theorem isClosed_compactPreimageIdeal [NonUnitalCStarAlgebra A] 74 (rho : A →⋆ₙₐ[ℂ] (H →L[ℂ] H)) : 75 IsClosed (compactPreimageIdeal rho : Set A) := by 76 let rhoL : A →L[ℂ] (H →L[ℂ] H) := 77 (LinearMapClass.linearMap rho).mkContinuous 1 fun a => by 78 change ‖rho a‖ ≤ 1 * ‖a‖ 79 simpa only [one_mul] using NonUnitalStarAlgHom.norm_apply_le rho a 80 have hcarrier : (compactPreimageIdeal rho : Set A) = 81 rhoL ⁻¹' (compactOperator (RingHom.id ℂ) H H : Set (H →L[ℂ] H)) := by 82 ext a 83 rw [Set.mem_preimage, SetLike.mem_coe, mem_compactPreimageIdeal] 84 change IsCompactOperator ⇑(rho a) ↔ IsCompactOperator ⇑(rhoL a) 85 rfl 86 have hclosed : IsClosed 87 (compactOperator (RingHom.id ℂ) H H : Set (H →L[ℂ] H)) := by 88 change IsClosed {T : H →L[ℂ] H | IsCompactOperator T} 89 exact isClosed_setOf_isCompactOperator 90 rw [hcarrier] 91 exact hclosed.preimage rhoL.continuous 92 93/-- In an injective representation of an infinite-dimensional algebra with 94no nontrivial closed two-sided ideals, every compact image is zero. The 95finite-dimensional target contradiction is proved here rather than hidden in 96a `no-compacts` premise. -/ 97theorem eq_zero_of_isCompactOperator_of_injective 98 [CStarAlgebra A] [Nontrivial A] (hA : ¬ FiniteDimensional ℂ A) 99 (hsimple : ∀ I : TwoSidedIdeal A, IsClosed (I : Set A) → I = ⊥ ∨ I = ⊤) 100 (rho : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (hrho : Function.Injective rho) 101 {a : A} (ha : IsCompactOperator (rho a)) : a = 0 := by 102 let rhoNU := rho.toNonUnitalStarAlgHom 103 let I := compactPreimageIdeal rhoNU 104 have haI : a ∈ I := (mem_compactPreimageIdeal rhoNU a).2 ha 105 rcases hsimple I (isClosed_compactPreimageIdeal rhoNU) with hI | hI 106 · rw [hI] at haI 107 simpa using haI 108 · have hH : ¬ Subsingleton H := by 109 intro hsub 110 letI : Subsingleton H := hsub 111 have : (1 : A) = 0 := hrho (Subsingleton.elim _ _) 112 exact one_ne_zero this 113 letI : Nontrivial H := not_subsingleton_iff_nontrivial.mp hH 114 have honeI : (1 : A) ∈ I := by rw [hI]; exact Set.mem_univ 1 115 have hcompactOne : IsCompactOperator ((1 : H →L[ℂ] H) : H → H) := by 116 have : IsCompactOperator (rho (1 : A)) := 117 (mem_compactPreimageIdeal rhoNU 1).1 honeI 118 simpa only [map_one, one_apply_eq_self] using this 119 letI : FiniteDimensional ℂ H := by 120 apply FiniteDimensional.of_isCompactOperator_id 121 change IsCompactOperator (fun x : H => x) 122 exact hcompactOne 123 letI : FiniteDimensional ℂ (H →L[ℂ] H) := 124 ContinuousLinearMap.finiteDimensional 125 exact (hA (FiniteDimensional.of_injective 126 (LinearMapClass.linearMap rho) hrho)).elim 127 128end MathlibAnnex.CStarAlgebra