Exact source: MathlibAnnex/Analysis/CStarAlgebra/CompactModel.lean, lines 72–92.
Back to The shell-generated algebra is not an algebra of all compact operators
1import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap 2import Mathlib.Analysis.InnerProductSpace.LinearMap 3import Mathlib.Analysis.Normed.Operator.Compact.FiniteDimension 4import Mathlib.Topology.Algebra.Module.FiniteDimension 5 6/-! 7# Algebraic models of the compact operators 8 9The fixed Mathlib version exposes compact operators as a predicate/submodule, 10not as a bundled star algebra. `IsCompactOperatorModel` is the exact range 11characterization of an ordinary nonunital star-algebra isomorphism onto all 12compact operators. 13-/ 14 15set_option autoImplicit false 16 17open scoped InnerProduct 18 19namespace MathlibAnnex.Analysis.CStarAlgebra 20 21universe u v 22 23variable {A : Type u} 24variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 25 26/-- A nonunital star representation that is injective and has precisely the 27compact operators as its range. This is the unbundled form of a star 28isomorphism with `K(H)`. -/ 29def IsCompactOperatorModel [NonUnitalCStarAlgebra A] 30 (e : A →⋆ₙₐ[ℂ] (H →L[ℂ] H)) : Prop := 31 Function.Injective e ∧ 32 (∀ a : A, IsCompactOperator (e a)) ∧ 33 ∀ T : H →L[ℂ] H, IsCompactOperator T → ∃ a : A, e a = T 34 35omit [CompleteSpace H] in 36/-- Rank-one operators are compact, proved by factoring through the 37one-dimensional scalar field. -/ 38theorem isCompactOperator_rankOne (x y : H) : 39 IsCompactOperator (InnerProductSpace.rankOne ℂ x y) := by 40 rw [InnerProductSpace.rankOne_def'] 41 exact (isCompactOperator_of_locallyCompactSpace_dom 42 (innerSL ℂ y)).clm_comp 43 (ContinuousLinearMap.toSpanSingleton ℂ x) 44 45theorem map_one_eq_one_of_isCompactOperatorModel [Nontrivial H] 46 [CStarAlgebra A] 47 (e : A →⋆ₙₐ[ℂ] (H →L[ℂ] H)) (he : IsCompactOperatorModel e) : e 1 = 1 := by 48 apply ContinuousLinearMap.ext 49 intro x 50 change e 1 x = x 51 obtain ⟨y, hy⟩ := exists_norm_ne_zero H 52 let z : H := ‖y‖⁻¹ • y 53 have hz : ‖z‖ = 1 := by 54 dsimp [z] 55 simp [norm_smul, inv_mul_cancel₀ hy] 56 let T : H →L[ℂ] H := InnerProductSpace.rankOne ℂ x z 57 obtain ⟨a, ha⟩ := he.2.2 T (isCompactOperator_rankOne x z) 58 have hleft : e 1 * T = T := by 59 rw [← ha, ← map_mul, one_mul] 60 have hTz : T z = x := by 61 simp [T, InnerProductSpace.rankOne_apply, 62 inner_self_eq_norm_sq_to_K, hz] 63 calc 64 e 1 x = e 1 (T z) := congrArg (e 1) hTz.symm 65 _ = (e 1 * T) z := rfl 66 _ = T z := congrArg (fun S : H →L[ℂ] H => S z) hleft 67 _ = x := hTz 68 69/-- A nonzero unital infinite-dimensional C-star algebra cannot be 70star-isomorphic to the compact operators on any Hilbert space, including the 71zero Hilbert space. -/ 72theorem not_isCompactOperatorModel_of_infiniteDimensional 73 [CStarAlgebra A] [Nontrivial A] (hA : ¬ FiniteDimensional ℂ A) 74 (e : A →⋆ₙₐ[ℂ] (H →L[ℂ] H)) : ¬ IsCompactOperatorModel e := by 75 intro he 76 have hH : ¬ Subsingleton H := by 77 intro hsub 78 letI : Subsingleton H := hsub 79 have hmap : e (1 : A) = e 0 := Subsingleton.elim _ _ 80 exact one_ne_zero (he.1 hmap) 81 letI : Nontrivial H := not_subsingleton_iff_nontrivial.mp hH 82 have hone := map_one_eq_one_of_isCompactOperatorModel e he 83 have hcompact_one : IsCompactOperator ((1 : H →L[ℂ] H) : H → H) := by 84 rw [← hone] 85 exact he.2.1 1 86 haveI : FiniteDimensional ℂ H := by 87 apply FiniteDimensional.of_isCompactOperator_id 88 change IsCompactOperator (fun x : H => x) 89 exact hcompact_one 90 haveI : FiniteDimensional ℂ (H →L[ℂ] H) := 91 ContinuousLinearMap.finiteDimensional 92 exact hA 93 (FiniteDimensional.of_injective (LinearMapClass.linearMap e) he.1) 94 95end MathlibAnnex.Analysis.CStarAlgebra