Exact source: MathlibAnnex/Analysis/CStarAlgebra/CompactModel.lean
Pinned GitHub source · Raw UTF-8 source
Back to A compact-operator model for a representation · Back to A singleton model is faithful and exactly compact-valued · Back to Compact-operator conclusion for the unital singleton condition
1import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap2import Mathlib.Analysis.InnerProductSpace.LinearMap3import Mathlib.Analysis.Normed.Operator.Compact.FiniteDimension4import Mathlib.Topology.Algebra.Module.FiniteDimension56/-!7# Algebraic models of the compact operators89The fixed Mathlib version exposes compact operators as a predicate/submodule,10not as a bundled star algebra. `IsCompactOperatorModel` is the exact range11characterization of an ordinary nonunital star-algebra isomorphism onto all12compact operators.13-/1415set_option autoImplicit false1617open scoped InnerProduct1819namespace MathlibAnnex.Analysis.CStarAlgebra2021universe u v2223variable {A : Type u}24variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]2526/-- A nonunital star representation that is injective and has precisely the27compact operators as its range. This is the unbundled form of a star28isomorphism 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 = T3435omit [CompleteSpace H] in36/-- Rank-one operators are compact, proved by factoring through the37one-dimensional scalar field. -/38theorem isCompactOperator_rankOne (x y : H) :39 IsCompactOperator (InnerProductSpace.rankOne ℂ x y) := by40 rw [InnerProductSpace.rankOne_def']41 exact (isCompactOperator_of_locallyCompactSpace_dom42 (innerSL ℂ y)).clm_comp43 (ContinuousLinearMap.toSpanSingleton ℂ x)4445theorem map_one_eq_one_of_isCompactOperatorModel [Nontrivial H]46 [CStarAlgebra A]47 (e : A →⋆ₙₐ[ℂ] (H →L[ℂ] H)) (he : IsCompactOperatorModel e) : e 1 = 1 := by48 apply ContinuousLinearMap.ext49 intro x50 change e 1 x = x51 obtain ⟨y, hy⟩ := exists_norm_ne_zero H52 let z : H := ‖y‖⁻¹ • y53 have hz : ‖z‖ = 1 := by54 dsimp [z]55 simp [norm_smul, inv_mul_cancel₀ hy]56 let T : H →L[ℂ] H := InnerProductSpace.rankOne ℂ x z57 obtain ⟨a, ha⟩ := he.2.2 T (isCompactOperator_rankOne x z)58 have hleft : e 1 * T = T := by59 rw [← ha, ← map_mul, one_mul]60 have hTz : T z = x := by61 simp [T, InnerProductSpace.rankOne_apply,62 inner_self_eq_norm_sq_to_K, hz]63 calc64 e 1 x = e 1 (T z) := congrArg (e 1) hTz.symm65 _ = (e 1 * T) z := rfl66 _ = T z := congrArg (fun S : H →L[ℂ] H => S z) hleft67 _ = x := hTz6869/-- A nonzero unital infinite-dimensional C-star algebra cannot be70star-isomorphic to the compact operators on any Hilbert space, including the71zero Hilbert space. -/72theorem not_isCompactOperatorModel_of_infiniteDimensional73 [CStarAlgebra A] [Nontrivial A] (hA : ¬ FiniteDimensional ℂ A)74 (e : A →⋆ₙₐ[ℂ] (H →L[ℂ] H)) : ¬ IsCompactOperatorModel e := by75 intro he76 have hH : ¬ Subsingleton H := by77 intro hsub78 letI : Subsingleton H := hsub79 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 hH82 have hone := map_one_eq_one_of_isCompactOperatorModel e he83 have hcompact_one : IsCompactOperator ((1 : H →L[ℂ] H) : H → H) := by84 rw [← hone]85 exact he.2.1 186 haveI : FiniteDimensional ℂ H := by87 apply FiniteDimensional.of_isCompactOperator_id88 change IsCompactOperator (fun x : H => x)89 exact hcompact_one90 haveI : FiniteDimensional ℂ (H →L[ℂ] H) :=91 ContinuousLinearMap.finiteDimensional92 exact hA93 (FiniteDimensional.of_injective (LinearMapClass.linearMap e) he.1)9495end MathlibAnnex.Analysis.CStarAlgebra