MATHLIBANNEX / EXACT SOURCE v0.4.0

MathlibAnnex.Analysis.CStarAlgebra.IsCompactOperatorModel

Raw UTF-8 source

def IsCompactOperatorModel [NonUnitalCStarAlgebra A]
    (e : A →⋆ₙₐ[ℂ] (H →L[ℂ] H)) : Prop

1 import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap
2 import Mathlib.Analysis.InnerProductSpace.LinearMap
3 import Mathlib.Analysis.Normed.Operator.Compact.FiniteDimension
4 import Mathlib.Topology.Algebra.Module.FiniteDimension
5 
6 /-!
7 # Algebraic models of the compact operators
8 
9 The fixed Mathlib version exposes compact operators as a predicate/submodule,
10 not as a bundled star algebra.  `IsCompactOperatorModel` is the exact range
11 characterization of an ordinary nonunital star-algebra isomorphism onto all
12 compact operators.
13 -/
14 
15 set_option autoImplicit false
16 
17 open scoped InnerProduct
18 
19 namespace MathlibAnnex.Analysis.CStarAlgebra
20 
21 universe u v
22 
23 variable {A : Type u}
24 variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
25 
26 /-- A nonunital star representation that is injective and has precisely the
27 compact operators as its range.  This is the unbundled form of a star
28 isomorphism with `K(H)`. -/
29 def 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 
35 omit [CompleteSpace H] in
36 /-- Rank-one operators are compact, proved by factoring through the
37 one-dimensional scalar field. -/
38 theorem 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 
45 theorem 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
70 star-isomorphic to the compact operators on any Hilbert space, including the
71 zero Hilbert space. -/
72 theorem 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 
95 end MathlibAnnex.Analysis.CStarAlgebra