Exact source: MathlibAnnex/Analysis/CStarAlgebra/NonUnital/CompactRange.lean
Pinned GitHub source · Raw UTF-8 source
Back to Every rank-one operator has an algebra preimage
1import Mathlib.Analysis.CStarAlgebra.Hom2import Mathlib.Analysis.InnerProductSpace.Adjoint3import Mathlib.Analysis.InnerProductSpace.PiL24import Mathlib.Topology.MetricSpace.Cover5import MathlibAnnex.Analysis.CStarAlgebra.NonUnital.RankOneProjection67/-!8# Rank-one operators in the range of a non-unital representation910Once an irreducible representation contains one rank-one projection, dense11orbits and closedness of an injective C-star homomorphism put every rank-one12operator in its range.13-/1415set_option autoImplicit false1617open Function Set18open scoped InnerProduct1920namespace MathlibAnnex.Analysis.CStarAlgebra2122universe u v2324variable {A : Type u} [NonUnitalCStarAlgebra A]25variable {H : Type v}26variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]2728namespace NonUnitalCStarRepresentation2930/-- A vector fixed by a represented projection has dense orbit under the31original non-unital algebra, not merely under its unitization. -/32theorem denseRange_apply_of_isIrreducible_of_fixed33 (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) := by36 have hirrU := isIrreducible_unitization pi hirr37 have horbitU : DenseRange (fun z : Unitization ℂ A => pi.unitization z e) :=38 Representation.denseRange_orbitMap_of_isIrreducible pi.unitization hirrU he39 rw [Metric.denseRange_iff] at horbitU ⊢40 intro y epsilon hepsilon41 obtain ⟨z, hz⟩ := horbitU y epsilon hepsilon42 induction z using Unitization.ind with43 | inl_add_inr c a =>44 refine ⟨c • p + a, ?_⟩45 simpa [unitization, hpe] using hz4647/-- Algebraic rank-one links obtained from one represented rank-one48projection. -/49theorem map_mul_projection_mul_star_eq_rankOne50 (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) := by55 apply ContinuousLinearMap.ext56 intro x57 simp only [map_mul, map_star, mul_apply_eq_comp, ContinuousLinearMap.comp_apply,58 hmap, InnerProductSpace.rankOne_apply, map_smul]59 congr 160 rw [ContinuousLinearMap.star_eq_adjoint]61 exact ContinuousLinearMap.adjoint_inner_right (pi b) e x6263/-- If an injective irreducible representation contains one rank-one64projection, then every rank-one operator belongs to its range. -/65theorem exists_preimage_rankOne_of_rankOne_projection66 (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 := by71 have hene : e ≠ 0 := by72 intro hzero73 simp [hzero] at he74 have hpe : pi p e = e := by75 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 hpe80 have hclosed : IsClosed (Set.range pi) :=81 (NonUnitalStarAlgHom.isometry pi hinj).isClosedEmbedding.isClosed_range82 have hright (a : A) (y : H) :83 InnerProductSpace.rankOne ℂ (pi a e) y ∈ Set.range pi := by84 exact horbit.induction_on y85 (hclosed.preimage (by fun_prop)) fun b => by86 refine ⟨a * p * star b, ?_⟩87 exact map_mul_projection_mul_star_eq_rankOne pi hmap88 intro x y89 have hx : InnerProductSpace.rankOne ℂ x y ∈ Set.range pi := by90 exact horbit.induction_on x91 (hclosed.preimage (by fun_prop)) fun a => hright a y92 exact hx9394/-- Under the genuinely non-unital singleton hypothesis, every rank-one95operator has a preimage in the original algebra. -/96theorem 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 := by102 obtain ⟨p, _hp, _hpne, ⟨e, he, hmap⟩, _hcompact⟩ :=103 exists_nonzero_projection_rankOne_map pi hsingle104 exact exists_preimage_rankOne_of_rankOne_projection pi hsingle.1105 (injective_of_singleton pi hsingle) he hmap106107/-- A finite sum of rank-one operators has a preimage whenever each108rank-one operator does. -/109theorem exists_preimage_sum_rankOne110 (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) := by116 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 i120121/-- Compact operators on a Hilbert space are norm limits of finite sums of122rank-one operators. This local formulation targets the closed range of an123injective representation directly. -/124theorem exists_preimage_of_isCompactOperator_of_rankOne_preimages125 (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 := by131 classical132 have hclosed : IsClosed (Set.range pi) :=133 (NonUnitalStarAlgHom.isometry pi hinj).isClosedEmbedding.isClosed_range134 have hclosure : T ∈ closure (Set.range pi) := by135 rw [Metric.mem_closure_iff]136 intro epsilon hepsilon137 let delta : ℝ := epsilon / 2138 have hdelta : 0 < delta := by dsimp [delta]; positivity139 let K : Set H := closure (T '' Metric.closedBall 0 1)140 have hK : IsCompact K := by141 exact hT.isCompact_closure_image_closedBall 1142 obtain ⟨N, hNK, hNfinite, hNcover⟩ :=143 hK.finite_cover_balls hdelta144 let E : Submodule ℂ H := Submodule.span ℂ N145 letI : FiniteDimensional ℂ E :=146 FiniteDimensional.span_of_finite ℂ hNfinite147 letI : E.HasOrthogonalProjection := inferInstance148 let P : H →L[ℂ] H := E.starProjection149 let S : H →L[ℂ] H := P * T150 let b : OrthonormalBasis (Fin (Module.finrank ℂ E)) ℂ E :=151 stdOrthonormalBasis ℂ E152 have hSsum : S = ∑ i,153 InnerProductSpace.rankOne ℂ ((b i : E) : H)154 (ContinuousLinearMap.adjoint T ((b i : E) : H)) := by155 dsimp [S, P]156 rw [b.starProjection_eq_sum_rankOne, Finset.sum_mul]157 apply Finset.sum_congr rfl158 intro i _159 exact InnerProductSpace.rankOne_comp160 ((b i : E) : H) ((b i : E) : H) T161 obtain ⟨a, ha⟩ := exists_preimage_sum_rankOne pi hpre162 (fun i => ((b i : E) : H))163 (fun i => ContinuousLinearMap.adjoint T ((b i : E) : H))164 have hSrange : S ∈ Set.range pi := by165 refine ⟨a, ?_⟩166 exact ha.trans hSsum.symm167 have hunit (x : H) (hx : ‖x‖ ≤ 1) :168 ‖T x - P (T x)‖ < delta := by169 have hTxK : T x ∈ K := by170 apply subset_closure171 exact ⟨x, by simpa using hx, rfl⟩172 have hcovered := hNcover hTxK173 simp only [Set.mem_iUnion, exists_prop, Metric.mem_ball] at hcovered174 obtain ⟨n, hnN, hn⟩ := hcovered175 rw [E.starProjection_minimal]176 refine lt_of_le_of_lt177 (ciInf_le ⟨0, Set.forall_mem_range.mpr fun _ => norm_nonneg _⟩178 (⟨n, Submodule.subset_span hnN⟩ : E)) ?_179 simpa [dist_eq_norm] using hn180 have hnorm : ‖T - S‖ ≤ delta := by181 apply ContinuousLinearMap.opNorm_le_bound' (T - S) hdelta.le182 intro x hxne183 let z : H := ((‖x‖⁻¹ : ℝ) : ℂ) • x184 have hxpos : 0 < ‖x‖ :=185 norm_pos_iff.mpr (norm_ne_zero_iff.mp hxne)186 have hz : ‖z‖ = 1 := by187 simp [z, norm_smul, hxpos.ne']188 have hzbound : ‖T z - P (T z)‖ < delta := hunit z hz.le189 have hxrepr : x = ((‖x‖ : ℝ) : ℂ) • z := by190 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 := by194 calc195 (T - P * T) x =196 (T - P * T) (((‖x‖ : ℝ) : ℂ) • z) :=197 congrArg (T - P * T) hxrepr198 _ = ((‖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 := by202 simpa [mul_apply_eq_comp] using hzbound203 simpa [mul_comm] using204 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 hclosure209 exact hclosure210211/-- The compact operators are contained in the range of a genuinely212non-unital singleton model. -/213theorem 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 := by220 apply exists_preimage_of_isCompactOperator_of_rankOne_preimages pi221 (injective_of_singleton pi hsingle)222 (exists_preimage_rankOne_of_singleton pi hsingle) T hT223224end NonUnitalCStarRepresentation225226end MathlibAnnex.Analysis.CStarAlgebra