Exact source: MathlibAnnex/Analysis/CStarAlgebra/CompactPreimage.lean
Pinned GitHub source · Raw UTF-8 source
Back to Every operator in a singleton image is compact · Back to A unital singleton model acts in finite dimension · Back to The preimage ideal of the compact operators
1import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap2import Mathlib.Analysis.CStarAlgebra.Hom3import Mathlib.Analysis.InnerProductSpace.LinearMap4import Mathlib.Analysis.Normed.Operator.Compact.FiniteDimension5import Mathlib.RingTheory.TwoSidedIdeal.Basic6import Mathlib.Topology.Algebra.Module.FiniteDimension78/-!9# The ideal pulled back from the compact operators1011For a star representation on a Hilbert space, the elements represented by12compact operators form a norm-closed two-sided ideal. Consequently an13injective representation of an infinite-dimensional simple unital C-star14algebra contains no nonzero compact operator.15-/1617set_option autoImplicit false1819open scoped CStarAlgebra2021namespace MathlibAnnex.CStarAlgebra2223universe u v2425variable {A : Type u}26variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]2728/-- 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 (by34 change rho 0 ∈ compactOperator (RingHom.id ℂ) H H35 rw [map_zero]36 exact Submodule.zero_mem _)37 (fun {x y} hx hy => by38 change rho x ∈ compactOperator (RingHom.id ℂ) H H at hx39 change rho y ∈ compactOperator (RingHom.id ℂ) H H at hy40 change rho (x + y) ∈ compactOperator (RingHom.id ℂ) H H41 rw [map_add]42 exact Submodule.add_mem _ hx hy)43 (fun {x} hx => by44 change rho x ∈ compactOperator (RingHom.id ℂ) H H at hx45 change rho (-x) ∈ compactOperator (RingHom.id ℂ) H H46 rw [map_neg]47 exact Submodule.neg_mem _ hx)48 (fun {x y} hy => by49 change rho y ∈ compactOperator (RingHom.id ℂ) H H at hy50 change rho (x * y) ∈ compactOperator (RingHom.id ℂ) H H51 rw [map_mul]52 have hxy : (rho x).comp (rho y) ∈ compactOperator (RingHom.id ℂ) H H := by53 change IsCompactOperator ⇑((rho x).comp (rho y))54 exact hy.clm_comp (rho x)55 exact hxy)56 (fun {x y} hx => by57 change rho x ∈ compactOperator (RingHom.id ℂ) H H at hx58 change rho (x * y) ∈ compactOperator (RingHom.id ℂ) H H59 rw [map_mul]60 have hxy : (rho x).comp (rho y) ∈ compactOperator (RingHom.id ℂ) H H := by61 change IsCompactOperator ⇑((rho x).comp (rho y))62 exact hx.comp_clm (rho y)63 exact hxy)6465@[simp] theorem mem_compactPreimageIdeal [NonUnitalCStarAlgebra A]66 (rho : A →⋆ₙₐ[ℂ] (H →L[ℂ] H)) (a : A) :67 a ∈ compactPreimageIdeal rho ↔ IsCompactOperator (rho a) := by68 unfold compactPreimageIdeal69 rw [TwoSidedIdeal.mem_mk']70 rfl7172/-- The compact-operator preimage is norm closed. -/73theorem isClosed_compactPreimageIdeal [NonUnitalCStarAlgebra A]74 (rho : A →⋆ₙₐ[ℂ] (H →L[ℂ] H)) :75 IsClosed (compactPreimageIdeal rho : Set A) := by76 let rhoL : A →L[ℂ] (H →L[ℂ] H) :=77 (LinearMapClass.linearMap rho).mkContinuous 1 fun a => by78 change ‖rho a‖ ≤ 1 * ‖a‖79 simpa only [one_mul] using NonUnitalStarAlgHom.norm_apply_le rho a80 have hcarrier : (compactPreimageIdeal rho : Set A) =81 rhoL ⁻¹' (compactOperator (RingHom.id ℂ) H H : Set (H →L[ℂ] H)) := by82 ext a83 rw [Set.mem_preimage, SetLike.mem_coe, mem_compactPreimageIdeal]84 change IsCompactOperator ⇑(rho a) ↔ IsCompactOperator ⇑(rhoL a)85 rfl86 have hclosed : IsClosed87 (compactOperator (RingHom.id ℂ) H H : Set (H →L[ℂ] H)) := by88 change IsClosed {T : H →L[ℂ] H | IsCompactOperator T}89 exact isClosed_setOf_isCompactOperator90 rw [hcarrier]91 exact hclosed.preimage rhoL.continuous9293/-- In an injective representation of an infinite-dimensional algebra with94no nontrivial closed two-sided ideals, every compact image is zero. The95finite-dimensional target contradiction is proved here rather than hidden in96a `no-compacts` premise. -/97theorem eq_zero_of_isCompactOperator_of_injective98 [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 := by102 let rhoNU := rho.toNonUnitalStarAlgHom103 let I := compactPreimageIdeal rhoNU104 have haI : a ∈ I := (mem_compactPreimageIdeal rhoNU a).2 ha105 rcases hsimple I (isClosed_compactPreimageIdeal rhoNU) with hI | hI106 · rw [hI] at haI107 simpa using haI108 · have hH : ¬ Subsingleton H := by109 intro hsub110 letI : Subsingleton H := hsub111 have : (1 : A) = 0 := hrho (Subsingleton.elim _ _)112 exact one_ne_zero this113 letI : Nontrivial H := not_subsingleton_iff_nontrivial.mp hH114 have honeI : (1 : A) ∈ I := by rw [hI]; exact Set.mem_univ 1115 have hcompactOne : IsCompactOperator ((1 : H →L[ℂ] H) : H → H) := by116 have : IsCompactOperator (rho (1 : A)) :=117 (mem_compactPreimageIdeal rhoNU 1).1 honeI118 simpa only [map_one, one_apply_eq_self] using this119 letI : FiniteDimensional ℂ H := by120 apply FiniteDimensional.of_isCompactOperator_id121 change IsCompactOperator (fun x : H => x)122 exact hcompactOne123 letI : FiniteDimensional ℂ (H →L[ℂ] H) :=124 ContinuousLinearMap.finiteDimensional125 exact (hA (FiniteDimensional.of_injective126 (LinearMapClass.linearMap rho) hrho)).elim127128end MathlibAnnex.CStarAlgebra