MATHLIBANNEX / EXACT SOURCE v0.4.0

MathlibAnnex.CStarAlgebra.compactPreimageIdeal

def compactPreimageIdeal [NonUnitalCStarAlgebra A]
    (rho : A →⋆ₙₐ[ℂ] (H →L[ℂ] H)) : TwoSidedIdeal A

1 import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap
2 import Mathlib.Analysis.CStarAlgebra.Hom
3 import Mathlib.Analysis.InnerProductSpace.LinearMap
4 import Mathlib.Analysis.Normed.Operator.Compact.FiniteDimension
5 import Mathlib.RingTheory.TwoSidedIdeal.Basic
6 import Mathlib.Topology.Algebra.Module.FiniteDimension
7 
8 /-!
9 # The ideal pulled back from the compact operators
10 
11 For a star representation on a Hilbert space, the elements represented by
12 compact operators form a norm-closed two-sided ideal.  Consequently an
13 injective representation of an infinite-dimensional simple unital C-star
14 algebra contains no nonzero compact operator.
15 -/
16 
17 set_option autoImplicit false
18 
19 open scoped CStarAlgebra
20 
21 namespace MathlibAnnex.CStarAlgebra
22 
23 universe u v
24 
25 variable {A : Type u}
26 variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
27 
28 /-- The inverse image of the compact operators under a star representation,
29 as an algebraic two-sided ideal. -/
30 def 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. -/
73 theorem 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
94 no nontrivial closed two-sided ideals, every compact image is zero.  The
95 finite-dimensional target contradiction is proved here rather than hidden in
96 a `no-compacts` premise. -/
97 theorem 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 
128 end MathlibAnnex.CStarAlgebra