MATHLIBANNEX / EXACT SOURCE v0.4.0
MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_preimage_of_compact_singleton
theorem exists_preimage_of_compact_singleton [Nontrivial A]
[PartialOrder A] [StarOrderedRing A]
[TopologicalSpace.SeparableSpace H]
(pi : NonUnitalCStarRepresentation A H)
(hsingle : IsSingletonIrreducibleModel.{u, v, u} pi)
(T : H →L[ℂ] H) (hT : IsCompactOperator T) :
∃ a : A, pi a = T1 import Mathlib.Analysis.CStarAlgebra.Hom 2 import Mathlib.Analysis.InnerProductSpace.Adjoint 3 import Mathlib.Analysis.InnerProductSpace.PiL2 4 import Mathlib.Topology.MetricSpace.Cover 5 import MathlibAnnex.Analysis.CStarAlgebra.NonUnital.RankOneProjection 6 7 /-! 8 # Rank-one operators in the range of a non-unital representation 9 10 Once an irreducible representation contains one rank-one projection, dense 11 orbits and closedness of an injective C-star homomorphism put every rank-one 12 operator in its range. 13 -/ 14 15 set_option autoImplicit false 16 17 open Function Set 18 open scoped InnerProduct 19 20 namespace MathlibAnnex.Analysis.CStarAlgebra 21 22 universe u v 23 24 variable {A : Type u} [NonUnitalCStarAlgebra A] 25 variable {H : Type v} 26 variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 27 28 namespace NonUnitalCStarRepresentation 29 30 /-- A vector fixed by a represented projection has dense orbit under the 31 original non-unital algebra, not merely under its unitization. -/ 32 theorem denseRange_apply_of_isIrreducible_of_fixed 33 (pi : NonUnitalCStarRepresentation A H) (hirr : pi.IsIrreducible) 34 {p : A} {e : H} (he : e ≠ 0) (hpe : pi p e = e) : 35 DenseRange (fun a : A => pi a e) := by 36 have hirrU := isIrreducible_unitization pi hirr 37 have horbitU : DenseRange (fun z : Unitization ℂ A => pi.unitization z e) := 38 Representation.denseRange_orbitMap_of_isIrreducible pi.unitization hirrU he 39 rw [Metric.denseRange_iff] at horbitU ⊢ 40 intro y epsilon hepsilon 41 obtain ⟨z, hz⟩ := horbitU y epsilon hepsilon 42 induction z using Unitization.ind with 43 | inl_add_inr c a => 44 refine ⟨c • p + a, ?_⟩ 45 simpa [unitization, hpe] using hz 46 47 /-- Algebraic rank-one links obtained from one represented rank-one 48 projection. -/ 49 theorem map_mul_projection_mul_star_eq_rankOne 50 (pi : NonUnitalCStarRepresentation A H) 51 {p a b : A} {e : H} 52 (hmap : pi p = InnerProductSpace.rankOne ℂ e e) : 53 pi (a * p * star b) = 54 InnerProductSpace.rankOne ℂ (pi a e) (pi b e) := by 55 apply ContinuousLinearMap.ext 56 intro x 57 simp only [map_mul, map_star, mul_apply_eq_comp, ContinuousLinearMap.comp_apply, 58 hmap, InnerProductSpace.rankOne_apply, map_smul] 59 congr 1 60 rw [ContinuousLinearMap.star_eq_adjoint] 61 exact ContinuousLinearMap.adjoint_inner_right (pi b) e x 62 63 /-- If an injective irreducible representation contains one rank-one 64 projection, then every rank-one operator belongs to its range. -/ 65 theorem exists_preimage_rankOne_of_rankOne_projection 66 (pi : NonUnitalCStarRepresentation A H) 67 (hirr : pi.IsIrreducible) (hinj : Function.Injective pi) 68 {p : A} {e : H} (he : ‖e‖ = 1) 69 (hmap : pi p = InnerProductSpace.rankOne ℂ e e) : 70 ∀ x y : H, ∃ a : A, pi a = InnerProductSpace.rankOne ℂ x y := by 71 have hene : e ≠ 0 := by 72 intro hzero 73 simp [hzero] at he 74 have hpe : pi p e = e := by 75 rw [hmap] 76 simp [InnerProductSpace.rankOne_apply, 77 inner_self_eq_norm_sq_to_K, he] 78 have horbit : DenseRange (fun a : A => pi a e) := 79 denseRange_apply_of_isIrreducible_of_fixed pi hirr hene hpe 80 have hclosed : IsClosed (Set.range pi) := 81 (NonUnitalStarAlgHom.isometry pi hinj).isClosedEmbedding.isClosed_range 82 have hright (a : A) (y : H) : 83 InnerProductSpace.rankOne ℂ (pi a e) y ∈ Set.range pi := by 84 exact horbit.induction_on y 85 (hclosed.preimage (by fun_prop)) fun b => by 86 refine ⟨a * p * star b, ?_⟩ 87 exact map_mul_projection_mul_star_eq_rankOne pi hmap 88 intro x y 89 have hx : InnerProductSpace.rankOne ℂ x y ∈ Set.range pi := by 90 exact horbit.induction_on x 91 (hclosed.preimage (by fun_prop)) fun a => hright a y 92 exact hx 93 94 /-- Under the genuinely non-unital singleton hypothesis, every rank-one 95 operator has a preimage in the original algebra. -/ 96 theorem exists_preimage_rankOne_of_singleton [Nontrivial A] 97 [PartialOrder A] [StarOrderedRing A] 98 [TopologicalSpace.SeparableSpace H] 99 (pi : NonUnitalCStarRepresentation A H) 100 (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) : 101 ∀ x y : H, ∃ a : A, pi a = InnerProductSpace.rankOne ℂ x y := by 102 obtain ⟨p, _hp, _hpne, ⟨e, he, hmap⟩, _hcompact⟩ := 103 exists_nonzero_projection_rankOne_map pi hsingle 104 exact exists_preimage_rankOne_of_rankOne_projection pi hsingle.1 105 (injective_of_singleton pi hsingle) he hmap 106 107 /-- A finite sum of rank-one operators has a preimage whenever each 108 rank-one operator does. -/ 109 theorem exists_preimage_sum_rankOne 110 (pi : NonUnitalCStarRepresentation A H) 111 {I : Type*} [Fintype I] 112 (hpre : ∀ x y : H, ∃ a : A, 113 pi a = InnerProductSpace.rankOne ℂ x y) 114 (x y : I → H) : 115 ∃ a : A, pi a = ∑ i, InnerProductSpace.rankOne ℂ (x i) (y i) := by 116 choose a ha using fun i => hpre (x i) (y i) 117 refine ⟨∑ i, a i, ?_⟩ 118 rw [map_sum] 119 exact Finset.sum_congr rfl fun i _ => ha i 120 121 /-- Compact operators on a Hilbert space are norm limits of finite sums of 122 rank-one operators. This local formulation targets the closed range of an 123 injective representation directly. -/ 124 theorem exists_preimage_of_isCompactOperator_of_rankOne_preimages 125 (pi : NonUnitalCStarRepresentation A H) 126 (hinj : Function.Injective pi) 127 (hpre : ∀ x y : H, ∃ a : A, 128 pi a = InnerProductSpace.rankOne ℂ x y) 129 (T : H →L[ℂ] H) (hT : IsCompactOperator T) : 130 ∃ a : A, pi a = T := by 131 classical 132 have hclosed : IsClosed (Set.range pi) := 133 (NonUnitalStarAlgHom.isometry pi hinj).isClosedEmbedding.isClosed_range 134 have hclosure : T ∈ closure (Set.range pi) := by 135 rw [Metric.mem_closure_iff] 136 intro epsilon hepsilon 137 let delta : ℝ := epsilon / 2 138 have hdelta : 0 < delta := by dsimp [delta]; positivity 139 let K : Set H := closure (T '' Metric.closedBall 0 1) 140 have hK : IsCompact K := by 141 exact hT.isCompact_closure_image_closedBall 1 142 obtain ⟨N, hNK, hNfinite, hNcover⟩ := 143 hK.finite_cover_balls hdelta 144 let E : Submodule ℂ H := Submodule.span ℂ N 145 letI : FiniteDimensional ℂ E := 146 FiniteDimensional.span_of_finite ℂ hNfinite 147 letI : E.HasOrthogonalProjection := inferInstance 148 let P : H →L[ℂ] H := E.starProjection 149 let S : H →L[ℂ] H := P * T 150 let b : OrthonormalBasis (Fin (Module.finrank ℂ E)) ℂ E := 151 stdOrthonormalBasis ℂ E 152 have hSsum : S = ∑ i, 153 InnerProductSpace.rankOne ℂ ((b i : E) : H) 154 (ContinuousLinearMap.adjoint T ((b i : E) : H)) := by 155 dsimp [S, P] 156 rw [b.starProjection_eq_sum_rankOne, Finset.sum_mul] 157 apply Finset.sum_congr rfl 158 intro i _ 159 exact InnerProductSpace.rankOne_comp 160 ((b i : E) : H) ((b i : E) : H) T 161 obtain ⟨a, ha⟩ := exists_preimage_sum_rankOne pi hpre 162 (fun i => ((b i : E) : H)) 163 (fun i => ContinuousLinearMap.adjoint T ((b i : E) : H)) 164 have hSrange : S ∈ Set.range pi := by 165 refine ⟨a, ?_⟩ 166 exact ha.trans hSsum.symm 167 have hunit (x : H) (hx : ‖x‖ ≤ 1) : 168 ‖T x - P (T x)‖ < delta := by 169 have hTxK : T x ∈ K := by 170 apply subset_closure 171 exact ⟨x, by simpa using hx, rfl⟩ 172 have hcovered := hNcover hTxK 173 simp only [Set.mem_iUnion, exists_prop, Metric.mem_ball] at hcovered 174 obtain ⟨n, hnN, hn⟩ := hcovered 175 rw [E.starProjection_minimal] 176 refine lt_of_le_of_lt 177 (ciInf_le ⟨0, Set.forall_mem_range.mpr fun _ => norm_nonneg _⟩ 178 (⟨n, Submodule.subset_span hnN⟩ : E)) ?_ 179 simpa [dist_eq_norm] using hn 180 have hnorm : ‖T - S‖ ≤ delta := by 181 apply ContinuousLinearMap.opNorm_le_bound' (T - S) hdelta.le 182 intro x hxne 183 let z : H := ((‖x‖⁻¹ : ℝ) : ℂ) • x 184 have hxpos : 0 < ‖x‖ := 185 norm_pos_iff.mpr (norm_ne_zero_iff.mp hxne) 186 have hz : ‖z‖ = 1 := by 187 simp [z, norm_smul, hxpos.ne'] 188 have hzbound : ‖T z - P (T z)‖ < delta := hunit z hz.le 189 have hxrepr : x = ((‖x‖ : ℝ) : ℂ) • z := by 190 simp [z, hxpos.ne'] 191 change ‖(T - P * T) x‖ ≤ delta * ‖x‖ 192 have hmaprepr : (T - P * T) x = 193 ((‖x‖ : ℝ) : ℂ) • (T - P * T) z := by 194 calc 195 (T - P * T) x = 196 (T - P * T) (((‖x‖ : ℝ) : ℂ) • z) := 197 congrArg (T - P * T) hxrepr 198 _ = ((‖x‖ : ℝ) : ℂ) • (T - P * T) z := map_smul _ _ _ 199 rw [hmaprepr, norm_smul, Complex.norm_real, 200 Real.norm_eq_abs, abs_of_nonneg (norm_nonneg x)] 201 have herr : ‖(T - P * T) z‖ < delta := by 202 simpa [mul_apply_eq_comp] using hzbound 203 simpa [mul_comm] using 204 mul_le_mul_of_nonneg_left herr.le (norm_nonneg x) 205 refine ⟨S, hSrange, ?_⟩ 206 rw [dist_eq_norm] 207 exact hnorm.trans_lt (by dsimp [delta]; linarith) 208 rw [hclosed.closure_eq] at hclosure 209 exact hclosure 210 211 /-- The compact operators are contained in the range of a genuinely 212 non-unital singleton model. -/ 213 theorem exists_preimage_of_compact_singleton [Nontrivial A] 214 [PartialOrder A] [StarOrderedRing A] 215 [TopologicalSpace.SeparableSpace H] 216 (pi : NonUnitalCStarRepresentation A H) 217 (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) 218 (T : H →L[ℂ] H) (hT : IsCompactOperator T) : 219 ∃ a : A, pi a = T := by 220 apply exists_preimage_of_isCompactOperator_of_rankOne_preimages pi 221 (injective_of_singleton pi hsingle) 222 (exists_preimage_rankOne_of_singleton pi hsingle) T hT 223 224 end NonUnitalCStarRepresentation 225 226 end MathlibAnnex.Analysis.CStarAlgebra